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

The consistency property

The paired model endpoint

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.