bend.ts accepts books the Lean kernel refuses: base-file live calls to later-filled laws, and non-Tree bodies

Summary

bend.ts accepts books whose semantics fall outside the fragment bend.lean states as Book.Ok — i.e. the implementation is strictly weaker than the mechanized core in two concrete, code-level ways. Neither is currently exploitable from a user file, but both are silent spec/implementation drift in the places the header claims are enforced ("mutual recursion cannot bypass the wall").

1. Base-file live calls to later-filled laws bypass the descent wall

infer-ref (bend.ts:~3292-3296) skips the "an unfilled law is a dead claim (live code cannot use it)" error whenever tld.b === true — a flag book_load sets for every base.bend tld. Shipped base.bend uses it: Word.adc.con (base.bend:1151) live-calls Word.adc, whose law is declared at 1143 and filled at 1156 — a forward live call, i.e. genuine mutual recursion whose descent the wall never tests. bend.lean's corresponding rule demands (q != .None -> j <= L.k) and rejects exactly this; its header even flags "that pair is mutual recursion the checker never tests ... The theory has no such call."

2. Def bodies are not required to be Trees

Lean's Book.Ok requires Tree beta d.n d.body (bend.lean:991) — the case-tree-over-columns invariant that check-mat's column-peel soundness rests on. book_valid (bend.ts:~3699-3712) checks bodies with term_check alone and never verifies Tree shape; e.g. a body that partially applies via check-any with zero columns bound checks fine in bend.ts while failing Tree. Benign for termination (fewer bound columns only tightens the descent scan), but it means the "model inclusion" claim does not hold for books bend.ts accepts.

Suggested direction

Restrict the b === true carve-out to demand-None (keep the live unfilled-law error for base too) and reorder base.bend's helpers, or thread a helper-self-recursion rule through the Lean model; record a Tree-shape bit at parse time so book_valid enforces what Book.Ok assumes.

Version / system

• bend 2.0.5 (main @ e6676b0); reading-level finding against bend.ts/bend.lean/base.bend, no user-file trigger (the carve-out is set only for BASE_BEND).