[oxura]

Problem

The original reproducer in #1182 defines a closed injectivity proof (inj), but the opaque use~F still has no model. Constructor, reflexivity, and projection models cannot construct that proof themselves.

This implements the checked-definition lookup direction requested in #1263 (comment). It does not restore the rejected backtracking implementation.

Change

• Preserve the existing model builders and their precedence.
• If those builders fail, look through the checked book for a definition with a body, no template parameters, no @unsafe marker, and a definitionally equal type.
• Use a reference to that definition as the model. It remains an ordinary emitted dependency: the native BendTT kernel checks its body, rather than trusting its signature.
• Add a proof regression whose witness is declared after the generic root and whose main actually calls use(~inj, ...) to return an equality proof.
• Document the witness requirement in the BendTT paper. No parser/checker, kernel, gate, or cap changes.

Verification

• The unchanged public higher_evidence_base.bend reproducer passes both --check-only and --verdict with the canonical Lean 4.34.0 BendTT kernel.
• The new forward-witness regression fails --verdict on untouched main (8578b7cb, no model for use~F) and passes with this change. Running it prints {==}.
• Baseline/treatment comparison across all 94 existing tests/proof/*.bend files: identical frontend classifications, out-of-scope reports, native-kernel results, and export hashes. All 61 previously emitted books are byte-identical. The new fixture adds one complete kernel certificate: 59 existing certificates become 60, with no existing outcome changed.
• model_false.bend and model_no_base.bend remain outside the translation's scope.
• bun gates/repo.ts: PASS: 54 / 54, including the staged new fixture and the unchanged 24k safe.ts cap.
• The edited BendTT paper builds with Typst.
• TypeScript 5.9.3 full-project checking is not green: untouched main and this branch both produce the same 12 diagnostics, ignoring shifted source locations. No new diagnostics; no suppression or unrelated repair.

Scope and limits

This fixes the original reported case where the book contains a closed witness. It is not a general proof-search or mutually dependent model-selection change.

The public law_higher_evidence_probe.bend has no closed witness and still reports no model for use~F. The public dependent_empty_result_probe.bend also remains rejected; its opaque function would have to return an empty value at Z. Both were exercised explicitly, not treated as complete certificates merely because a partial book can be exported.

The separate v_n / bend-mathlib model-choice case from the issue comments is not claimed fixed. This PR intentionally does not auto-close that broader issue thread.

The proof comparison ran locally against the actual native kernel, not on the mini-cluster. The cluster gates were unavailable in the preceding qualification because the bastion hostname did not resolve; no gate was bypassed.

[nicolas-abril]

Thanks @oxura. The diagnosis is right, and this is the lookup suggested in #1263, but we're closing it in favor of #1580.

A ~ constant's model only shows that its type is inhabited. The constant stays opaque, and the kernel checks the model, so any model is sound. Where the model comes from is the problem:

• It's non-local. Whether use is certified depends on some def anywhere in the book (Base included) having a definitionally equal type. If inj is renamed or deleted, takes its arguments in a different order, or gains a ~ parameter, use falls back out of scope. It also takes the first match, so a matching def that is itself out of scope takes use with it.
• It's premise selection. It chooses a term from the book by type. The natural follow-ups (instantiate a lemma, partially apply it, combine two) are steps toward proof search, the same slope The ~ constants of a root take models that hold together, so a ~ law of a ~ function reaches the kernel (#1182) #1263 went down. Finding an inhabitant of an arbitrary type is theorem proving: there is no last rule, and safe.ts shouldn't be a solver. It should translate the program's own terms.

#1580 takes the model from the template's instances instead. main calls use(~inj, …), bend2 records that call (book.tmps), and bend2 has already checked inj at F's type. So use~F := inj, with no search or type matching, and use is still checked at an opaque F. One call supplies all of a root's constants, so they fit together. Your forward-witness test passes there in substance; it's included, with a two-constant case.

#1182's literal repro, which never calls use, stays out of scope under #1580. That's deliberate: nothing in the program says which term stands for F.

[oxura]

Understood. I will not reopen the book-wide witness lookup or try to make the literal no-call repro pass. Taking models from the template instances in #1580 keeps the source of the model explicit.

AI-assisted; no subagents.