| name | use-case-d |
| description | The Squeeze Loop instance for Use Case D — formally verified Rocq (Coq) proofs of textbook arithmetic (e.g. commutativity of + on nat), on terrain A with a deductive lower bound (the Rocq kernel). The dominant failure is the prover discharging (Qed.) an adjacent weaker claim under the intended theorem name (e.g. right-identity n+0=n instead of n+m=m+n), or smuggling an axiom. The kernel (coqc) plus the axiom auditor (rocqchk --print-assumptions) is the immutable lower bound none of the actors can alter, and the exerciser authors false-theorem mutations the kernel must reject. Use when working on src/D — the textbook manifest, the formal theorem statement, the tactical proof, the false-theorem mutation matrix, the pinned Rocq stdlib, the prior-proofs regression registry, or the axiom audit. Trigger phrasings: "use case D", "instance D", "Rocq/Coq proof squeeze", "adjacent weaker theorem", "smuggled axiom / Admitted", "mutation must fail to compile", "Closed under the global context". |
Use Case D — the deductive-kernel proof squeeze loop
Use Case D is a base squeeze loop (instance-d, terrain A with a deductive lower
bound): formally verified Rocq proofs of textbook arithmetic. Its SL-1.0 self-description is
src/D/instance-d.sl.json; the companion write-up is
src/D/docs/use-case-d.md.
The dominant failure it guards
Coherent-and-wrong here = the prover discharges Qed. on an adjacent weaker claim under
the intended theorem name — proving right-identity n+0=n where the exercise asked for
commutativity n+m=m+n — or smuggles an axiom to close a goal it could not prove. The
proof compiles, the name matches, and the wrong theorem is "proved."
The bounds
- Upper bound
U — the textbook exercise manifest (English + scope clauses
CLAUSE_1..N), sharpened by the formalizer into a precise formal theorem statement
(the formalizer's lower bound is expressibility: the statement must type-check under
coqc + the pinned stdlib).
- Lower bound
L — the deductive kernel: coqc 8.20.1 (the proof must compile to
Qed.) plus the axiom auditor rocqchk --print-assumptions (must report "Closed
under the global context" — rejecting Admitted/Axiom). The pinned stdlib is immutable
(root 0555), and the prior-proofs registry is recompiled each cycle (no regression).
The cast (four actors)
| Actor | Builds | U | L | Must not see |
|---|
| Gate sentinel (coordinator) | plan approval, gate verdicts, the axiom audit, the .sl.json | manifest clauses | registry recompiled + proof compiled + axiom audit clean + every mutation rejected | — |
| Theorem formalizer (property author) | the formal theorem statement (the precise U) | the textbook exercise + scope clauses | expressibility: the statement type-checks under coqc + stdlib | the proof, the mutations |
| Tactical prover (implementer) | the tactical proof | the immutable formal statement | compiles to Qed. + passes the axiom audit | the mutations |
| Mutation exerciser | false-theorem mutations the kernel must reject | manifest clauses + the formal statement | each mutation must FAIL to compile (it is genuinely false) | the proof |
The barrier (physical, not honorary)
The prover never sees the mutations and the exerciser never sees the proof; the formalizer
sees neither — Unix 0700 homedirs, and the prover imports the statement one-way via
coqc Require only. The prover cannot tune to the mutations; the exerciser cannot crib the
proof's structure.
The gates
- Gate A (editorial). The plan cites every manifest scope clause.
- Gate B (machine). The registry recompiles (no regression), the proof compiles to
Qed., the axiom audit is clean (no Admitted/Axiom/admit), and every false
mutation is rejected by the kernel.
- Gate C (coverage). Every manifest clause appears in some mutation's
target_clauses.
Disjointness
The formalizer holds only the English manifest (never the proof or mutations); the prover
holds only the formal statement and the kernel (never the mutations); the exerciser holds
the manifest and the statement and authors falsehoods the kernel must reject (never the
proof). The deductive kernel (coqc + rocqchk) is the immutable lower bound none of them
can alter, and the registry pins prior proofs against regression. Catchability: a vacuous /
inconsistent statement is caught by the exerciser's vacuous-hypothesis mutation (and the
axiom audit catches smuggled axioms); an adjacent weaker theorem under the intended name is
caught by the exerciser's identity-flip mutations the kernel must reject; a missing mutation
for some clause is caught by the sentinel (Gate C).
python config/skills/sl-internal/scripts/sl_disjointness_check.py src/D/instance-d.sl.json
(0 FAIL / 11 checks.)
