Support-parameterized inseparability and the C7 closure step (issue #8 kernel gate)

InsepAt F R A Γ Δ: the pair (Γ, Δ) of L[[ℕ]]-sentence sets admits no separator σ whose base symbols lie in (F, R) (the shared vocabulary), whose constant support lies in the finite allowed set A, with Γ ⊨ σ and Δ ⊨ ¬σ. Parameterizing by the allowed support A is what makes the quantifier (C7) closure step compositional and the root case (A = ∅) reachable (docs/craig-audit.md §7).

This file is the kernel gate (audit §6a.6): it certifies that the constant-abstraction machinery composes into the exact C7 closure argument — a separator of the witness-instantiated pair at support insert c A abstracts, via the acceptance lemmas, to a separator of the existential pair at support A. The full inseparability consistency-property instance and the Henkin model existence belong to tranche 2.

def FirstOrder.Language.InsepAt {L : Language} (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) (A : Finset ℕ) (Γ Δ : Set (L.withConstants ℕ).Sentenceω) : Prop

Support-parameterized inseparability: no separator with base symbols in (F, R), constant support in A, entailed by Γ and refuted on Δ.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.insepAt_witness_of_insepAt_genEx {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (c : ℕ) (φc : (L.withConstants ℕ).Sentenceω) (hcΓ : ∀ γ ∈ Γ, c ∉ sentenceJConsts γ) (hcΔ : ∀ δ ∈ Δ, c ∉ sentenceJConsts δ) (h : InsepAt F R A (insert (genEx c φc) Γ) Δ) : InsepAt F R (insert c A) (insert φc Γ) Δ

The C7 closure step (separator abstraction): if the existential pair is inseparable at support A, then the witness-instantiated pair is inseparable at support insert c A, for a constant c fresh for both sides. This is the contrapositive of the acceptance pair: a separator of (Γ ∪ {φ(c)}, Δ) at insert c A abstracts to the separator genEx c σ of (Γ ∪ {∃x φ}, Δ) at A.