A term η-expanded under a new λ keeps its annotations on its own binders, so --verdict checks what bend2 checks (#1665)

[aaaxn]

Fixes #1665.

Cause

bend2 wraps each node it checks in its type, as a cell (Infer and Check in bend.ts), and term_higher keeps a cell as it is. So a binder inside a def's body is a closure, but an annotation names it by the level bend2 checked it at. eta in safe.ts makes a term of a function type η-long, λy => t(y), and y takes the level t was checked at. Each binder inside t lands one level deeper, and the annotations that name it don't move. In the issue's file, the λ-match under n keeps {x1 == x1 : Nat} while n is now x2 and x1 is y : Bool, so the kernel rejects a program bend2 accepts.

eta has three callers, and each one hits this: arg_term (an argument, the issue's case), a leaf in tree (a def's body or a match arm), and a default arm in swi.

Fix

• eta takes the depth t is at and puts t under the λ through its lowered form, with subst, the way model_at builds a λ around a body it found once. Lowered, an annotation names t's binders as t's own uses do, so under the λ they move together.
• The three callers pass s.d.
• subst now keeps a variable from outside t (below the depth) at its level, instead of each caller mapping it back. closed_val and model_at did that by hand; they now leave it to subst. This keeps safe.ts under its ttok cap.

The issue's term now goes out as the hand-written η-long one in the report, byte for byte.

Checks

On HEAD (main e5527d5b), Linux x86_64, kernel built from that bendtt.lean with Lean 4.34.0:

• tests/check/eta_levels.bend covers the four places a term goes η-long: an argument (arg), a def's body (leaf), a match arm (arm) and a default arm (rest). Each one fails --verdict on main when it is on its own. A law pins main at 10n. The file prints 10n when run and from the JS and C builds, and --checkup exits 0.
• Mutations: putting back the old eta in arg_term, at the leaf in tree or at the default arm each makes the test fail, at the defs that path builds (arg; leaf and arm; rest). Dropping subst's default for outer variables (they come back as Refs), or putting t under the λ at depth d + 1 or d - 1, fails all four.
• --verdict on the other 1,733 test, demo and bench files gives the same exit code and output as main: 1,114 check, 619 fail.
• -o is byte-identical to main for the 1,226 of those files that emit one; the other 507 fail -o on both, with the same message. eta runs 37,201 times over 743 of them, 10,194 times on a term with a binder inside (308 files). 577 of those terms hold bare redexes (601 in all), which raising reduces. All 601 sit inside a type.
• --verdict output and -o on all 1,734 files are byte-identical to this PR's first commit (742429e3).
• A differential sweep over 432 generated programs varied where the term goes η-long, the parameters before it (0 to 2), the quantity of the η binder and of the inner binder, and the inner λs (n => .. naming n, n => m => .. naming n or m, or no λ-match). bend2 accepts all 432. The 108 without a λ-match check on both. The 324 with one fail on main and check here. None checks on main and fails here.
• Timing: interleaving main and this branch five times each with -o on proofs_3200, generics_3200, defs_12800, trees_400 and app_slash_boss_3d's PROOF.bend, the medians are within 2% of main.
• With PR fix(safe): preserve neutral function fields in constructors #1657 on top, both patches apply cleanly, and eta_levels, constructor_function_reuse and the repro in --verdict rejects a reused proof after reconstructing a constructor with a function field #1623 all check.
• bun gates/repo.ts with ttok==0.3, as CI runs it: 54 / 54. safe.ts goes from 23,986 to 23,987 ttok, under its 24,000 cap.
• tsc: 11 errors, the same as main.
• I didn't run the cluster gates. The --verdict and -o runs above were local, one bend <f> --verdict per file as gates/safe_node.ts runs it.

Limits

rebuild also builds a λ's body under binders bend2 didn't check it at, and it has the same bug (#1669). No test, demo or bench file reaches it. #1670 fixes it on top of this PR, with the same subst.