tri lean: proofs that nothing compiles
12 Lean files, 15,553 lines and 4 sorry, are reached by no build root: nothing compiles them.
t27 · tri lean
t27 $ tri lean reach
BUILD-GRAPH REACHABILITY (~/t27/.claude/worktrees/gif-animation-reposts-5eb60f/proofs/lean4/Trinity.lea
n)
files lines sorry
reached by the root 11 7651 1
NOT reached 12 15553 4
Stranded -- present, shaped like proofs, compiled by nothing:
Trinity.GoldenFloatRoundTrip 105 lines 3 sorry
Trinity.IcarusLowerable.Ast 90 lines
Trinity.IcarusLowerable.AstInduction 130 lines
Trinity.IcarusLowerable.Completeness 4986 lines
Trinity.IcarusLowerable.Emitter 221 lines
Trinity.IcarusLowerable.Equivalence 2875 lines 1 sorry
Trinity.IcarusLowerable.Lemmas 3444 lines
Trinity.IcarusLowerable.Predicate 1005 lines
Trinity.IcarusLowerable.Semantics 389 lines
Trinity.IcarusLowerable.SemanticsTotal 546 lines
Trinity.IcarusLowerable.Soundness 1641 lines
Trinity.IcarusLowerable.Verilog 121 lines
`lake build` prints what it compiled and never what it skipped, so these produce
no output at all -- not an error, not a warning. A build graph is a claim about
coverage that nothing prints, and the root file is the whole of the claim.
4 of the 5 admitted proofs counted by `lean-proofs.yml` are in these files.
That gate greps the directory; the build compiles the closure. Its comment says
a `sorry` compiles -- for these it does not, because nothing compiles them.
t27 $ recorded 2026-10-03 16:18 UTC real 4.7 s shown 4.7 s exit codes 0 0
$ tri lean vacuous
$ tri lean reach
Staged: the prompt and the typing. Real: every byte the commands printed, at the time they printed it. Any silence longer than 2 s is shown for 2 s, and the title bar says so while it happens. Edited: home directory shown as ~.
Trinity S³AI
