propositions
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.
What this skill does
# 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:
```bash
# 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`](../../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
Related in Security
mac-ops
IncludedComprehensive macOS workstation operations — diagnose kernel panics, identify failing drives, audit launchd startup items, decode wake reasons, triage TCC permission denials, manage APFS snapshots, recover from no-boot. Use for: Mac is slow, slow bootup, won't boot, kernel panic, kernel_task hot, mds_stores CPU, photoanalysisd, cloudd, login loop, gray screen, sleep wake failure, drive failing, IO errors, APFS snapshots eating space, Time Machine local snapshots, Spotlight indexing, launchd, LaunchAgent, LaunchDaemon, login items, TCC permissions, Full Disk Access, Screen Recording denied, Gatekeeper, quarantine, com.apple.quarantine, app is damaged, helper tool, /Library/PrivilegedHelperTools, pmset, wake reasons, dark wake, sysdiagnose, panic.ips, DiagnosticReports, configuration profile, MDM profile, remote diagnostics over SSH.
a11y-audit
IncludedRun accessibility audits on web projects combining automated scanning (axe-core, Lighthouse) with WCAG 2.1 AA compliance mapping, manual check guidance, and structured reporting. Output is configurable: markdown report only, markdown plus machine-readable JSON, or markdown plus issue tracker integration. Use this skill whenever the user mentions "accessibility audit", "a11y audit", "WCAG audit", "accessibility check", "compliance scan", or asks to check a web project for accessibility issues. Also trigger when the user wants to verify WCAG conformance or map findings to a specific standard (CAN-ASC-6.2, EN 301 549, ADA/AODA).
erpclaw
IncludedAI-native ERP system with self-extending OS. Full accounting, invoicing, inventory, purchasing, tax, billing, HR, payroll, advanced accounting (ASC 606/842, intercompany, consolidation), and financial reporting. 413 actions across 14 domains, 43 expansion modules. Constitutional guardrails, adversarial audit, schema migration. Double-entry GL, immutable audit trail, US GAAP.
assess
IncludedAssesses and rates quality 0-10 across multiple dimensions (correctness, maintainability, security, performance, testability, simplicity) with pros/cons analysis. Compares against project conventions and prior decisions from memory. Produces structured evaluation reports with actionable improvement suggestions. Use when evaluating code, designs, architectures, or comparing alternative approaches.
spring-boot-security-jwt
IncludedProvides JWT authentication and authorization patterns for Spring Boot 3.5.x covering token generation with JJWT, Bearer/cookie authentication, database/OAuth2 integration, and RBAC/permission-based access control using Spring Security 6.x. Use when implementing authentication or authorization in Spring Boot applications.
code-hardcode-audit
IncludedDetect hardcoded values, magic numbers, and leaked secrets. TRIGGERS - hardcode audit, magic numbers, PLR2004, secret scanning.