fix(verdict): lift Data captures in type-only templates

[oxura]

Problem

least(lo, xs) from #1483 checks in Bend, but its type-only List.all(~…, ~(y => Nat.is_le(lo, y)), xs) is dropped by the BendTT translator because the template lambda captures lo. Consequently even the universally valid least_nil(lo) fails --verdict.

Fixes #1483.

Change

• Close template arguments over private, typed capture references instead of rejecting a run-time Data capture in a type.
• Lift those captures into explicit kernel parameters. Apply the actual caller's values at every specialized call, including recursive calls; never replace a capture with an opaque global constant or a chosen model value.
• Keep dependencies before dependent capture types, carry their bindings through scope moves, and retain the same capture-prefix contract for the existing mutual-recursion selector representation.
• Leave closed specializations on their existing path: no capture map is allocated for ordinary scopes or copied for a closed call; skip capture traversal when the pass has none.
• Add a semantic proof regression for a universal empty-list result, true and false nonempty bounds, two distinct captures, source-variable-level changes and a captured Data record. Update the existing template-limit documentation.

No edit to bend.ts, bendtt.lean, gates, allow list or token caps. The existing live-code rule still rejects template arguments that depend on run-time variables.

Evidence

Actual unchanged native BendTT kernel, byte-identical to the current-main Lean source; Bun 1.3.13 on Linux x64.

• Issue reproducer on main: --check-only exits 0; --verdict exits 1; emitted module omits least and least_nil as out of scope.
• This branch: source CLI --verdict exits 0 and emits both definitions without out-of-scope omissions.
• Final permanent regression fails on main and passes here: 7 genuine proof obligations, including 2 <= 1 yielding False and separate lower/upper captures rather than only vacuous empty-list checks.
• Real compiled/installed CLI also validates that regression, exit 0.
• Actual emitted captured predicate checked directly by the real kernel: lower bound 0 with [0] validates; lower bound 1 with [0] is rejected, exit 1. This checks preservation of the captured argument, not merely successful elaboration.
• Neighboring template_law, fold_assoc, model_lambdas and model_order retain successful actual kernel verdicts before/after.
• Repository gate 54/54, unchanged permanent caps.

Limits

Mini-cluster/GPU were not run. This does not solve the separate opaque higher-order-template problem #1182, and no full bend-mathlib verdict is claimed. Non-Data captures are not made duplicable: the unchanged kernel remains authoritative for their quantity/type admissibility. The standard output-only gate is not claimed to run the proof kernel; the actual before/after --verdict runs above are the kernel regression evidence.