proof: closed_by_stub rides in the signed receipt (SPEC §6.1) #72
Loading…
Reference in a new issue
No description provided.
Delete branch "proof/stub-on-the-wire"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
Closes the last open item from #62: whether the stand-in marker enters the JCR-1 wire.
The defect is an internal inconsistency in the spec. §5.2 says a relying party "MUST check" whether the closing rung discharged anything — but §6 never put that marker in the receipt, so a party holding only the artifact could not perform the check §5.2 asks of them. A verifier that must consult the prover to learn whether a proof is real is not a verifier.
What the published pack ships today, signed and verifying:
Goldbach's conjecture, sealed as proved, with nothing in the bytes to qualify it.
No existing field answers it.
closed_bynames a tier —T0is the propositional decider inreal_ladderand aGoalKindgate inreference_ladder, same tag.energy_provenancequalifies energy,spec_groundingqualifies intent. This is the only field that says whether the verdict was earned.Emit-when-true is what makes it non-breaking, and it was measured before committing rather than assumed:
All 4 move only because all 4 come from the all-stand-in
reference_ladder. The cost is confined to fixtures, and is zero for every honest proof — pinned byte-for-byte against the canonical core, not just by inspecting the map.44 tests pass across proof-rs; all 10 conformance checks (C1–C6 + 4 negatives) pass against the regenerated vectors; nothing outside
proof/consumes the pack.Also documents
ceiling_ujin the §6 table — emitted since the joule-ceiling work but never listed, which is the same class of defect.Not merged deliberately — this changes a published signed format, so the call is yours.
SPEC §5.2 already says a relying party "MUST check" whether the rung that closed a goal discharged anything. Until now that marker lived only on the in-process `CascadeResult`, so a party holding **only the receipt** — which is the entire purpose of sealing one — could not perform the check the spec asks of them. A verifier that must consult the prover to learn whether a proof is real is not a verifier. What the published pack ships today, signed and verifying under the steward key: { "verdict": "proved", "closed_by": "T3", "artifact": "ae28bd3b…", <- hash of the goal restated "spec_grounding": "Ungrounded" } That is Goldbach's conjecture, sealed as proved, with nothing in the bytes to qualify it. Not forged — honestly signed and substantively empty, which is worse, because it verifies. No existing field answers it. `closed_by` names a TIER, and the same tag covers a real decision procedure on one ladder and a stand-in on another (`T0` is the propositional decider in `real_ladder`, a `GoalKind` gate in `reference_ladder`). `energy_provenance` qualifies the energy; `spec_grounding` qualifies the intent. This is the only field that says whether the VERDICT was earned. Emit-when-true is normative, not an optimisation, and it is what makes this revision non-breaking: * a receipt closed by a real solver canonicalizes to EXACTLY the bytes it did before this field existed — verified byte-for-byte against the canonical core, not merely by inspecting the map — so every such receipt sealed under an earlier revision still verifies untouched; * the byte cost falls entirely on receipts that were making an unearned claim. Measured before committing: all 4 published vectors change (+16 bytes, new ids and envelopes) because every one of them comes from the all-stand-in `reference_ladder` — that is the whole accepted cost, and it is confined to fixtures. Nothing outside `proof/` consumes the pack. 44 tests pass across proof-rs and all 10 conformance checks (C1–C6, four negatives) still pass against the regenerated vectors. Also documents `ceiling_uj` in the §6 core table. The code has emitted it since the joule-ceiling work; the spec never listed it, and an artifact that says more than its specification is the same class of defect this commit closes. Co-Authored-By: Claude Opus 5 <[email protected]>