The polarity-refined paired family and its cross gates (issue #14, Unit 4a)

The first genuinely paired layer of the Lyndon refinement. A family member is a support-budgeted, GenU-bounded, side-typed pair carrying the refined inseparability at the flipped intersection class:

Γ ⊆ SentBndPol F₁ P₁ N₁        Δ ⊆ SentBndPol F₂ P₂ N₂
LyndonInsepAt (F₁ ∩ F₂) (P₁ ∩ N₂) (N₁ ∩ P₂) A Γ Δ

The flip on the Δ coordinate is the audit's §D4a orientation, and it is what makes the mixed C0 gate go through: a sentence φ occurring on the left with φ.not on the right satisfies

Pos φ ⊆ P₁  and  Pos φ ⊆ N₂          Neg φ ⊆ N₁  and  Neg φ ⊆ P₂

— the first pair because φ ∈ SentBndPol F₁ P₁ N₁, the second because φ.not ∈ SentBndPol F₂ P₂ N₂ exchanges the components (sentBndPol_not_iff). So φ lies in the maintained separator class and is itself a separator: the configuration cannot occur. That calculation is sentBndPol_flip_inter, stated on its own so the orientation is checkable in isolation.

Right-coordinate gates are never duplicated: each is the left gate conjugated by lyndonInsepAt_swap, which exchanges (P, N). The unsigned support/freshness bookkeeping (support_mem_*, support_insert_*, fresh_*) is reused verbatim from the Craig engine — it carries no polarity content.

Unit 4b adds the sixteen consistency-property fields, the Henkin completion, and the model endpoint.

The mixed-C0 class calculation

theorem FirstOrder.Language.sentBndPol_flip_inter {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {P₁ N₁ P₂ N₂ : Set ((n : ℕ) × L.Relations n)} {φ : (L.withConstants ℕ).Sentenceω} (h₁ : φ ∈ SentBndPol F₁ P₁ N₁) (h₂ : BoundedFormulaω.not φ ∈ SentBndPol F₂ P₂ N₂) : φ ∈ SentBndPol (F₁ ∩ F₂) (P₁ ∩ N₂) (N₁ ∩ P₂)

The flipped intersection calculation (mixed C0, audit §D4a). A sentence bounded on the left, whose negation is bounded on the right, lies in the maintained separator class:

• Pos φ ⊆ P₁ (left bound) and Pos φ ⊆ N₂ (right bound, after the negation exchange);
• Neg φ ⊆ N₁ (left bound) and Neg φ ⊆ P₂ (right bound, after the exchange).

theorem FirstOrder.Language.lyndonInsepAt_shared_contradiction {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {P₁ N₁ P₂ N₂ : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φ : (L.withConstants ℕ).Sentenceω} (hφ₁ : φ ∈ SentBndPol F₁ P₁ N₁) (hφ₂ : BoundedFormulaω.not φ ∈ SentBndPol F₂ P₂ N₂) (hφA : sentenceJConsts φ ⊆ ↑A) (hΓφ : Theoryω.Entails Γ φ) (hΔφ : Theoryω.Entails Δ (BoundedFormulaω.not φ)) (h : LyndonInsepAt (F₁ ∩ F₂) (P₁ ∩ N₂) (N₁ ∩ P₂) A Γ Δ) : False

Mixed C0: a sentence entailed on the left whose negation is entailed on the right is a separator in the flipped intersection class, so it cannot occur under inseparability.

Right-coordinate gates, by conjugation with lyndonInsepAt_swap

theorem FirstOrder.Language.lyndonInsepAt_insert_right_of_entails {L : Language} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {φ : (L.withConstants ℕ).Sentenceω} (hcons : Theoryω.Entails Δ φ) (h : LyndonInsepAt F P N A Γ Δ) : LyndonInsepAt F P N A Γ (insert φ Δ)

Grow the Δ-coordinate by an entailed sentence — the right twin of lyndonInsepAt_insert_of_entails, obtained purely by conjugation with the class-exchanging swap.

theorem FirstOrder.Language.lyndonInsepAt_insert_right_of_shared_constEq_entails {L : Language} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {φ : (L.withConstants ℕ).Sentenceω} (a b : ℕ) (hσA : sentenceJConsts (constEq a b) ⊆ ↑A) (hΓσ : Theoryω.Entails Γ (constEq a b)) (hcons : (insert (constEq a b) Δ).Entails φ) (h : LyndonInsepAt F P N A Γ Δ) : LyndonInsepAt F P N A Γ (insert φ Δ)

The right twin of the equality-transfer gate: a shared constant equality entailed by Γ transfers a consequence into the Δ coordinate. Again pure conjugation — the (P, N) exchange happens twice and cancels.

theorem FirstOrder.Language.lyndonInsepAt_iSup_component_right {L : Language} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} (φs : ℕ → (L.withConstants ℕ).Sentenceω) (hmem : BoundedFormulaω.iSup φs ∈ Δ) (h : LyndonInsepAt F P N A Γ Δ) : ∃ (k : ℕ), LyndonInsepAt F P N A Γ (insert (φs k) Δ)

The right twin of the iSup component selection.

theorem FirstOrder.Language.lyndonInsepAt_neg_iInf_component_right {L : Language} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} (φs : ℕ → (L.withConstants ℕ).Sentenceω) (hmem : (BoundedFormulaω.iInf φs).not ∈ Δ) (h : LyndonInsepAt F P N A Γ Δ) : ∃ (k : ℕ), LyndonInsepAt F P N A Γ (insert (BoundedFormulaω.not (φs k)) Δ)

The right twin of the negated-iInf component selection.

theorem FirstOrder.Language.lyndonInsepAt_imp_dichotomy_right {L : Language} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {φ ψ : (L.withConstants ℕ).Sentenceω} (hmem : BoundedFormulaω.imp φ ψ ∈ Δ) (h : LyndonInsepAt F P N A Γ Δ) : LyndonInsepAt F P N A Γ (insert (BoundedFormulaω.not φ) Δ) ∨ LyndonInsepAt F P N A Γ (insert ψ Δ)

The right twin of the implication dichotomy.

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

The right twin of fresh-support growth.

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

The right twin of the quantifier round trip.

The paired family

def FirstOrder.Language.LyndonPairedMem {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ω) (S : Set (L.withConstants ℕ).Sentenceω) : Prop

A polarity-refined paired family member: a symmetrically support-budgeted, GenU-bounded, side-typed pair (Γ, Δ), inseparable at the flipped intersection class (F₁ ∩ F₂, P₁ ∩ N₂, N₁ ∩ P₂).

Equations

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

theorem FirstOrder.Language.lyndonPairedMem_subset_genU {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {P₁ N₁ P₂ N₂ : Set ((n : ℕ) × L.Relations n)} {rL rR : (L.withConstants ℕ).Sentenceω} {S : Set (L.withConstants ℕ).Sentenceω} (hS : LyndonPairedMem F₁ P₁ N₁ F₂ P₂ N₂ rL rR S) : S ⊆ GenU rL rR

Every family member lies in the enumeration universe.

The two coordinate-growth constructors

theorem FirstOrder.Language.lyndonPaired_insert_left {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {P₁ N₁ P₂ N₂ : Set ((n : ℕ) × L.Relations n)} {rL rR : (L.withConstants ℕ).Sentenceω} {S Γ Δ : Set (L.withConstants ℕ).Sentenceω} {A : Finset ℕ} {φ : (L.withConstants ℕ).Sentenceω} (hSeq : S = Γ ∪ Δ) (hΓfin : Γ.Finite) (hΔfin : Δ.Finite) (hΓU : Γ ⊆ GenU rL rR) (hΔU : Δ ⊆ GenU rL rR) (hΓS : Γ ⊆ SentBndPol F₁ P₁ N₁) (hΔS : Δ ⊆ SentBndPol F₂ P₂ N₂) (hφU : φ ∈ GenU rL rR) (hφS : φ ∈ SentBndPol F₁ P₁ N₁) (hsupp : (⋃ γ ∈ insert φ Γ, sentenceJConsts γ) ∪ ⋃ δ ∈ Δ, sentenceJConsts δ ⊆ ↑A) (hA : LyndonInsepAt (F₁ ∩ F₂) (P₁ ∩ N₂) (N₁ ∩ P₂) A (insert φ Γ) Δ) : LyndonPairedMem F₁ P₁ N₁ F₂ P₂ N₂ rL rR (S ∪ {φ})

Add φ to the Γ-coordinate of a family member.

theorem FirstOrder.Language.lyndonPaired_insert_right {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {P₁ N₁ P₂ N₂ : Set ((n : ℕ) × L.Relations n)} {rL rR : (L.withConstants ℕ).Sentenceω} {S Γ Δ : Set (L.withConstants ℕ).Sentenceω} {A : Finset ℕ} {φ : (L.withConstants ℕ).Sentenceω} (hSeq : S = Γ ∪ Δ) (hΓfin : Γ.Finite) (hΔfin : Δ.Finite) (hΓU : Γ ⊆ GenU rL rR) (hΔU : Δ ⊆ GenU rL rR) (hΓS : Γ ⊆ SentBndPol F₁ P₁ N₁) (hΔS : Δ ⊆ SentBndPol F₂ P₂ N₂) (hφU : φ ∈ GenU rL rR) (hφS : φ ∈ SentBndPol F₂ P₂ N₂) (hsupp : (⋃ γ ∈ Γ, sentenceJConsts γ) ∪ ⋃ δ ∈ insert φ Δ, sentenceJConsts δ ⊆ ↑A) (hA : LyndonInsepAt (F₁ ∩ F₂) (P₁ ∩ N₂) (N₁ ∩ P₂) A Γ (insert φ Δ)) : LyndonPairedMem F₁ P₁ N₁ F₂ P₂ N₂ rL rR (S ∪ {φ})

Add φ to the Δ-coordinate of a family member.