Repository navigation
fix(proofs): real Lean model for ar_ternary_logic, theorem = false; leave the ledger - #6684
Merged
Merged
Conversation
…eave the ledger The Lean model of specs/ar/ternary_logic.t27 was EMPTY, so native_decide proved the empty module lowerable while the classifier answers false. It is now a signature projection of the spec (as ar_asp_solver is): the three Trit consts, struct Rule, all ten functions, the 33 tests and nine benches by name, unmodeled types kept under their source names. Its theorem is `= false`, matching the classifier. A second theorem pins the reason #6658 names: with Trit declared as a lowerable struct, exactly backward_chain, resolve and apply_restraint -- the functions with a variable-length [Rule] / [Trit] in their signature -- are still not lowerable. Both theorems checked with Lean 4.31.0 core (Ast + Predicate) on the Railway lab; the old `= true` claim over the new model fails there, as it should. lowerability_models_keep_real_source_signatures now ties four of the model's signatures to what gen-rust emits for the spec. The ar_ternary_logic ledger entry from #6672 is removed; max_entries and max_vacuous return to 77 and 44. The theorem count is unchanged, so the 245 floor stays. The two hand-edited files get a one-time entry in tools/policy/foreign-exceptions.txt, removed again right after merge. Owner approved 2026-10-06 (all three options for #6658), translated. debt: #5980 Refs #6658 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
gHashTag
added
the
owner-approved-foreign
Contributor
Collaborator
Author
|
Lab run on 68b993e: green (frozen-hash, build, suite RATCHET CLEAN, lean ok, seal-currency, seal-coverage, specs-parse, specs-generate). https://t27c-lab-production.up.railway.app/runs/68b993e5be896d55577ac440526f68141f9dd5fd.json. Also on the lab: |
This was referenced Oct 6, 2026
Collaborator
Author
|
CI notes: |
Contributor
PR DashboardGenerated at: 2026-10-06 07:15:43 UTC
Summary
Seal Status
|
This was referenced Oct 6, 2026
Merged
Merged
Merged
…stall lake build has been red since the W472/W460 wave block landed in TernaryFPGABoot.lean with Rust-flavored syntax (struct ... where, .length, Array.forall) and identifiers the file never imported. Repaired in place: - Lean surface: structure/deriving, Array.set with proof, #[...] literals, arr.all; import Trinity.TernaryGemm for ternaryMac/ternaryGemm2x2. - raw_ns_preserved_under_jitter was false as stated (base 1000, jittered 1002); the 2 ns margin the claim needed now sits in the hypothesis. - worst_case_jitter_envelope_bound: 200000 was not a witness (eff + 2 only bounds the jittered value by 200002); tight witness 184002, bound proved by period*derating <= period*(23/20) <= 160000*(23/20) = 184000. - Array.getElem_set_self is namespaced in core; native_decide for the array lemma kernel decide cannot reduce. TernaryInference.lean: drop the three simp args the linter reports unused (Int.mul_neg x2, identityWeights) and rename 17 shadowed binders x -> _x. CI plumbing, same tree: - wasm-explorer.yml: cargo install wasm-objdump can never work (no such crate is published); install wabt from apt, which ships wasm-objdump. - test-baseline.txt: the corpus is fully parseable now, so the_dead_code_census_names_what_it_skipped fails on master too; one hand entry, reason in a comment, prune on next regen. - foreign-exceptions.txt: one-time entries for the two Lean files and the workflow repair. Refs #6658 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
This was referenced Oct 6, 2026
The sorry ratchet in lean-proofs.yml ran for the first time once the build went green and counted 434: batteries and mathlib ship `sorry` literals in their own test files under .lake/packages, which the recursive grep swept in. The ceiling of 5 describes the Trinity tree (3 real sorries in GoldenFloatRoundTrip + 2 prose mentions), which --exclude-dir=.lake restores. The gate's own comment says "Five sit in the tree today" -- the tree, not the dependencies. Refs #6658 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Contributor
PR DashboardGenerated at: 2026-10-06 11:07:39 UTC
Summary
Seal Status
|
This was referenced Oct 6, 2026
`-p t27-wasm-explorer` from the repo root can never resolve: the crate is on the workspace exclude list with its own Cargo.toml and Cargo.lock, and cargo only matches -p over workspace members. Run the build and the tests with working-directory set, as the crate's own header prescribes, and read the artifact from the package-local target dir. Verified locally: the wasm32 build finishes and the binary carries all four no_mangle exports. Refs #6658 Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
This was referenced Oct 6, 2026
Contributor
PR DashboardGenerated at: 2026-10-06 11:26:26 UTC
Summary
Seal Status
|
Contributor
PR DashboardGenerated at: 2026-10-06 11:30:55 UTC
Summary
Seal Status
|
This was referenced Oct 6, 2026
6 tasks
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
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.
Refs #6658
Owner approved 2026-10-06 (all three options for #6658), translated
debt: #5980
What
ar_ternary_logic_lowerableinproofs/lean4/Trinity/IcarusLowerable/Completeness.leanwas proven over an EMPTY model, so it said nothing aboutspecs/ar/ternary_logic.t27. This PR:ar_asp_solver): the threeTritconsts,struct Rule, all ten functions, the 33 tests and 9 benches by name; unmodeled types keep their source names (Trit,[Trit],[Rule]).= false, matching the Rust classifier.ar_ternary_logic_slices_block_with_trit_declared: withTritdeclared as a lowerable struct, exactlybackward_chain,resolveandapply_restraint(the variable-length[Rule]/[Trit]signatures) are still not lowerable. This name does not match the completeness regex, so the theorem count the 245 floor guards is unchanged.lowerability_models_keep_real_source_signatureswith fourar_ternary_logicsignatures taken fromt27c gen-rust, so the model cannot drift back to empty unnoticed.ar_ternary_logicledger entry added by fix(ledger): enter ar_ternary_logic Rust/Lean mismatch (fast green for #6658) #6672;max_entries77,max_vacuous44 again.tools/policy/foreign-exceptions.txt; a follow-up PR removes it right after merge.Evidence
Ast.lean+Predicate.lean+ the exact new block) on the Railway t27c lab: both theorems check. Negative control: the old claim= trueover the new model fails withnative_decide evaluated that the proposition ... is false.Option 3 (lower the 245 floor) is not needed: the theorem count is unchanged.
🤖 Generated with Claude Code