67% of the Lean development is outside the build graph: 647 theorems lake build has never compiled

[gHashTag]

lake build has never compiled the IcarusLowerable proof development. Not "fails on it" — never targets it.

The measurement

proofs/lean4/Trinity.lean is the library root. It imports nine modules:

Trinity.CorePhi          Trinity.TernaryMac
Trinity.ExactIdentities  Trinity.TernaryGemm
Trinity.H4Derivations    Trinity.TernaryInference
Trinity.NeutrinoMasses   Trinity.TernaryFPGABoot
Trinity.H4Lagrangian

Trinity.IcarusLowerable.* is not among them, and nothing else in the root imports it. The eleven files under IcarusLowerable/ import each other — a closed subtree with no edge from the root — so lean_lib «Trinity» never reaches any of it.

	lines	theorems
in the build graph (Trinity/*.lean)	7 447	—
outside it (Trinity/IcarusLowerable/*.lean)	15 447	647

67% of the Lean development has never been compiled by anything.

Including Completeness.lean: 4 986 lines, 250 native_decide theorems.

How this was established

Dispatched lean-proofs.yml at master (it is read-only: checkout plus lean-action, zero write commands) and read the log of the previous run. The word Icarus appears zero times in 481 lines of build output. The modules it names are exactly the nine the root imports.

The two most recent runs before this one both failed, on Trinity/H4Lagrangian.lean:73 and :108 — unsolved goals. That is a real failure in the built part, and it is not why Completeness is unchecked: fixing H4Lagrangian would not add a single IcarusLowerable file to the graph.

What this explains

• A Lean model splits a dotted type into three parameters, and the theorem is true because of it #2893 — a model that splits std.mem.Allocator into three parameters and invents a struct to make its theorem provable. Nothing ever type-checked it.
• Nothing in this repository builds the Lean proofs #2747 / The vacuous ratchet counts 44 of 114 #2890 — 114 of 250 models with functions := []. Nothing ever asked whether the other 136 elaborate.
• The header of lean-proofs.yml already says every by native_decide in the tree is a claim no instrument has checked. This is the mechanism: the claim is not merely unchecked by CI, it is unreachable from the build root.

The repair is one line, and that is the uncomfortable part

Adding import Trinity.IcarusLowerable.Completeness to Trinity.lean puts 647 theorems into the build. It will almost certainly go red — #2893 predicts at least one theorem that cannot hold — and that redness is the point.

I am not making that change here. It converts a green build into a red one on evidence I cannot evaluate locally (lean, lake and elan are not installed on this machine), and the right sequencing — how loud the first run should be, whether to land it behind a separate job — is a decision rather than a measurement.

Refs #2747