Paired inseparability: the cross-coordinate gates (issue #8, commit 4c — risky core)

Commits 4a/4b built a one-sided consistency family (InsepFamilyMem: only the Γ coordinate, with Δ fixed externally). That completes only the Γ-side: the Henkin limit S* contains r₁ but nothing forces r₂, so the truth lemma yields M ⊨ r₁ with no handle on r₂. The Craig contradiction needs one model of both sides at once.

This file restores the audit's paired finite conditions S = Γ ∪ Δ (docs/craig-audit.md §4, §7): Γ ⊆ Sent₁, Δ ⊆ Sent₂ over the two side vocabularies, inseparable at the shared vocabulary (F₀, R₀). The one-sided closures of InseparablePairFamily.lean remain the left-coordinate engine; the right coordinate is obtained by the swap below, and the genuinely new content is the three cross-coordinate gates the audit flagged as load-bearing.

The gates (all proved here)

• insepAt_swap — dualization: inseparability is symmetric under (Γ, Δ) ↦ (Δ, Γ) with σ ↦ σ.not. This turns every left-coordinate closure into its right-coordinate twin.
• insepAt_shared_contradiction — cross-coordinate contradiction ⟹ shared separator: a shared sentence φ with Γ ⊨ φ and Δ ⊨ φ.not (support in A) is a separator, so it cannot occur; this is the global C0 for the union (the case φ ∈ Γ, φ.not ∈ Δ). A φ occurring on both sides is automatically shared: φ ∈ Sent₁ and φ.not ∈ Sent₂ force φ's base symbols into F₁ ∩ F₂ = F₀.
• insepAt_insert_of_shared_entails — shared-hypothesis transfer: if σ is shared and Δ ⊨ σ, and φ is a consequence of Γ ∪ {σ}, then φ may be added to the Γ coordinate. A separator ρ of the enlarged pair yields the shared separator σ.imp ρ. This single lemma discharges both the plain shared-equality transfer and the cross-coordinate relation congruence (σ = constEq (g i) b ∈ Δ, φ = relInst R (Function.update g i b), a consequence of relInst R g ∈ Γ together with σ).

The full paired family (Sent₁/Sent₂ predicates, PairedInsepFamilyMem, the right-coordinate closures, the ConsistencyPropertyEqOn instance over the union, and the {r₁, r₂} Henkin endpoint yielding M ⊨ r₁ ∧ ¬ M ⊨ r₂) is assembled on top of these gates in the next tranche.

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

Swap (dualization). Inseparability is symmetric under (Γ, Δ) ↦ (Δ, Γ) with σ ↦ σ.not: a separator σ of (Δ, Γ) gives the separator σ.not of (Γ, Δ) (double negation on the Δ side). Applied to swapped arguments this is an iff; every left-coordinate closure becomes a right-coordinate one through it.

theorem FirstOrder.Language.insepAt_shared_contradiction {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φ : (L.withConstants ℕ).Sentenceω} (hφF : BoundedFormulaω.baseFunctionsIn φ ⊆ F) (hφR : BoundedFormulaω.baseRelationsIn φ ⊆ R) (hφA : sentenceJConsts φ ⊆ ↑A) (hΓφ : Theoryω.Entails Γ φ) (hΔφ : Theoryω.Entails Δ (BoundedFormulaω.not φ)) (h : InsepAt F R A Γ Δ) : False

Gate (a): cross-coordinate contradiction gives a shared separator. A shared sentence φ entailed by Γ and refuted on Δ (base symbols in (F, R), support in A) is itself a separator, so it is incompatible with inseparability. This is the union-level C0 for the mixed case φ ∈ Γ, φ.not ∈ Δ.

theorem FirstOrder.Language.insepAt_insert_of_shared_entails {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {σ φ : (L.withConstants ℕ).Sentenceω} (hσF : BoundedFormulaω.baseFunctionsIn σ ⊆ F) (hσR : BoundedFormulaω.baseRelationsIn σ ⊆ R) (hσA : sentenceJConsts σ ⊆ ↑A) (hΔσ : Theoryω.Entails Δ σ) (hcons : (insert σ Γ).Entails φ) (h : InsepAt F R A Γ Δ) : InsepAt F R A (insert φ Γ) Δ

Gates (b) and (c): shared-hypothesis transfer. If σ is shared (base symbols in (F, R), support in A) and entailed by Δ, and φ is a consequence of Γ ∪ {σ}, then φ may be added to the Γ coordinate without breaking inseparability. A separator ρ of the enlarged pair yields the shared separator σ.imp ρ. Instantiating φ := σ gives the plain shared-formula transfer (gate b); instantiating σ := constEq (g i) b ∈ Δ, φ := relInst R (Function.update g i b) (a consequence of relInst R g ∈ Γ and σ) gives the cross-coordinate relation congruence (gate c).

The allowed-support budget: variance and fresh growth

The paired family carries the invariant support Γ ∪ support Δ ⊆ ↑A — A is an allowed-support budget, not an exact support. Shrinking the budget is free; growing it by a fresh constant (supplied by the invariant whenever c ∉ A) is the one non-trivial move, and it is exactly constant abstraction.

theorem FirstOrder.Language.insepAt_mono_support {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {B : Finset ℕ} (hAB : A ⊆ B) (h : InsepAt F R B Γ Δ) : InsepAt F R A Γ Δ

Variance (shrink the budget). A smaller allowed support makes inseparability easier: every separator allowed at A is allowed at B ⊇ A.

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

Fresh growth. Enlarging the allowed-support budget by a constant c fresh for Δ preserves inseparability: a separator using c abstracts to genEx c σ, whose support lies back in A. Only the Δ-side (∀-generalization) needs the freshness; the Γ-side is ∃-weakening. Under the family invariant, c ∉ A already gives c ∉ support Δ.