[soundness-adjacent] `isFun` unsatisfiable for lambdas over qualified codomain arrows (forallCoBody unguarded)

## Summary

The `@isFun` predicate constraint (`*_cstr` for a function sort) is emitted with its inner `forall` over the **arguments unguarded**, so it says "`f` is a well-typed function iff its codomain qualifier holds for *every* element of the carrier sort", not "…for every element of the *qualified* domain". Combined with the unguarded lambda `def_cstr`s (see #194), `@isFun` becomes **unsatisfiable** for a concrete lambda whose values leave the codomain qualifier off the qualified domain.

This is currently **silent incompleteness** (extensionality / congruence are premised on `@isFun` and become vacuous), with an **unsoundness vector to audit** if any translation path asserts `@isFun` positively.

Relationship to #194: independent. #194 reproduces even where `@isFun` is trivial (see below); the two bugs share the same "unguarded quantifier over a qualified carrier" root cause but neither depends on the other.

## Affected code (main @ `3a141c8`)

- `Blaster/Smt/Translate/Quantifier.lean:761`–`:762` — `forallCoBody ← createPredQualifierAppAux f_applyTerm1 retType (inPredQualifier := true)` then `forallCoDomain := mkForallTerm none co_quantifiers forallCoBody none`. The `co_quantifiers` (the `@x` args) get **no** `@isNat @x =>` premise, in contrast to the extensionality/congruence bodies a few lines below (`:757`) which *are* guarded by `predAppX`.

## Why it is often invisible (important for reproduction)

For a `Nat → Bool` arrow the codomain qualifier is `@isBool`, which Blaster defines as trivially true:

```
(define-fun @isBool ((@x0 Bool)) Bool true)
```

So for Bool-codomain lambdas `@isFun` is trivially satisfiable and the bug shows nothing. It only bites when the codomain qualifier is non-trivial — e.g. `Nat → Nat`, where the codomain qualifier is `@isNat` (`(<= 0 x)`). A maintainer testing with a Bool-codomain lambda will see no problem and could wrongly close this.

## Decisive SMT evidence (`Nat → Nat`, hand-reduced from Blaster's emission pattern)

`@isFun_cstr` with the inner `forall` **unguarded** (as emitted), plus a `def_cstr` for `fun x : Nat => x + 1`:

```
(assert (forall ((f ArrowNN)) (= (forall ((x0 Nat)) (isNat (app f x0))) (isFun f))))
(assert (forall ((y Nat)) (= (app L y) (+ 1 y)))) ; def_cstr, unguarded
```

`isFun L` unfolds to `∀ x0:Int. app(L,x0) ≥ 0`, i.e. `∀ x0. x0 + 1 ≥ 0`, which is false at `x0 = -2`. Hence:

```
$ z3 min_isfun_a.smt2 # adds (assert (isFun L))
unsat
$ z3 min_isfun_b.smt2 # adds (assert (not (isFun L)))
sat
```

So `@isFun L` is unsatisfiable for this lambda. Every extensionality/congruence axiom guarded by `@isFun @f` becomes vacuous for it — incompleteness.

## Unsoundness vector (to audit, not yet demonstrated)

In the queries observed, `@isFun` appears only as an **antecedent** (`ext_fun`, `congr_ext_fun`, `congr_args` are `(=> (@isFun @f) …)`) — the safe direction. `createPredQualifierAppAux'` (`Quantifier.lean:573`) *does* produce `@isFun st` for arrow-typed binders, so the open question is whether any caller emits it **positively** (a standalone `assert`, or a positive conjunct — e.g. an existential over an arrow type, or a structure invariant field of function type) rather than as a premise. If such a path exists, an unsatisfiable `@isFun` on a lambda could make a negated goal vacuously `unsat` → spurious `Valid` (a soundness bug). I did not find such a path; filing this as incompleteness with an unsoundness vector to audit.

## Fix direction

Same as #194: guard the `co_quantifiers` of the `@isFun` constraint at `Quantifier.lean:761`–`:762` with the domain qualifier premises (reuse the `predAppX`/`impliesSmt` discipline already present at `:751`–`:757`). Guarding `def_cstr` (#194) also removes the concrete-lambda trigger.

## Environment

- input-output-hk/Lean-blaster `main` @ `3a141c8`; Lean `v4.24.0`; Z3 4.15.2

## Severity

Soundness-adjacent — today a silent incompleteness; potential unsoundness pending the positive-assertion audit above.

## Polymorphic false Valid persists after PRs #198 and #199, 9 September 2026

The restriction in #199 that omits domain guards for polymorphic arguments is still unsound, not only incomplete. Reproduced on latest beta with both existing fixes adapted and combined:

```lean
import Blaster
example : ¬ (∀ α : Type, ∀ f : α → α, (∀ x, f x = x) → ∃ _ : α, True) := by
intro h
obtain ⟨x, _⟩ := h Empty id (fun x => Empty.elim x)
exact Empty.elim x
#blaster (gen-cex: 0) (solve-result: 1) (timeout: 5)
[∀ α : Type, ∀ f : α → α, (∀ x, f x = x) → ∃ _ : α, True]
```

Actual: `Unexpected Valid`. The kernel proof refutes the proposition with `α := Empty` and `f := id`. The unguarded `isFun` constraint forces a member of α from any well-typed α → α function, although such functions exist for empty α. The predicate declaration and every application need all domain generics in scope so the domain guard can be emitted consistently.

## Guarded iff is insufficient for empty domains

Merely adding the skipped generic guards to the existing membership iff is still unsound. Function instances share an SMT arrow carrier. On an empty domain, the behavioral side of that iff is vacuously true for every carrier value; extensionality then collapses function values belonging to other domain types as well.

This kernel-checked counterexample was reported `Unexpected Valid` by that intermediate encoding. The proposed completion uses forward typing contracts and explicit typing of introduced functions; it reports `Falsified`:

```lean
import Blaster
example : ¬ (∀ α β : Type, ∀ _b : β, ∀ g : (β → Nat) → Nat,
(∀ _ : α, False) → g (fun _ => 0) ≠ g (fun _ => 1) → False) := by
intro h
exact h Empty Unit () (fun f => f ()) (fun x => Empty.elim x) (by decide)
#blaster (gen-cex: 0) (solve-result: 1) (timeout: 5)
[∀ α β : Type, ∀ _b : β, ∀ g : (β → Nat) → Nat,
(∀ _ : α, False) → g (fun _ => 0) ≠ g (fun _ => 1) → False]
```

The expanded `Issue195.lean` regression module passes on the completion candidate. Integration remains a draft because stricter typing introduces timeouts in older recursive-function tests; their expectations have not been weakened.