propositions

name	propositions
description	Extract atomic propositions from a math manuscript .tex file into a JSONL structural representation, then run R1-R8 mechanical validation. Each prop carries text (verbatim from .tex), location (line range), cites (internal UUID dependency DAG), asserts (atomic claims), claim_type, and evidence_class. Use when: starting propositions side-file for a new manuscript, re-extracting after large rewrite, or running mechanical gate before audit. NOT for L4 semantic walk — that's the /proofread skill. v0.1.0 SCAFFOLDING — execution body TODO. Source-of-truth scripts currently in PsychQuantHsu/psychophysical_representations/scripts/validate-propositions.py.
allowed-tools	["Read","Write","Edit","Bash","AskUserQuestion"]

Propositions — Extract + Validate

Status (v0.1.0)

Scaffolding only. Execution body deferred to v0.2.0+. Until then, run the source-of-truth scripts directly:

# Validate (R1-R8 mechanical gate)
python3 scripts/validate-propositions.py \
  --jsonl manuscript/propositions/main.jsonl \
  --meta manuscript/propositions/_meta.json \
  --tex manuscript/main.tex
# Exit 0 = all pass; exit 1 = at least one rule fail

# Refresh location field after main.tex line shift
python3 scripts/refresh-prop-locations.py --jsonl manuscript/propositions/main.jsonl

Both scripts live at PsychQuantHsu/psychophysical_representations/scripts/ (will be extracted to this plugin in v0.2.0).

R1-R8 Coverage (frozen contract)

Rule	What it checks	False-negative pitfall
R1	prop.text verbatim found in main.tex (via normalize_for_match)	substring containment is line-anchor-blind → location-drift silent (use R9-pending or refresh script)
R1.5	surjective coverage — every .tex paragraph covered by ≥1 prop	informational, not blocking; WARN-only
R2	every cite UUID resolves to an existing prop	catches typo / deletion gaps
R3	cite graph is a DAG (no cycles)	structural, not semantic — DAG ≠ logical implication (L4 walk needed)
R4	mechanical-contradiction PATTERN-A/B	catches boundary-axiom violations like #60 #68
R6	sentence/clause-index v1.1 invariants hold	catches granularity drift
R7	every prop.id is canonical UUID v7 (RFC 9562 §5.7)	gates id-format compliance
R8	unique-ids within file	catches paste-clone errors

Execution Steps (v0.2.0 target — TODO)

Step 0: Bootstrap Stage Task List

TaskCreate parse_args / detect_jsonl_path / run_validator / parse_exit_code /
            classify_finding / decide_fix_path (refresh-locations / re-extract /
            split-prop / escalate-issue) / write_audit_summary

Step 1: Resolve manuscript root + JSONL paths

Walk up from cwd to find manuscript/propositions/main.jsonl (canonical) + optional _stage2/*.jsonl (staging area like Theorem 1 in source repo).

Step 2: Run validator, parse output

(TODO: structured-output mode for validate-propositions.py — feature request once script extracted)

Step 3: Triage findings → AskUserQuestion routing

Finding	Likely fix	Route
R1 fail (text drift)	manuscript-jsonl-sync.md scenario 1 (wording) — update prop.text verbatim	inline edit
R1 PASS but location stale	scenario 2 (line shift) — refresh-prop-locations.py	one-shot script
R2 dangling	scenario 4 (delete) — strip cites referencing deleted UUIDs	inline edit
R3 cycle	structural error — likely circular dependency in newly-added prop	escalate
R4 PATTERN-A	boundary-axiom contradiction	escalate to audit-finding issue
R6 / R7 / R8	schema violation — re-run EXTRACTION-PROMPT.md against affected section	re-extract

Cross-link

• Source dogfood: PsychQuantHsu/psychophysical_representations #107 (proofread workflow experiment, 3 pilots)
• Rule: ../../rules/manuscript-jsonl-sync.md — prop-level sync HARD RULE
• Sister skill: /math-tools:proofread for L4 alignment walk (semantic, not mechanical)
• Sister skill: /math-tools:manuscript-audit for R1-R4 cross-doc drift detection