fix(bendtt): distinguish free variables in diagnostics

[vicmcorrea]

Problem and fix

Term.show prints every free index as x0 because natural-number subtraction saturates. For example, Ctx.fit (Book.of []) [] (Var 1) (Var 0) reports expected: x0 / observed: x0 even though the terms differ.

Preserve bound-variable names and print free[i - d] when index i is outside depth d. This isolates the diagnostic portion of #1448, following the maintainer's separate-scope guidance.

Blast radius

Only the Var branch of Term.show in bend2/bendtt.lean changes (+3/-1). The change affects printing open terms; parser/checker logic, reduction, claims and proofs are untouched. The default --verdict kernel cache uses a new source key.

Regression evidence

Two native Lean harnesses use the actual source's THEORY section and its existing Ctx.fit/Term.check consumers. The baseline fails the diagnostic guards; this change passes them. The example above now reports expected: free[0] / observed: free[1].

Controls cover distinct free indices, depth-relative shifts, nested binders and rewrite motives. Bound names, successful closed checks and the direct unbound variable error remain unchanged.

Checks

• Full lean bend2/bendtt.lean with Lean 4.34.0: passes.
• Native baseline/updated harnesses: updated versions pass all 13 and 9 controls respectively; baseline versions fail the intended diagnostic guards.
• Repository gate: 54/54; git diff --check passes.

Validation limits

The reproduction constructs malformed open terms through the Lean API. Ordinary parsed .bend/.bendtt CLI reachability has not been established; this is a diagnostic cleanup, not a soundness fix. The native harnesses are private validation, not a new tracked test suite. Checks ran on macOS arm64; full cluster, GPU, performance gates and a full native-kernel CLI corpus were not run.