proof: universally-proven conditional laws export a plain-logic companion form#500
Merged
Conversation
…nion form Every when-law that earns a universal proof in the side build now ships a companion theorem alongside its twin: premises lowered to plain logical hypotheses (Bool conjunctions split, bare comparisons un-coerced, == conclusions lowered to equality) via a fixed bridge tactic, so later proofs can apply the law directly with no Bool/Prop bridging at the call site. Crediting is untouched by construction: the audit probes only the theorem names recorded in the lane index, and companions are never indexed — there is no path for a companion to count as a credited law. A companion lives in its twin's module, so a failing twin takes the companion down with it (the existing sabotage test covers the pair). All emitted companions certify within the kernel-axiom whitelist on the live builds (json, the synthetic lane fixtures, the Peano bridge laws). Counted builds byte-identical; json's universal credit unchanged. Known sharp edge (pre-existing class, measured during review): a sibling law deliberately named <law>_prop — like <law>_universal before this change — collides with the emitted name and withholds the original law's credit (fail-closed, never grants); a collision guard is queued for the lane-imports follow-up. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
First increment of conditional helper lemmas (measured feasibility probe:
prompts/conditional-helper-lemmas-probe.md): every when-law with a universal proof in the side build now ships a Prop-form companion next to its twin — premises lowered to plain hypotheses,==conclusions lowered to=, one fixed bridge tactic covering all three measured Bool/Prop seams. Future increments let later laws consume these companions via explicithave(the probe proved the full chain on the 1996 paper's hardest-lemma shapes, including a 39-line core-Lean proof of the floor-stability brick).Fail-closed by construction
Gates
when_universal5, exact credited set, counted summary identical across normal/sabotage/revert).cargo test --workspacegreen (live proof_spec 145); fmt/clippy clean.Known sharp edge (measured, queued)
A sibling law deliberately named
<law>_propcollides with the emitted name and withholds the original credit (never grants) — same pre-existing hazard class as_universalon the baseline (measured both). Collision guard queued for the next increment, which touches lane naming anyway.🤖 Generated with Claude Code