Polarity-refined inseparability and the mixed closures (issue #14, Unit 2 — the stop/go gate)

The single definitional change of the Lyndon refinement (audit v2 §D4): the separator class of InsepAt is refined from "base symbols in (F, R)" to "base functions in F, base positive relations in P, base negative relations in N".

LyndonInsepAt F P N A Γ Δ says the pair (Γ, Δ) admits no such separator at allowed constant support A. Everything else about the engine is untouched.

This file contains only the stop/go gate of the audit: the definition, the three genuinely mixed closures, the equality corollary they are consumed at, and the root-class acceptance equation. SentBndPol, the one-sided closure suite, and the paired family are Unit 3+.

• lyndonInsepAt_swap — dualization is class-exchanging: its separator map is σ ↦ σ.not, which swaps the two polarity classes, so the conclusion is at (F, N, P);
• lyndonInsepAt_imp_dichotomy (C1) — polarity-clean: the separator (σ₁.not).imp σ₂ has pos = pos σ₁ ∪ pos σ₂ and neg = neg σ₁ ∪ neg σ₂, the antecedent's two flips cancelling;
• lyndonInsepAt_insert_of_shared_entails — the only flipped-antecedent gate: its separator is σ.imp ρ, so the shared hypothesis enters with reversed polarity and the general statement must demand σ in the swapped class (Pos σ ⊆ N, Neg σ ⊆ P);
• lyndonInsepAt_insert_of_shared_constEq_entails — the specialization actually consumed by the kernel's cross-coordinate transfers, where the shared sentence is a constant equality and the swapped-class hypotheses are discharged by baseRelationsInSigned_constEq. The dependency on "equality is logical" is thereby visible in the API, not hidden inside a generic theorem;
• lyndon_root_class_eq — the acceptance equation of audit §D4a: with the Γ-root φ and the Δ-root ψ.not, the maintained class (P₁ ∩ N₂, N₁ ∩ P₂) is the endpoint's (Pos φ ∩ Pos ψ, Neg φ ∩ Neg ψ). This is the machine-checked form of the side flip in López–Escobar 1965, Theorem 4.0(.4).

The refined separator class

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

Polarity-refined support-parameterized inseparability: no separator whose base function symbols lie in F, whose base positively occurring relations lie in P and negatively occurring ones in N, whose constant support lies in A, entailed by Γ and refuted on Δ.

Equations

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

Gate 1: dualization exchanges the classes

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

Dualization is class-exchanging. Inseparability at (F, P, N) for (Γ, Δ) is inseparability at (F, N, P) for (Δ, Γ): the separator map σ ↦ σ.not swaps the polarity classes.

Gate 2: the implication dichotomy (the polarity-clean mixed closure)

theorem FirstOrder.Language.lyndonInsepAt_imp_dichotomy {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φ ψ : (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 ψ Γ) Δ

C1 (implication), polarity-refined. An implication in Γ yields one of the two possible refinements. The combined separator (σ₁.not).imp σ₂ stays in the same class: the antecedent is negated and then flipped again by the implication, so the two flips cancel.

Gate 3: shared-hypothesis transfer, with the swapped-class signature

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

Shared-hypothesis transfer, polarity-refined. If σ is shared in the swapped class (its positive relations bounded by N and its negative ones by P), is entailed by Δ, and φ is a consequence of Γ ∪ {σ}, then φ may be added to the Γ coordinate.

The swap is forced by the separator this gate builds, σ.imp ρ: since Pos (σ → ρ) = Neg σ ∪ Pos ρ and Neg (σ → ρ) = Pos σ ∪ Neg ρ, the shared hypothesis enters with reversed polarity. Keeping that in the signature is deliberate: a future transfer of a non-equality shared sentence must supply these bounds rather than silently break the theorem.

theorem FirstOrder.Language.lyndonInsepAt_insert_of_shared_constEq_entails {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {P N : Set ((n : ℕ) × L.Relations n)} {A : Finset ℕ} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φ : (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 equality specialization — the form the kernel's four cross-coordinate transfers actually consume. A constant equality has empty base polarity sets in both signs, so the swapped-class hypotheses of the general gate are discharged outright: this is exactly where "equality is logical" does its work, in the open.

The root-class acceptance equation (audit §D4a)

theorem FirstOrder.Language.lyndon_root_class_eq {L : Language} (φ ψ : L.Sentenceω) : (BoundedFormulaω.positiveRelationsIn φ ∩ (BoundedFormulaω.not ψ).negativeRelationsIn, BoundedFormulaω.negativeRelationsIn φ ∩ (BoundedFormulaω.not ψ).positiveRelationsIn) = (BoundedFormulaω.positiveRelationsIn φ ∩ BoundedFormulaω.positiveRelationsIn ψ, BoundedFormulaω.negativeRelationsIn φ ∩ BoundedFormulaω.negativeRelationsIn ψ)

The root orientation, as an equation. The engine runs with the Γ-root φ bounded by (Pos φ, Neg φ) and the Δ-root ψ.not bounded by (Pos (ψ.not), Neg (ψ.not)), maintaining the separator class (P₁ ∩ N₂, N₁ ∩ P₂). That class is the endpoint's pair of intersections — which is the machine-checked form of the side flip in López–Escobar 1965, Theorem 4.0(.4).