Repository navigation
t27b ledger: delete the five vacuous stubs -- lsp/language, tri/utils/string, tri/utils/error, sandbox/modules, physics/lqg_entropy (Closes #8908) - #8912
Merged
Conversation
…/string, tri/utils/error, sandbox/modules, physics/lqg_entropy (Closes #8908) 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 Opus 5.5 <noreply@anthropic.com>
gHashTag
enabled auto-merge (squash)
October 11, 2026 04:09
Contributor
This was referenced Oct 11, 2026
gHashTag
added a commit
that referenced
this pull request
Oct 23, 2026
…s ledger, types ratchet, seals, one power test (#11735) Four master checks red, one common cause: three days of merges landed specs without re-sealing and with new fixture tables and type names. - Verilog widths: ledger the four CR-CHAT-03 treekem guards whose test-fixture const tables lower as one packed localparam each (257x21152, 1025x2176, 2049x8512, 4097x544 -- arithmetic in the ledger comment; the class and the maintainer question stay #2566) - types ratchet: bless the 11 names the CR-CHAT-03 and trios-server ports added (Provider, TestResults, TreeNode, UpdatePathRecord, DbHandle, OpenDbOptions, Edge, LLMConfig, OAuthTokenRow, RefinePromptRequest, RefinePromptResult) and drop the resolved Promise, as the ratchet demands - seals: re-seal the 19 moved seals (tri/net, pipeline, tools, demos, isa, t27os/pty_logic, idea_factory gen-drift) and delete the three lsp seals whose spec #8912 deleted; twins synced - power_analysis: #6860 set the within-typical-budget test's budget to 7000 while its own message says 6683; the measured estimate IS 6683, and is_within_budget is <=, so any budget >= the estimate fails the false expectation. A full trinity top at 6683 mW stands over a 6000 mW typical budget; the test reads 37/37, 0 vacuous Verified locally at 9222efe: check_verilog_widths --require exit 0 (14 known, 0 new, self-check 7/7), tri types ratchet exit 0 (133/133), check_seal_coverage exit 0 (2920 hold, 113 known-broken in baseline), check_seal_currency exit 0, ring drift exit 0, t27c corpus: 0 unresolved, 0 refusals. Refs #11030 (duplicate-bodies already green on master; the t27b-native ratchet stays with its lane)
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.
Closes #8908
Part of the t27b ledger work (see #8326 and #6063). The last five
pass_vacuousrows are stubs with nothing a real test could assert, as #8766 found. They are deleted, as #8054 deleted 22 empty stubs.Cause
specs/lsp/language.t27main()specs/tri/utils/string.t27moduleline and twouselinesspecs/tri/utils/error.t27struct { enum : , }specs/sandbox/modules.t27use sandbox.session_timeout;and anassert trueinvariantspecs/physics/lqg_entropy.t27then true/assert truegit grepfinds nouseof any of the five modules. The other mentions are seals, historical reports, docs, and one dangling dep inarchitecture/graph.tri.Fix
spec_pathmatches).pass_vacuousrows do not count towardmax_not_pass, so the cap does not move.Completeness.leanheld lowerability models of three of them:physics_lqg_entropy,tri_utils_errorandtri_utils_string. Remove the three env/module/theorem triples, and lower the floor ofcorpus_classifier_matches_lean_completenessby 3 (223 -> 220): deletion, not a theorem going quiet, as proofs: drop the Lean models of the 22 spec stubs #8054 deleted (Closes #8222) #8223 did after t27b vacuous: delete 22 empty generated spec stubs (Closes #8052) #8054. None was inlean_completeness_mismatches.json. Hand-written lines: +3 -3.tools/oracle/baseline.tsv(the nightly zig oracle) lists three of them as passing. Drop those lines and lowerpassby 3 (189 -> 186).architecture/graph.trinamessandbox.modulesas a dep ofsandbox.health. There is no such node, andhealth.t27does notuseit, so the dep is dropped.docs/nona-02-organism/physics-kepler/KEPLER-NEWTON-CHERN-SIMONS.md. Its one missing point moves there: CS and LQG give gamma different origins, with its two references. The note's spec list now points atspecs/physics/lqg_cs_bridge.t27, which defines and tests every quantity the stub named (phi^-3, d_tau = phi, the Immirzi gamma).Checks on the t27c lab (master 39d5af3)
cargo test --release -p t27c --test icarus_lowerablet27b corpus specs --jobs 6under qemu, before and after (with the other ledger items, see #8910)own_language.ccheck_budgetexit 0,check_allexit 0; net hand-written lines 0The one
pass_vacuousleft in the corpus,specs/tri/agent/eternal_monitor.t27, has no ledger row, because the reference does not pass it. After this PR the ledger holds nopass_vacuousrow. #8766 is closed with this outcome once this merges.🤖 Generated with Claude Code