Repository navigation
proofs: drop the Lean models of the 22 spec stubs #8054 deleted (Closes #8222) - #8223
Merged
Merged
Conversation
#8222) Since #8054, test-ratchet has been red on every PR. The cause is corpus_classifier_matches_lean_completeness, which reported 26 envs without matching specs where it expects 4. The other 22 were the env, module and theorem triples of the empty generated stubs that #8054 deleted. Completeness.lean loses those 66 definitions (418 lines). Nothing else referenced them, and none was in lean_completeness_mismatches.json. The test's anti-vacuity floor moves from 245 to 223. That is exactly the 22 deleted theorems: deletion, not a theorem going quiet. The four Lean-only witnesses stay as they are. Local check: cargo test --release -p t27c --test icarus_lowerable gives 359 passed. The test failed on master with the same message CI shows. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Contributor
gHashTag
pushed a commit
that referenced
this pull request
Oct 9, 2026
… (Refs #8222, Closes #7370) test-ratchet was red on this PR (and on master): #8054 deleted 22 empty spec stubs, but proofs/lean4/Trinity/IcarusLowerable/Completeness.lean still modelled them, so corpus_classifier_matches_lean_completeness found 26 envs without specs. #8223 fixes it; this is its two files, byte-identical to its head ad0b510, so it no-ops once #8223 lands. cargo test -p t27c --test icarus_lowerable corpus_classifier_matches_lean_completeness: ok. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ScHVrGSr6zZUdwkdC8DR9k
This was referenced Oct 9, 2026
This was referenced Oct 11, 2026
gHashTag
added a commit
that referenced
this pull request
Oct 11, 2026
…/string, tri/utils/error, sandbox/modules, physics/lqg_entropy (Closes #8908) (#8912) The last five pass_vacuous rows of the t27b ledger are stubs with nothing to assert (see #8766): a TODO with an empty main(), a module line with two `use` lines, a broken struct skeleton, a registry holding one `use`, and a prose file whose tests assert `true`. git grep finds no `use` of any of the five modules. They go as #8054's 22 stubs went: - the five specs, their 11 seals (spec_path matches) and their 5 ledger rows; pass_vacuous rows do not count toward max_not_pass, so it stays; - the Lean lowerability models of the three that had one (physics_lqg_entropy, tri_utils_error, tri_utils_string), and the floor of corpus_classifier_matches_lean_completeness 223 -> 220, deletion and not a theorem going quiet, as #8223 did for #8054 (hand-written lines +3 -3); none was in lean_completeness_mismatches.json; - their three lines in tools/oracle/baseline.tsv, pass 189 -> 186; - the dangling `sandbox.modules` dep of sandbox.health in architecture/graph.tri (no such node; health.t27 does not use it). lqg_entropy's prose was already section 5 of docs/nona-02-organism/physics-kepler/KEPLER-NEWTON-CHERN-SIMONS.md. Its one missing point, the two origins of gamma with its references, moves there, and the note's spec list points at specs/physics/lqg_cs_bridge.t27, which defines and tests every quantity the stub named. Lab (master 39d5af3): cargo test --release -p t27c --test icarus_lowerable, 359 passed, "220 theorems compared, 78 disagree (ledger holds 78)" (base: 223); t27b corpus before and after: the five files leave, pass_vacuous 6 -> 1 (the one left, eternal_monitor.t27, has no ledger row: the reference does not pass it). Co-authored-by: Claude <claude@anthropic.com> Co-authored-by: Claude Opus 5.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
2 participants
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.
Closes #8222.
Since #8054 deleted 22 empty generated spec stubs,
test-ratchethas been red on every PR. #8183 and #8155 are two of them. The failing test iscorpus_classifier_matches_lean_completeness:Fix
proofs/lean4/Trinity/IcarusLowerable/Completeness.lean: remove the_env,_moduleand_lowerabletriple of each of the 22 deleted specs. That is 66 definitions and 418 lines.proofs/,docs/orbootstrap/named them.docs/reports/lean_completeness_mismatches.json.tri_pipeline_pipeline_parallel, a live spec whose name shares a prefix, is untouched.bootstrap/tests/icarus_lowerable.rs: the anti-vacuity floor moves from 245 to 223 (+4/-3). After the first fix the test reached that floor and stopped at 223 checked plus 0 prose. The 22 that went away are exactly the deleted stubs' theorems, so the comment records the drop as deletion, not as a theorem going quiet.expected_missingis not widened. The four Lean-only witnesses stay as they were.Verified locally
cargo test --release -p t27c --test icarus_lowerablereports 359 passed, 0 failed.lake build) runs only in CI. The change only deletes definitions that nothing references.🤖 Generated with Claude Code