[ScottMoore0]

Opened after Nico's go-ahead on Discord.

Claim.consistent says no checked def has type <>. This adds the claim a law's user relies on: a checked proof of {a == b} means a and b convert. It holds for any closed, live term, so a checked law holds at each closed instance (its proof def applied to closed values), in the kernel's own reduction (opaque defs at their models, as in Part 2).

def Claim.adequate : Prop :=
  ∀ bk t T a b A, Book.check bk = .ok () → Term.Closed t → Term.Live bk t →
    Typed bk [] t T → Conv bk T (Eql a b A) → Conv bk a b

The proof is adequate, after consistent. It reuses halts, progress, pars_sr, value_form, gen and fits_conv, plus two small lemmas after canon_enu: eql_inj (the sides of convertible equations convert) and canon_eql (a closed value at an equation is {==}). It changes no line that Book.check or main runs.

What I ran on this exact file (identical to main at 22d627b plus this patch; bendtt.lean is unchanged since 234cb9b, where I ran these):

Check	Result
lake build (Lean 4.34.0)	builds
#print axioms on all 10 theorems, Book.check, main	propext, Classical.choice, Quot.sound only
leanchecker --fresh	passes
Lean4Lean --fresh (its 4.33.0-rc2 toolchain)	93,251 declarations checked
lean -c + leanc -O3 -DNDEBUG kernel binary	byte-identical to main's
tests/ + demos/*/PROOF.bend (1,666 files) through --verdict	same verdict and output text for every file
Size (ttok==0.3, which matches CI)	62,092 → 62,676 of the 64,000 cap

Happy to shorten it, rename, or restate it in the file's style.

Found and tested with Claude Code, running Claude Opus 5.5, during an audit of --verdict.