The polarity-refined consistency property and paired model (issue #14, Unit 4b)

The sixteen ConsistencyPropertyEqOn fields for the polarity-refined paired family, and the model endpoint the Lyndon argument will consume.

The port is field-for-field with the Craig instance; only the side-bound reasoning changes, and it changes exactly where the audit predicted:

• deterministic and branching fields consume Unit 3's directional rules (sentBndPol_imp_neg_left, sentBndPol_neg_imp_right, sentBndPol_neg_component_*, …) rather than a same-class negation equivalence;
• every right-coordinate case is the left case conjugated by the class-exchanging lyndonInsepAt_swap (through the Unit-4a right twins), never a duplicated proof;
• the mixed C0 cases are lyndonInsepAt_shared_contradiction: a sentence on one side whose negation is on the other lies in the flipped intersection class and is itself a separator;
• the equality fields are class-free, and the cross-coordinate equality/congruence transfers go through lyndonInsepAt_insert_of_shared_constEq_entails, whose swapped-class hypotheses the empty polarity sets of constEq discharge;
• rel_congr moves along sentBndPol_relInst_congr, i.e. the positive-only iff — an atomic instance is in the side class exactly when its symbol is in P;
• the constant rules reuse the unchanged support/freshness machinery verbatim.

This is the first Lyndon file to invoke the countable-completion kernel: exists_henkinComplete and exists_model_of_henkinComplete are consumed exactly as the Craig development consumes them, with no MaximalConsistent machinery — a fact the truth-lemma dependency-cone guard now checks for exists_lyndon_paired_model_neg.

Root inseparability itself is not proved here; that (and interpolation) is Unit 5.

The remaining quantifier round-trip consumers, in signed form

theorem FirstOrder.Language.lyndonInsepAt_insert_congr {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {σ₁ σ₂ : (L.withConstants ℕ).Sentenceω} (hequiv : ∀ (M : Type) [inst : (L.withConstants ℕ).Structure M] [Nonempty M], σ₁.Realize M ↔ σ₂.Realize M) : LyndonInsepAt F P N A (insert σ₁ Γ) Δ ↔ LyndonInsepAt F P N A (insert σ₂ Γ) Δ

Replacing a hypothesis by a semantically equivalent one does not change inseparability (the separator is untouched, so the polarity classes are irrelevant).

theorem FirstOrder.Language.lyndonInsepAt_instConst_of_ex {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (c : ℕ) (ψ : (L.withConstants ℕ).BoundedFormulaω Empty 1) (hcψ : c ∉ sentenceJConsts ψ) (hcΓ : ∀ γ ∈ Γ, c ∉ sentenceJConsts γ) (hcΔ : ∀ δ ∈ Δ, c ∉ sentenceJConsts δ) (h : LyndonInsepAt F P N A (insert ψ.ex Γ) Δ) : LyndonInsepAt F P N (insert c A) (insert (instConst c ψ) Γ) Δ

C7 consumer (existential), signed.

theorem FirstOrder.Language.lyndonInsepAt_not_instConst_of_not_all {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (c : ℕ) (ψ : (L.withConstants ℕ).BoundedFormulaω Empty 1) (hcψ : c ∉ sentenceJConsts ψ.not) (hcΓ : ∀ γ ∈ Γ, c ∉ sentenceJConsts γ) (hcΔ : ∀ δ ∈ Δ, c ∉ sentenceJConsts δ) (h : LyndonInsepAt F P N A (insert ψ.all.not Γ) Δ) : LyndonInsepAt F P N (insert c A) (insert (instConst c ψ.not) Γ) Δ

C7 consumer (negated universal), signed: ¬∀x ψ is ∃x ¬ψ, witnessed by ¬ψ(c).

theorem FirstOrder.Language.lyndonInsepAt_not_instConst_of_not_all_right {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (c : ℕ) (ψ : (L.withConstants ℕ).BoundedFormulaω Empty 1) (hcψ : c ∉ sentenceJConsts ψ.not) (hcΓ : ∀ γ ∈ Γ, c ∉ sentenceJConsts γ) (hcΔ : ∀ δ ∈ Δ, c ∉ sentenceJConsts δ) (h : LyndonInsepAt F P N A Γ (insert ψ.all.not Δ)) : LyndonInsepAt F P N (insert c A) Γ (insert (instConst c ψ.not) Δ)

The right twin of the negated-universal C7 consumer, again by conjugation.

The consistency property

def FirstOrder.Language.lyndonPairedConsistencyProperty {L : Language} (F₁ : Set ((n : ℕ) × L.Functions n)) (P₁ N₁ : Set ((n : ℕ) × L.Relations n)) (F₂ : Set ((n : ℕ) × L.Functions n)) (P₂ N₂ : Set ((n : ℕ) × L.Relations n)) (rL rR : (L.withConstants ℕ).Sentenceω) (hrL : (sentenceJConsts rL).Finite) (hrR : (sentenceJConsts rR).Finite) : ConsistencyPropertyEqOn (GenU rL rR)

Equations

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

The paired model endpoint

theorem FirstOrder.Language.exists_lyndon_paired_model {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (F₁ : Set ((n : ℕ) × L.Functions n)) (P₁ N₁ : Set ((n : ℕ) × L.Relations n)) (F₂ : Set ((n : ℕ) × L.Functions n)) (P₂ N₂ : Set ((n : ℕ) × L.Relations n)) (rL rR : (L.withConstants ℕ).Sentenceω) (hrL : (sentenceJConsts rL).Finite) (hrR : (sentenceJConsts rR).Finite) (hrLsent : rL ∈ SentBndPol F₁ P₁ N₁) (hrRsent : rR ∈ SentBndPol F₂ P₂ N₂) (A₀ : Finset ℕ) (hsupp : sentenceJConsts rL ∪ sentenceJConsts rR ⊆ ↑A₀) (hroot : LyndonInsepAt (F₁ ∩ F₂) (P₁ ∩ N₂) (N₁ ∩ P₂) A₀ {rL} {rR}) : ∃ (M : Type) (x : (L.withConstants ℕ).Structure M) (_ : Nonempty M), rL.Realize M ∧ rR.Realize M

Paired model existence, polarity-refined. From a root pair side-typed at the two polarity classes and inseparable at the flipped intersection class, the fair enumeration produces a Henkin-complete set containing both roots, whose quotient term model realizes them.

theorem FirstOrder.Language.exists_lyndon_paired_model_neg {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (F₁ : Set ((n : ℕ) × L.Functions n)) (P₁ N₁ : Set ((n : ℕ) × L.Relations n)) (F₂ : Set ((n : ℕ) × L.Functions n)) (P₂ N₂ : Set ((n : ℕ) × L.Relations n)) (r₁ r₂ : (L.withConstants ℕ).Sentenceω) (hr₁ : (sentenceJConsts r₁).Finite) (hr₂ : (sentenceJConsts r₂).Finite) (hr₁sent : r₁ ∈ SentBndPol F₁ P₁ N₁) (hr₂sent : BoundedFormulaω.not r₂ ∈ SentBndPol F₂ P₂ N₂) (A₀ : Finset ℕ) (hsupp : sentenceJConsts r₁ ∪ sentenceJConsts (BoundedFormulaω.not r₂) ⊆ ↑A₀) (hroot : LyndonInsepAt (F₁ ∩ F₂) (P₁ ∩ N₂) (N₁ ∩ P₂) A₀ {r₁} {BoundedFormulaω.not r₂}) : ∃ (M : Type) (x : (L.withConstants ℕ).Structure M) (_ : Nonempty M), r₁.Realize M ∧ ¬r₂.Realize M

The Unit-5 consumer endpoint: instantiating the right root at r₂.not gives one model realizing the left root and refuting the (un-negated) right root. Root inseparability is a hypothesis here; establishing it from a failed interpolant is Unit 5's business.