zeekayandHanzo Dev 95870aa61d lean: report what each theorem rests on, and namespace the colliding pair ...

lean/axioms.py runs `#print axioms` over every theorem in the corpus. A green
build says each proof follows from what it was given; only this says what that
was. Lean's own propext, Classical.choice and Quot.sound are the ambient logic
and are not assumptions about our systems, so a theorem resting on those alone
is proved and anything else it names is load-bearing.

Measured here: 715 theorems queried, 594 proved outright, 121 resting on
axioms. It also ranks the axioms by how many theorems stand on them, which is
where the corpus's weight actually sits — Crypto.NonCustodial.sign carries 15,
and the four Quasar hardness axioms carry 7 each.

Building it surfaced a defect no per-file build could: `Vault.KeyIsolation` and
`Crypto.DEKDerivation` both declared `deriveOrgKEK` at top level, with no
namespace in either, so importing both failed and the corpus could not be
loaded as a whole. They were the only two files in 115 without a namespace, and
nothing imports either. Both now have one.

Modules in no library have no .olean, so importing one aborts the query. Those
are exactly the modules nothing checks; they are named and counted, not
imported.

vacuity.py caught one shape and now catches four, which took it from 55 to 75:

  - `... True`, as before
  - `∃ x, e = x`, closed by `⟨_, rfl⟩` — the witness is whatever the other side
    evaluates to, so the equation says only that it has a value
  - a conclusion that is one of its own hypotheses, `P → P`
  - `sorry` and `admit`, over comment-stripped source

And the claim of a `def` is its body, not the part before `:=`. Cutting at `:=`
for every kind is what let `TSUFBound : Prop := ∃ _a, True` read as content —
along with `MagnetarTSUFBound`, `corona_eufcma_to_mlwe`, and both
`NoLeakReduction`, all now reported.

Co-authored-by: Hanzo Dev <[email protected]>

2026-07-29 11:39:31 -07:00

..

KeyIsolation.lean

lean: report what each theorem rests on, and namespace the colliding pair

2026-07-29 11:39:31 -07:00