The budgeted labelled pair (issue #15, side-labelled restart)

The certificate selected by docs/malitz-source-reconstruction-2.md: Feferman's Theorem 4.3 keeps the two sides labelled — formulas are retained on their derivational side, never reprojected by vocabulary — and carries three conditions along the derivation beside the two entailments:

• the shared vocabulary condition on the separator;
• the shared constant condition, sentenceJConsts θ ⊆ theoryJConsts Γ ∩ theoryJConsts Δ (Feferman's Free₀(θ) ⊆ Free₀(ϕ) ∩ Free₀(ψ), in the constant presentation);
• the two quantifier permissions, hasQuantSigned true θ → HasQuantSigned true Γ and hasQuantSigned false θ → HasQuantSigned true Δ.

The second permission reads true on the right because Δ holds the negated consequent: at the root Un({r₂.not}) = Ex(r₂).

The shared-constant condition is primary, not derived from the permissions. That is the source's own account: "in building up an interpolant following a cut-free derivation … we are forced to introduce quantifiers into the interpolant only as required to maintain the condition (iii), and that turns out to lead to (iv)" (Feferman, "Ah, Chu!", pp. 2–3). The earlier FefermanAllowed had the dependency backwards, charging constants into the permissions as a standing assumption.

Everything the canonical-projection experiment needed disappears here. A fresh witness constant is added to one labelled side; being absent from the other, the shared-constant condition forbids the separator from mentioning it, so the separator transports unchanged — no genEx, no genAll, no support parameter to strip, no projection coverage, and no root tags. Quantifier non-growth is likewise immediate, because the quantified parent already sits on the same labelled side.

Methods/Interpolation/FefermanProjection.lean is not imported: it is retained as experimental evidence for the canonical-projection route and its C1 failure, not as a dependency.

Provenance

The labelled architecture is source-backed by Feferman's split-sequent proof, which he describes explicitly. The semantic consistency-property implementation below is this repository's adaptation: Stern's model-theoretic forcing proof is identified as the semantic dual, but its exact invariant is unverified — the paper has not been read.

The constant support of a labelled side

def FirstOrder.Language.theoryJConsts {L : Language} (T : Set (L.withConstants ℕ).Sentenceω) : Set ℕ

The Henkin constants occurring anywhere in a set of sentences.

Equations

• FirstOrder.Language.theoryJConsts T = ⋃ σ ∈ T, FirstOrder.Language.sentenceJConsts σ

theorem FirstOrder.Language.sentenceJConsts_subset_theoryJConsts {L : Language} {T : Set (L.withConstants ℕ).Sentenceω} {σ : (L.withConstants ℕ).Sentenceω} (hmem : σ ∈ T) : sentenceJConsts σ ⊆ theoryJConsts T

theorem FirstOrder.Language.theoryJConsts_mono {L : Language} {T T' : Set (L.withConstants ℕ).Sentenceω} (h : T ⊆ T') : theoryJConsts T ⊆ theoryJConsts T'

@[simp]

theorem FirstOrder.Language.theoryJConsts_insert {L : Language} {T : Set (L.withConstants ℕ).Sentenceω} {σ : (L.withConstants ℕ).Sentenceω} : theoryJConsts (insert σ T) = sentenceJConsts σ ∪ theoryJConsts T

theorem FirstOrder.Language.theoryJConsts_insert_of_subset {L : Language} {T : Set (L.withConstants ℕ).Sentenceω} {σ : (L.withConstants ℕ).Sentenceω} (h : sentenceJConsts σ ⊆ theoryJConsts T) : theoryJConsts (insert σ T) = theoryJConsts T

Insertion non-growth for constants: inserting a sentence whose constants the side already carries does not enlarge the side's support. Every branch rule needs exactly this.

theorem FirstOrder.Language.notMem_theoryJConsts_iff {L : Language} {T : Set (L.withConstants ℕ).Sentenceω} {c : ℕ} : c ∉ theoryJConsts T ↔ ∀ γ ∈ T, c ∉ sentenceJConsts γ

Freshness for a side is exactly non-membership in its support.

The certificate

def FirstOrder.Language.BudgetedPairSeparates {L : Language} (F₁ : Set ((n : ℕ) × L.Functions n)) (R₁ : Set ((n : ℕ) × L.Relations n)) (F₂ : Set ((n : ℕ) × L.Functions n)) (R₂ : Set ((n : ℕ) × L.Relations n)) (Γ Δ : Set (L.withConstants ℕ).Sentenceω) (θ : (L.withConstants ℕ).Sentenceω) : Prop

A budgeted separator of the labelled pair (Γ, Δ). Five conditions: the two entailments, the shared vocabulary, the shared constants, and the two quantifier permissions.

Equations

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

def FirstOrder.Language.BudgetedPairInsep {L : Language} (F₁ : Set ((n : ℕ) × L.Functions n)) (R₁ : Set ((n : ℕ) × L.Relations n)) (F₂ : Set ((n : ℕ) × L.Functions n)) (R₂ : Set ((n : ℕ) × L.Relations n)) (Γ Δ : Set (L.withConstants ℕ).Sentenceω) : Prop

The invariant: the labelled pair admits no budgeted separator.

Equations

• FirstOrder.Language.BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ = ¬∃ (θ : (L.withConstants ℕ).Sentenceω), FirstOrder.Language.BudgetedPairSeparates F₁ R₁ F₂ R₂ Γ Δ θ

Order behaviour of the invariant

Inseparability is antitone: a separator of a smaller labelled pair is still a separator of any larger one, because all five conditions weaken the right way — entailment survives adding premises, the constant condition survives enlarging the supports, and both permissions survive enlarging the sides. Contrapositively, inseparability of the larger pair gives it for every sub-pair.

This is what lets a discharge transfer a premise onto a side temporarily and then drop it again.

theorem FirstOrder.Language.budgetedPairInsep_antitone {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ Γ' Δ' : Set (L.withConstants ℕ).Sentenceω} (hΓ : Γ ⊆ Γ') (hΔ : Δ ⊆ Δ') (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ' Δ') : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ

Antitonicity in both labels.

theorem FirstOrder.Language.budgetedPairInsep_antitone_left {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ Γ' : Set (L.withConstants ℕ).Sentenceω} (hΓ : Γ ⊆ Γ') (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ' Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ

Antitonicity on the left alone — the form that drops a temporarily transferred premise.

theorem FirstOrder.Language.budgetedPairInsep_antitone_right {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ Δ' : Set (L.withConstants ℕ).Sentenceω} (hΔ : Δ ⊆ Δ') (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ') : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ

Antitonicity on the right alone.

C0 — the mixed contradiction gate

The diagnostic case for the labelled architecture: a sentence on the left with its negation on the right. All five conditions are paid by the two memberships themselves.

theorem FirstOrder.Language.not_budgetedPairInsep_of_mixed {L : Language} {σ : (L.withConstants ℕ).Sentenceω} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (hΓ : Γ ⊆ SentBnd F₁ R₁) (hΔ : Δ ⊆ SentBnd F₂ R₂) (hσΓ : σ ∈ Γ) (hσΔ : BoundedFormulaω.not σ ∈ Δ) : ¬BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ

Mixed C0. If σ ∈ Γ and σ.not ∈ Δ then σ is a budgeted separator: its vocabulary is shared because the two sides bound the same sentence, its constants occur in both, its universal occurrences are paid by Γ, and its existential occurrences are paid by the universal occurrences of σ.not in Δ.

theorem FirstOrder.Language.not_budgetedPairInsep_of_mixed_rev {L : Language} {σ : (L.withConstants ℕ).Sentenceω} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (hΓ : Γ ⊆ SentBnd F₁ R₁) (hΔ : Δ ⊆ SentBnd F₂ R₂) (hσΓ : BoundedFormulaω.not σ ∈ Γ) (hσΔ : σ ∈ Δ) : ¬BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ

Mixed C0, reverse labels. The other cross combination: the negation on the left and the sentence itself on the right. σ.not separates directly — no double-negation detour through not_budgetedPairInsep_of_mixed, which would need σ.not.not ∈ Δ.

Both permissions flip with the sign: the universal occurrences of σ.not are paid by its own membership in Γ, and its existential occurrences are the universal occurrences of σ, paid by σ ∈ Δ.

theorem FirstOrder.Language.not_budgetedPairInsep_of_left_contradiction {L : Language} {σ : (L.withConstants ℕ).Sentenceω} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (hσ : σ ∈ Γ) (hnσ : BoundedFormulaω.not σ ∈ Γ) : ¬BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ

Same-side C0. A sentence and its negation on one side make it inconsistent, and the quantifier-free, constant-free ⊥ (resp. ⊤) separates.

theorem FirstOrder.Language.not_budgetedPairInsep_of_falsum_left {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (hmem : BoundedFormulaω.falsum ∈ Γ) : ¬BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ

C0a, left. ⊥ on a side is its own separator: Γ ⊨ ⊥ by membership, Δ ⊨ ¬⊥ vacuously, and ⊥ carries no symbol, constant or quantifier.

theorem FirstOrder.Language.not_budgetedPairInsep_of_falsum_right {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (hmem : BoundedFormulaω.falsum ∈ Δ) : ¬BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ

C0a, right. Dual: ⊤ separates, since Δ holding ⊥ has no models at all.

C1 — implication branching

The source's rule verbatim: disjunction when the principal formula is on the left, conjunction when on the right. There is no leakage case to consider — the branch sentences join the side their parent is on, and nowhere else.

theorem FirstOrder.Language.budgetedPairInsep_imp_left {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (φ ψ : (L.withConstants ℕ).Sentenceω) (hmem : BoundedFormulaω.imp φ ψ ∈ Γ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ (insert (BoundedFormulaω.not φ) Γ) Δ ∨ BudgetedPairInsep F₁ R₁ F₂ R₂ (insert ψ Γ) Δ

C1, left. Separator τ₁ ∨ τ₂, written (τ₁.not).imp τ₂.

theorem FirstOrder.Language.budgetedPairInsep_imp_right {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (φ ψ : (L.withConstants ℕ).Sentenceω) (hmem : BoundedFormulaω.imp φ ψ ∈ Δ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ (insert (BoundedFormulaω.not φ) Δ) ∨ BudgetedPairInsep F₁ R₁ F₂ R₂ Γ (insert ψ Δ)

C1, right. Separator τ₁ ∧ τ₂.

The fresh-witness rules

The payoff of labelling. A witness constant c fresh for both sides is added to one of them. Freshness on the opposite side is what forbids the separator from mentioning c — via the shared-constant condition — so the separator transports unchanged; freshness on the own side is what moves the entailment. No constant abstraction appears anywhere.

theorem FirstOrder.Language.entails_of_entails_insert_witness_of_fresh {L : Language} {T : Set (L.withConstants ℕ).Sentenceω} (c : ℕ) (φc τ : (L.withConstants ℕ).Sentenceω) (hpar : genEx c φc ∈ T) (hcT : ∀ γ ∈ T, c ∉ sentenceJConsts γ) (hcτ : c ∉ sentenceJConsts τ) (h : (insert φc T).Entails τ) : Theoryω.Entails T τ

Entailment transfer for a separator that does not mention the witness constant, from an existential parent. The _of_fresh suffix distinguishes these from the quarantined constant-free versions in FefermanProjection.lean: here the separator need only avoid the single witness constant, which is exactly what the shared-constant condition delivers.

theorem FirstOrder.Language.entails_of_entails_insert_negInstConst_of_fresh {L : Language} {T : Set (L.withConstants ℕ).Sentenceω} (c : ℕ) (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) (τ : (L.withConstants ℕ).Sentenceω) (hpar : φ.all.not ∈ T) (hcT : ∀ γ ∈ T, c ∉ sentenceJConsts γ) (hcτ : c ∉ sentenceJConsts τ) (h : (insert (BoundedFormulaω.not (instConst c φ)) T).Entails τ) : Theoryω.Entails T τ

The kernel's neg_all_witness shape: parent (φ.all).not, inserted witness (instConst c φ).not.

theorem FirstOrder.Language.budgetedPairInsep_witness_left {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (c : ℕ) (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) (hpar : φ.all.not ∈ Γ) (hcΓ : c ∉ theoryJConsts Γ) (hcΔ : c ∉ theoryJConsts Δ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ (insert (BoundedFormulaω.not (instConst c φ)) Γ) Δ

Fresh witness on the left. The separator is transported unchanged: opposite-side freshness plus the shared-constant condition force c ∉ sentenceJConsts θ.

theorem FirstOrder.Language.budgetedPairInsep_witness_right {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (c : ℕ) (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) (hpar : φ.all.not ∈ Δ) (hcΓ : c ∉ theoryJConsts Γ) (hcΔ : c ∉ theoryJConsts Δ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ (insert (BoundedFormulaω.not (instConst c φ)) Δ)

Fresh witness on the right, the mirror image.

The root collapse and the interpolant equation

theorem FirstOrder.Language.isUniversal_of_budgetedPairSeparates {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {θ : (L.withConstants ℕ).Sentenceω} (h : BudgetedPairSeparates F₁ R₁ F₂ R₂ Γ Δ θ) (hΔ : ¬Theoryω.HasQuantSigned true Δ) : BoundedFormulaω.IsUniversal θ

Root collapse. A budgeted separator against a right side with no universal occurrence is universal; against constant-free sides it is constant-free.

theorem FirstOrder.Language.sentenceJConsts_eq_empty_of_budgetedPairSeparates {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {θ : (L.withConstants ℕ).Sentenceω} (h : BudgetedPairSeparates F₁ R₁ F₂ R₂ Γ Δ θ) (hΓ : theoryJConsts Γ = ∅) : sentenceJConsts θ = ∅

theorem FirstOrder.Language.exists_universal_interpolant_of_not_budgetedPairInsep {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} (hr₂ : ¬BoundedFormulaω.hasQuantSigned false r₂) (hc₁ : sentenceJConsts r₁ = ∅) (h : ¬BudgetedPairInsep F₁ R₁ F₂ R₂ {r₁} {BoundedFormulaω.not r₂}) : ∃ (θ : (L.withConstants ℕ).Sentenceω), BoundedFormulaω.IsUniversal θ ∧ θ ∈ SentBnd (F₁ ∩ F₂) (R₁ ∩ R₂) ∧ sentenceJConsts θ = ∅ ∧ r₁.Entails θ ∧ θ.Entails r₂

The root equation. Failure of the invariant at the root pair ({r₁}, {r₂.not}) — with r₂ carrying no existential occurrence, i.e. universal, and the roots constant-free — delivers exactly a Malitz interpolant: universal, shared-vocabulary, constant-free, r₁ ⊨ θ and θ ⊨ r₂.

The family shell

BudgetedPairMem is the existential labelled decomposition: the scheduler still completes the single set S, while every membership proof retains the labels the closure argument uses. A shared formula is never automatically duplicated — but, S = Γ ∪ Δ permitting overlap, a discharge may choose a decomposition in which it appears on both sides, which is exactly what the cross-label transfer gates below license.

def FirstOrder.Language.BudgetedPairMem {L : Language} (r₁ r₂ : (L.withConstants ℕ).Sentenceω) (F₁ : Set ((n : ℕ) × L.Functions n)) (R₁ : Set ((n : ℕ) × L.Relations n)) (F₂ : Set ((n : ℕ) × L.Functions n)) (R₂ : Set ((n : ℕ) × L.Relations n)) (S : Set (L.withConstants ℕ).Sentenceω) : Prop

Membership in the labelled family: some finite, GenU-bounded, side-typed decomposition of S whose labelled pair is budget-inseparable.

Equations

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

theorem FirstOrder.Language.budgetedPairMem_insert_left {L : Language} {σ : (L.withConstants ℕ).Sentenceω} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {S : Set (L.withConstants ℕ).Sentenceω} (hΓfin : Γ.Finite) (hΔfin : Δ.Finite) (hΓU : Γ ⊆ GenU r₁ r₂) (hΔU : Δ ⊆ GenU r₁ r₂) (hΓb : Γ ⊆ SentBnd F₁ R₁) (hΔb : Δ ⊆ SentBnd F₂ R₂) (hS : S = Γ ∪ Δ) (hσU : σ ∈ GenU r₁ r₂) (hσb : σ ∈ SentBnd F₁ R₁) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ (insert σ Γ) Δ) : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ (insert σ S)

Left-label insertion bookkeeping: the union re-decomposes with σ on the left.

theorem FirstOrder.Language.budgetedPairMem_insert_right {L : Language} {σ : (L.withConstants ℕ).Sentenceω} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {S : Set (L.withConstants ℕ).Sentenceω} (hΓfin : Γ.Finite) (hΔfin : Δ.Finite) (hΓU : Γ ⊆ GenU r₁ r₂) (hΔU : Δ ⊆ GenU r₁ r₂) (hΓb : Γ ⊆ SentBnd F₁ R₁) (hΔb : Δ ⊆ SentBnd F₂ R₂) (hS : S = Γ ∪ Δ) (hσU : σ ∈ GenU r₁ r₂) (hσb : σ ∈ SentBnd F₂ R₂) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ (insert σ Δ)) : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ (insert σ S)

Right-label insertion bookkeeping.

Fresh constants for a labelled pair

Γ.Finite alone is not enough: a single infinitary sentence can mention infinitely many constants. Finiteness of the support needs the GenU bound as well, via genU_finite_support, together with finite constant support of the two roots.

theorem FirstOrder.Language.theoryJConsts_finite_of_subset_genU {L : Language} {Γ : Set (L.withConstants ℕ).Sentenceω} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} (hr₁ : (sentenceJConsts r₁).Finite) (hr₂ : (sentenceJConsts r₂).Finite) (hΓfin : Γ.Finite) (hΓU : Γ ⊆ GenU r₁ r₂) : (theoryJConsts Γ).Finite

The constant support of a finite, GenU-bounded side is finite.

theorem FirstOrder.Language.exists_fresh_budgetedPair {L : Language} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} (hr₁ : (sentenceJConsts r₁).Finite) (hr₂ : (sentenceJConsts r₂).Finite) (hΓfin : Γ.Finite) (hΔfin : Δ.Finite) (hΓU : Γ ⊆ GenU r₁ r₂) (hΔU : Δ ⊆ GenU r₁ r₂) : ∃ c ∉ theoryJConsts Γ, c ∉ theoryJConsts Δ

A constant fresh for both labels exists. Consumed only by the fresh-witness fields; the root finiteness hypotheses enter the package for this reason alone.

C0, the remaining label combination

theorem FirstOrder.Language.not_budgetedPairInsep_of_right_contradiction {L : Language} {σ : (L.withConstants ℕ).Sentenceω} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (hσ : σ ∈ Δ) (hnσ : BoundedFormulaω.not σ ∈ Δ) : ¬BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ

Same-side C0, right. An inconsistent right side is separated by ⊤, the mirror of the ⊥ separator for an inconsistent left side.

Shared-hypothesis transfer

Duplicating a quantifier-free shared sentence onto the other label. The separator becomes σ.imp θ (resp. σ.and θ), and the price is exactly that σ's constants already occur on the receiving side — the shared-constant condition is what charges it.

theorem FirstOrder.Language.budgetedPairInsep_insert_shared_left {L : Language} {σ : (L.withConstants ℕ).Sentenceω} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (hσΔ : σ ∈ Δ) (hb₁ : σ ∈ SentBnd F₁ R₁) (hb₂ : σ ∈ SentBnd F₂ R₂) (hcσ : sentenceJConsts σ ⊆ theoryJConsts Γ) (hq : ∀ (s : Bool), ¬BoundedFormulaω.hasQuantSigned s σ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ (insert σ Γ) Δ

Transfer right → left. A quantifier-free shared σ ∈ Δ whose constants Γ already carries may be duplicated onto the left.

theorem FirstOrder.Language.budgetedPairInsep_insert_shared_right {L : Language} {σ : (L.withConstants ℕ).Sentenceω} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (hσΓ : σ ∈ Γ) (hb₁ : σ ∈ SentBnd F₁ R₁) (hb₂ : σ ∈ SentBnd F₂ R₂) (hcσ : sentenceJConsts σ ⊆ theoryJConsts Δ) (hq : ∀ (s : Bool), ¬BoundedFormulaω.hasQuantSigned s σ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ (insert σ Δ)

Transfer left → right. The mirror: separator σ.and θ.

Cross-label equality and relation transfer

The mixed rel_congr case, which was load-bearing in Craig's paired construction and is the likeliest hidden obstruction here: the relation atom is on the left, the equality atom on the right. The derived atom mentions a constant b that only the right side carries, so the separator of the extended pair may mention b; substituting the equality's shared partner g i for b removes it, and the shared-constant condition pays for it — g i occurs on both sides. No quantifier is introduced, so both budgets are untouched.

theorem FirstOrder.Language.budgetedPairInsep_relCongr_mixed {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {l : ℕ} (R : L.Relations l) (g : Fin l → ℕ) (i : Fin l) (b : ℕ) (hrel : relInst R g ∈ Γ) (heq : constEq (g i) b ∈ Δ) (hbΓ : b ∉ theoryJConsts Γ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ (insert (relInst R (Function.update g i b)) Γ) Δ

Mixed-label relation congruence. relInst R g ∈ Γ, constEq (g i) b ∈ Δ, b fresh for the left: the derived atom may be inserted on the left. The separator is transported by substConst b (g i).

Generic insertion drivers

Every deterministic field is an instance of the same statement: the new sentence is entailed by the side that receives it, and both its constants and its positive quantifier occurrences are already carried there. The three obligations stay separate on purpose — the proof's content is which label received the formula.

theorem FirstOrder.Language.budgetedPairInsep_insert_entailed_left {L : Language} {σ : (L.withConstants ℕ).Sentenceω} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (hent : Theoryω.Entails Γ σ) (hcσ : sentenceJConsts σ ⊆ theoryJConsts Γ) (hqσ : BoundedFormulaω.hasQuantSigned true σ → Theoryω.HasQuantSigned true Γ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ (insert σ Γ) Δ

Left driver.

theorem FirstOrder.Language.budgetedPairInsep_insert_entailed_right {L : Language} {σ : (L.withConstants ℕ).Sentenceω} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (hent : Theoryω.Entails Δ σ) (hcσ : sentenceJConsts σ ⊆ theoryJConsts Δ) (hqσ : BoundedFormulaω.hasQuantSigned true σ → Theoryω.HasQuantSigned true Δ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ (insert σ Δ)

Right driver.

theorem FirstOrder.Language.budgetedPairInsep_insert_of_member_left {L : Language} {σ : (L.withConstants ℕ).Sentenceω} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {ρ : (L.withConstants ℕ).Sentenceω} (hρ : ρ ∈ Γ) (hent : Theoryω.Entails Γ σ) (hc : sentenceJConsts σ ⊆ sentenceJConsts ρ) (hq : BoundedFormulaω.hasQuantSigned true σ → BoundedFormulaω.hasQuantSigned true ρ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ (insert σ Γ) Δ

The recurring shape: the new sentence is licensed by a member ρ of the side.

theorem FirstOrder.Language.budgetedPairInsep_insert_of_member_right {L : Language} {σ : (L.withConstants ℕ).Sentenceω} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {ρ : (L.withConstants ℕ).Sentenceω} (hρ : ρ ∈ Δ) (hent : Theoryω.Entails Δ σ) (hc : sentenceJConsts σ ⊆ sentenceJConsts ρ) (hq : BoundedFormulaω.hasQuantSigned true σ → BoundedFormulaω.hasQuantSigned true ρ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ (insert σ Δ)

The deterministic connective fields

C2 (double negation), C1′ (negated implication, both components), C3 (conjunction component) and C4′ (negated-disjunction component), on each label. Each is three obligations against the parent.

theorem FirstOrder.Language.budgetedPairInsep_not_not_left {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φ : (L.withConstants ℕ).Sentenceω} (hmem : (BoundedFormulaω.not φ).not ∈ Γ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ (insert φ Γ) Δ

C2, left.

theorem FirstOrder.Language.budgetedPairInsep_not_not_right {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φ : (L.withConstants ℕ).Sentenceω} (hmem : (BoundedFormulaω.not φ).not ∈ Δ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ (insert φ Δ)

C2, right.

theorem FirstOrder.Language.budgetedPairInsep_neg_imp_left₁ {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φ ψ : (L.withConstants ℕ).Sentenceω} (hmem : (BoundedFormulaω.imp φ ψ).not ∈ Γ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ (insert φ Γ) Δ

C1′ antecedent, left.

theorem FirstOrder.Language.budgetedPairInsep_neg_imp_left₂ {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φ ψ : (L.withConstants ℕ).Sentenceω} (hmem : (BoundedFormulaω.imp φ ψ).not ∈ Γ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ (insert (BoundedFormulaω.not ψ) Γ) Δ

C1′ consequent, left.

theorem FirstOrder.Language.budgetedPairInsep_neg_imp_right₁ {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φ ψ : (L.withConstants ℕ).Sentenceω} (hmem : (BoundedFormulaω.imp φ ψ).not ∈ Δ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ (insert φ Δ)

C1′ antecedent, right.

theorem FirstOrder.Language.budgetedPairInsep_neg_imp_right₂ {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φ ψ : (L.withConstants ℕ).Sentenceω} (hmem : (BoundedFormulaω.imp φ ψ).not ∈ Δ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ (insert (BoundedFormulaω.not ψ) Δ)

C1′ consequent, right.

theorem FirstOrder.Language.budgetedPairInsep_iInf_component_left {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φs : ℕ → (L.withConstants ℕ).Sentenceω} {k : ℕ} (hmem : BoundedFormulaω.iInf φs ∈ Γ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ (insert (φs k) Γ) Δ

C3, left: a conjunction component.

theorem FirstOrder.Language.budgetedPairInsep_iInf_component_right {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φs : ℕ → (L.withConstants ℕ).Sentenceω} {k : ℕ} (hmem : BoundedFormulaω.iInf φs ∈ Δ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ (insert (φs k) Δ)

C3, right.

theorem FirstOrder.Language.budgetedPairInsep_neg_iSup_component_left {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φs : ℕ → (L.withConstants ℕ).Sentenceω} {k : ℕ} (hmem : (BoundedFormulaω.iSup φs).not ∈ Γ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ (insert (BoundedFormulaω.not (φs k)) Γ) Δ

C4′, left: a negated-disjunction component.

theorem FirstOrder.Language.budgetedPairInsep_neg_iSup_component_right {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φs : ℕ → (L.withConstants ℕ).Sentenceω} {k : ℕ} (hmem : (BoundedFormulaω.iSup φs).not ∈ Δ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ (insert (BoundedFormulaω.not (φs k)) Δ)

C4′, right.

Countable branching — the last isolated gate

The ⋁-style fields, where the consumer must choose a component. Each is proved by contraposition: assume every component extension is separable, choose its separator θₙ, combine with iSup or iInf according to the label, and check the five conditions componentwise.

Three things are worth watching, and all three come out clean:

• the combined separator's constant support is the union of the component supports, and each component support already lies in both theory supports — because inserting a component does not enlarge the receiving side's support, the parent already carrying its constants;
• hasQuantSigned on iSup/iInf exposes one offending component, so the permission flows from that component's separator and then from the parent formula, again by non-growth;
• no label projection and no support enlargement appears anywhere.

theorem FirstOrder.Language.budgetedPairInsep_iSup_left {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (hmem : BoundedFormulaω.iSup φs ∈ Γ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : ∃ (k : ℕ), BudgetedPairInsep F₁ R₁ F₂ R₂ (insert (φs k) Γ) Δ

C4, left: countable disjunction. Separator ⋁ₙ θₙ.

theorem FirstOrder.Language.budgetedPairInsep_iSup_right {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (hmem : BoundedFormulaω.iSup φs ∈ Δ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : ∃ (k : ℕ), BudgetedPairInsep F₁ R₁ F₂ R₂ Γ (insert (φs k) Δ)

C4, right: countable disjunction. Separator ⋀ₙ θₙ.

theorem FirstOrder.Language.budgetedPairInsep_neg_iInf_left {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (hmem : (BoundedFormulaω.iInf φs).not ∈ Γ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : ∃ (k : ℕ), BudgetedPairInsep F₁ R₁ F₂ R₂ (insert (BoundedFormulaω.not (φs k)) Γ) Δ

C3′, left: negated countable conjunction. Separator ⋁ₙ θₙ.

theorem FirstOrder.Language.budgetedPairInsep_neg_iInf_right {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φs : ℕ → (L.withConstants ℕ).Sentenceω} (hmem : (BoundedFormulaω.iInf φs).not ∈ Δ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : ∃ (k : ℕ), BudgetedPairInsep F₁ R₁ F₂ R₂ Γ (insert (BoundedFormulaω.not (φs k)) Δ)

C3′, right: negated countable conjunction. Separator ⋀ₙ θₙ.

The substitution cut, and the mixed equality cases

Mixed eq_trans is the one equality case the shared-hypothesis transfer cannot reach: with a = b on the left and b = d on the right, neither side's support contains both endpoints — the pivot b is the only automatically shared constant. The substitution mechanism that solved mixed rel_congr solves it too, and the two statements genuinely align, so the common core is extracted once.

theorem FirstOrder.Language.budgetedPairInsep_substCut_left {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (b c : ℕ) (ψ : (L.withConstants ℕ).Sentenceω) (hcΓ : c ∉ theoryJConsts Γ) (hbΓ : b ∈ theoryJConsts Γ) (hbΔ : b ∈ theoryJConsts Δ) (hΔeq : Theoryω.Entails Δ (constEq b c)) (hcψ : sentenceJConsts ψ ⊆ insert c (theoryJConsts Γ)) (hqψ : ∀ (s : Bool), ¬BoundedFormulaω.hasQuantSigned s ψ) (hΓψ : Theoryω.Entails Γ (substConst c b ψ)) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ (insert ψ Γ) Δ

Substitution cut, left. Insert ψ on the left, where ψ mentions a constant c that only the right side carries. If the left entails the c := b image of ψ and the right proves b = c, then a separator of the extended pair substitutes down to one of the original pair — mentioning the shared pivot b instead of the remote c. hasQuantSigned_substConst keeps both budgets fixed.

theorem FirstOrder.Language.budgetedPairInsep_substCut_right {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} (b c : ℕ) (ψ : (L.withConstants ℕ).Sentenceω) (hcΔ : c ∉ theoryJConsts Δ) (hbΓ : b ∈ theoryJConsts Γ) (hbΔ : b ∈ theoryJConsts Δ) (hΓeq : Theoryω.Entails Γ (constEq b c)) (hcψ : sentenceJConsts ψ ⊆ insert c (theoryJConsts Δ)) (hqψ : ∀ (s : Bool), ¬BoundedFormulaω.hasQuantSigned s ψ) (hΔψ : Theoryω.Entails Δ (substConst c b ψ)) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ (insert ψ Δ)

Substitution cut, right. The mirror of budgetedPairInsep_substCut_left: ψ goes onto the right, mentioning a constant c that only the left side carries, and it is the left that proves b = c. Same separator operation, sides exchanged.

theorem FirstOrder.Language.budgetedPairInsep_relCongr_mixed_rev {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {l : ℕ} (Rr : L.Relations l) (g : Fin l → ℕ) (i : Fin l) (b : ℕ) (hrel : relInst Rr g ∈ Δ) (heq : constEq (g i) b ∈ Γ) (hbΔ : b ∉ theoryJConsts Δ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ (insert (relInst Rr (Function.update g i b)) Δ)

Mixed relation congruence, reverse labels. The fourth rel_congr distribution: the atom on the right, the equation on the left. A short application of the right substitution cut — the pivot is g i (shared: on the right by the atom, on the left by the equation) and the remote constant is the replacement b, which only the left carries.

theorem FirstOrder.Language.budgetedPairInsep_eq_trans_mixed_right {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {a b d : ℕ} (hab : constEq a b ∈ Γ) (hbd : constEq b d ∈ Δ) (hdΓ : d ∉ theoryJConsts Γ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ (insert (constEq a d) Γ) Δ

Mixed transitivity, remote right endpoint. a = b on the left, b = d on the right, d absent from the left: insert a = d on the left, substituting the pivot b for d.

theorem FirstOrder.Language.budgetedPairInsep_eq_trans_mixed_left {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {a b d : ℕ} (hab : constEq a b ∈ Δ) (hbd : constEq b d ∈ Γ) (haΓ : a ∉ theoryJConsts Γ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ (insert (constEq a d) Γ) Δ

Mixed transitivity, remote left endpoint. a = b on the right, b = d on the left, a absent from the left: insert a = d on the left, substituting the pivot b for a.

The remaining equality fields

eq_refl, eq_symm, and same-label eq_trans, on each label. All are entailed-insertion driver applications: the atoms are quantifier-free, so the budget obligations are vacuous, and only the constant obligation carries information.

theorem FirstOrder.Language.budgetedPairInsep_eq_refl_left {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {c : ℕ} (hc : c ∈ theoryJConsts Γ ∨ c ∉ theoryJConsts Δ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ (insert (constEq c c) Γ) Δ

eq_refl, left. Legal whenever c is already on the left, or absent from the right — together with the right twin this covers every constant.

theorem FirstOrder.Language.budgetedPairInsep_eq_symm_left {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {a b : ℕ} (hmem : constEq a b ∈ Γ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ (insert (constEq b a) Γ) Δ

eq_symm, left.

theorem FirstOrder.Language.budgetedPairInsep_eq_symm_right {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {a b : ℕ} (hmem : constEq a b ∈ Δ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ (insert (constEq b a) Δ)

eq_symm, right.

theorem FirstOrder.Language.budgetedPairInsep_eq_trans_left {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {a b d : ℕ} (hab : constEq a b ∈ Γ) (hbd : constEq b d ∈ Γ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ (insert (constEq a d) Γ) Δ

eq_trans, both premises on the left.

theorem FirstOrder.Language.budgetedPairInsep_eq_trans_right {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {a b d : ℕ} (hab : constEq a b ∈ Δ) (hbd : constEq b d ∈ Δ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ (insert (constEq a d) Δ)

eq_trans, both premises on the right.

Same-side relation congruence, and the right eq_refl twin

The two remaining atomic fields. Both are deterministic: the new sentence is entailed by the receiving side, its constants are already carried there, and being atomic it contributes no quantifier occurrence at either sign — so each is an instance of the corresponding driver.

theorem FirstOrder.Language.budgetedPairInsep_eq_refl_right {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {c : ℕ} (hc : c ∈ theoryJConsts Δ ∨ c ∉ theoryJConsts Γ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ (insert (constEq c c) Δ)

eq_refl, right — the twin of budgetedPairInsep_eq_refl_left; together they cover every constant.

theorem FirstOrder.Language.budgetedPairInsep_relCongr_left {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {l : ℕ} (Rr : L.Relations l) (g : Fin l → ℕ) (i : Fin l) (b : ℕ) (hrel : relInst Rr g ∈ Γ) (heq : constEq (g i) b ∈ Γ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ (insert (relInst Rr (Function.update g i b)) Γ) Δ

Same-side relation congruence, left. Both premises on Γ: the congruent atom is entailed there, and every constant it mentions — including the replacement b — is already carried, b by the equation constEq (g i) b ∈ Γ itself. Contrast budgetedPairInsep_relCongr_mixed, where the equation sits on the opposite side and the separator must be substituted.

theorem FirstOrder.Language.budgetedPairInsep_relCongr_right {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {l : ℕ} (Rr : L.Relations l) (g : Fin l → ℕ) (i : Fin l) (b : ℕ) (hrel : relInst Rr g ∈ Δ) (heq : constEq (g i) b ∈ Δ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ (insert (relInst Rr (Function.update g i b)) Δ)

Same-side relation congruence, right.

Universal instantiation — the all_inst gate

The first field whose new sentence can carry a constant the side does not yet own. Two facts make it go through without strengthening the invariant:

• the quantifier budget collapses: the inserted instance can only add occurrences that the universal parent φ.all, already on the same side, pays for;
• the constant support grows by at most {c}, so a separator that survives the insertion either never mentioned c (and transports unchanged) or can be universally generalized over it.

theorem FirstOrder.Language.sentBnd_genAll {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} (c : ℕ) {θ : (L.withConstants ℕ).Sentenceω} (h : θ ∈ SentBnd F R) : genAll c θ ∈ SentBnd F R

genAll keeps a sentence inside a side's vocabulary bound: generalization removes a constant, it never introduces a base symbol.

theorem FirstOrder.Language.theoryJConsts_insert_instConst_subset {L : Language} {Γ : Set (L.withConstants ℕ).Sentenceω} {φ : (L.withConstants ℕ).BoundedFormulaω Empty 1} {c : ℕ} (hmem : φ.all ∈ Γ) : theoryJConsts (insert (instConst c φ) Γ) ⊆ insert c (theoryJConsts Γ)

Support growth of an instance. Inserting instConst c φ beside its universal parent enlarges the side's constant support by at most {c}.

theorem FirstOrder.Language.hasQuantSigned_true_of_all_mem {L : Language} {Γ : Set (L.withConstants ℕ).Sentenceω} {φ : (L.withConstants ℕ).BoundedFormulaω Empty 1} (hmem : φ.all ∈ Γ) : Theoryω.HasQuantSigned true Γ

Quantifier-budget collapse. A side holding a universal sentence has a universal budget outright — hasQuantSigned true φ.all is true = true ∨ _, so the parent alone witnesses it.

Stated unconditionally rather than as HasQuantSigned true (insert (instConst c φ) Γ) → HasQuantSigned true Γ: the implication is what the gate consumes, but it holds vacuously, because the conclusion never depended on the inserted instance. Every universal permission demanded of the augmented left side is discharged by this.

theorem FirstOrder.Language.budgetedPairInsep_all_inst_left {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φ : (L.withConstants ℕ).BoundedFormulaω Empty 1} (c : ℕ) (hmem : φ.all ∈ Γ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ (insert (instConst c φ) Γ) Δ

all_inst, left. A universal on the left admits every constant instance — including constants the left side does not yet carry, and constants already shared with a separator. No freshness hypothesis is required.

The proof splits on whether Γ already owns c.

• If it does, the instance adds no constant and the separator transports unchanged (budgetedPairInsep_insert_entailed_left).
• If it does not, a separator of the augmented pair may mention c; universally generalizing it to genAll c θ removes c, and freshness for Γ — which is exactly this branch's hypothesis — licenses ∀-introduction on the left. The right side needs no freshness: it refutes ∀x θ(x) by instantiating at c's own interpretation.

Both branches pay the universal permission with φ.all itself, never with the instance.

theorem FirstOrder.Language.sentBnd_genEx {L : Language} {F : Set ((n : ℕ) × L.Functions n)} {R : Set ((n : ℕ) × L.Relations n)} (c : ℕ) {θ : (L.withConstants ℕ).Sentenceω} (h : θ ∈ SentBnd F R) : genEx c θ ∈ SentBnd F R

genEx keeps a sentence inside a side's vocabulary bound.

theorem FirstOrder.Language.entails_not_genEx_of_all_inst_entails_not {L : Language} {Δ : Set (L.withConstants ℕ).Sentenceω} {φ : (L.withConstants ℕ).BoundedFormulaω Empty 1} {c : ℕ} {θ : (L.withConstants ℕ).Sentenceω} (hfresh : ∀ δ ∈ Δ, c ∉ sentenceJConsts δ) (hmem : φ.all ∈ Δ) (hyp : (insert (instConst c φ) Δ).Entails (BoundedFormulaω.not θ)) : Theoryω.Entails Δ (BoundedFormulaω.not (genEx c θ))

The right gate's semantic core. If Δ together with the instance φ(c) refutes θ, and c is fresh for Δ while the universal parent φ.all sits in Δ, then Δ alone refutes ∃x θ(x).

Given a witness x for genEx c θ, reinterpret c as x: freshness preserves every member of Δ, the parent φ.all ∈ Δ re-supplies the instance under that reinterpretation, and the hypothesis then refutes the corresponding instance of θ.

Neutral in content — belongs in the eventual #39 constant-surgery consolidation rather than here.

theorem FirstOrder.Language.budgetedPairInsep_all_inst_right {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {Γ Δ : Set (L.withConstants ℕ).Sentenceω} {φ : (L.withConstants ℕ).BoundedFormulaω Empty 1} (c : ℕ) (hmem : φ.all ∈ Δ) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ Δ) : BudgetedPairInsep F₁ R₁ F₂ R₂ Γ (insert (instConst c φ) Δ)

all_inst, right. The mirror of budgetedPairInsep_all_inst_left, with genEx in place of genAll.

The asymmetry is only in which side abstracts: here Γ ⊨ genEx c θ is freshness-free (∃-introduction is weakening), and the work moves to Δ, where the fresh-case hypothesis is exactly what entails_not_genEx_of_all_inst_entails_not consumes. The new existential occurrence is paid outright by φ.all ∈ Δ, which witnesses a universal budget on the receiving side.

The family-level field helpers

One helper per ConsistencyPropertyEqOn field, each stated in the structure's own S ∪ {φ} shape so that the final package is pure eta-application. Every body follows the same four steps: unpack the labelled decomposition, dispatch on the label of the parent, apply one BudgetedPairInsep gate, and repackage with budgetedPairMem_insert_left/_right. The insert-versus-union normalization is hidden here via Set.union_singleton.

No semantic realization proof appears below; if one is ever needed, a gate is missing.

theorem FirstOrder.Language.budgetedPairMem_subset_U {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {S : Set (L.withConstants ℕ).Sentenceω} (hS : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ S) : S ⊆ GenU r₁ r₂

theorem FirstOrder.Language.budgetedPairMem_C0_no_falsum {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {S : Set (L.withConstants ℕ).Sentenceω} (hS : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ S) : BoundedFormulaω.falsum ∉ S

theorem FirstOrder.Language.budgetedPairMem_C0_no_contradiction {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {S : Set (L.withConstants ℕ).Sentenceω} (hS : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ S) (φ : (L.withConstants ℕ).Sentenceω) : ¬(φ ∈ S ∧ BoundedFormulaω.not φ ∈ S)

All four label combinations, visibly.

theorem FirstOrder.Language.budgetedPairMem_C1_imp {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {S : Set (L.withConstants ℕ).Sentenceω} (hS : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ S) (φ ψ : (L.withConstants ℕ).Sentenceω) (hmem : BoundedFormulaω.imp φ ψ ∈ S) : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ (S ∪ {BoundedFormulaω.not φ}) ∨ BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ (S ∪ {ψ})

C1. The first field that builds a new member, so it is the one that exercises the whole repackaging path: label dispatch, the gate's own disjunction, and the insert-versus-union normalization — which is confined to the simpa only [Set.union_singleton] at each boundary.

theorem FirstOrder.Language.budgetedPairMem_C1_neg_imp {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {S : Set (L.withConstants ℕ).Sentenceω} (hS : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ S) (φ ψ : (L.withConstants ℕ).Sentenceω) (hmem : (BoundedFormulaω.imp φ ψ).not ∈ S) : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ (S ∪ {φ}) ∧ BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ (S ∪ {BoundedFormulaω.not ψ})

C1′. A conjunction of two insertions per label, so four gate applications.

theorem FirstOrder.Language.budgetedPairMem_C2_not_not {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {S : Set (L.withConstants ℕ).Sentenceω} (hS : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ S) (φ : (L.withConstants ℕ).Sentenceω) (hmem : (BoundedFormulaω.not φ).not ∈ S) : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ (S ∪ {φ})

C2.

The four countable-connective fields

The two ∀ k fields select the component up front; the two ∃ k fields unpack the gate's witness and return the same k, so the GenU, SentBnd and insertion obligations visibly concern one component. No witness is constructed here.

theorem FirstOrder.Language.budgetedPairMem_C3_iInf {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {S : Set (L.withConstants ℕ).Sentenceω} (hS : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ S) (φs : ℕ → (L.withConstants ℕ).Sentenceω) (hmem : BoundedFormulaω.iInf φs ∈ S) (k : ℕ) : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ (S ∪ {φs k})

C3.

theorem FirstOrder.Language.budgetedPairMem_C4_neg_iSup {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {S : Set (L.withConstants ℕ).Sentenceω} (hS : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ S) (φs : ℕ → (L.withConstants ℕ).Sentenceω) (hmem : (BoundedFormulaω.iSup φs).not ∈ S) (k : ℕ) : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ (S ∪ {BoundedFormulaω.not (φs k)})

C4′.

theorem FirstOrder.Language.budgetedPairMem_C4_iSup {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {S : Set (L.withConstants ℕ).Sentenceω} (hS : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ S) (φs : ℕ → (L.withConstants ℕ).Sentenceω) (hmem : BoundedFormulaω.iSup φs ∈ S) : ∃ (k : ℕ), BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ (S ∪ {φs k})

C4. The gate's witness is returned unchanged.

theorem FirstOrder.Language.budgetedPairMem_C3_neg_iInf {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {S : Set (L.withConstants ℕ).Sentenceω} (hS : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ S) (φs : ℕ → (L.withConstants ℕ).Sentenceω) (hmem : (BoundedFormulaω.iInf φs).not ∈ S) : ∃ (k : ℕ), BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ (S ∪ {BoundedFormulaω.not (φs k)})

C3′. The gate's witness is returned unchanged.

The equality fields

theorem FirstOrder.Language.budgetedPairMem_eq_refl {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {S : Set (L.withConstants ℕ).Sentenceω} (hS : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ S) (c : ℕ) : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ (S ∪ {constEq c c})

eq_refl. One case split suffices: if the left already carries c, insert there; otherwise c ∉ theoryJConsts Γ is exactly the right gate's second disjunct. The right support is never inspected.

theorem FirstOrder.Language.budgetedPairMem_eq_symm {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {S : Set (L.withConstants ℕ).Sentenceω} (hS : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ S) (a b : ℕ) (hmem : constEq a b ∈ S) : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ (S ∪ {constEq b a})

eq_symm.

theorem FirstOrder.Language.budgetedPairMem_eq_trans {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {S : Set (L.withConstants ℕ).Sentenceω} (hS : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ S) (a b d : ℕ) (hab : constEq a b ∈ S) (hbd : constEq b d ∈ S) : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ (S ∪ {constEq a d})

eq_trans. All four premise distributions, visibly. Note both mixed gates derive on Γ by eliminating a Γ-fresh remote endpoint — they are not mirrors indexed by receiving side — so three of the four cases insert on the left.

When the "remote" endpoint is not actually remote, the mixed gate does not apply: instead transfer the opposite side's equality onto Γ (legal, since it is quantifier-free and Γ already carries both its constants), apply the same-side gate, and drop the transferred premise with budgetedPairInsep_antitone_left.

theorem FirstOrder.Language.budgetedPairMem_rel_congr {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {S : Set (L.withConstants ℕ).Sentenceω} (hS : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ S) {l : ℕ} (Rr : L.Relations l) (g : Fin l → ℕ) (i : Fin l) (b : ℕ) (hrel : relInst Rr g ∈ S) (heq : constEq (g i) b ∈ S) : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ (S ∪ {relInst Rr (Function.update g i b)})

rel_congr. Four distributions. Same-side cases use the same-side gates; each mixed case splits on whether the replacement constant is fresh for the receiving side, and if it is not, transfers the equality across, applies the same-side gate, and drops the transferred premise with antitonicity. The transfer is legal because the atom supplies the pivot g i and the non-fresh branch supplies b.

theorem FirstOrder.Language.budgetedPairMem_all_inst {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {S : Set (L.withConstants ℕ).Sentenceω} (hS : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ S) (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) (hmem : φ.all ∈ S) (c : ℕ) : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ (S ∪ {instConst c φ})

all_inst. Plain label dispatch: neither gate takes a freshness hypothesis.

theorem FirstOrder.Language.budgetedPairMem_neg_all_witness {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} {S : Set (L.withConstants ℕ).Sentenceω} (hr₁ : (sentenceJConsts r₁).Finite) (hr₂ : (sentenceJConsts r₂).Finite) (hS : BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ S) (φ : (L.withConstants ℕ).BoundedFormulaω Empty 1) (hmem : φ.all.not ∈ S) : ∃ (c : ℕ), BudgetedPairMem r₁ r₂ F₁ R₁ F₂ R₂ (S ∪ {BoundedFormulaω.not (instConst c φ)})

neg_all_witness. The only helper that constructs anything: the witness constant is chosen before the label dispatch, since both gates demand freshness for both supports and the requirement is symmetric. This is also the only consumer of root-support finiteness, which is why those hypotheses appear here and nowhere else in the layer.

The initial family member

Two named facts, deliberately separate. The structural one is pure packaging: a labelled pair of singletons, with the generated universe instantiated at those very roots so both GenU obligations are literally root₁_mem/root₂_mem. The logical one supplies its hypothesis, and is where the interpolation assumption enters — note the root pair is inseparable because no admissible interpolant exists, not because of the entailment r₁ ⊨ r₂, which is consumed only at the very end against the extracted model.

theorem FirstOrder.Language.budgetedPairMem_root {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {ρ₁ ρ₂ : (L.withConstants ℕ).Sentenceω} (hb₁ : ρ₁ ∈ SentBnd F₁ R₁) (hb₂ : ρ₂ ∈ SentBnd F₂ R₂) (h : BudgetedPairInsep F₁ R₁ F₂ R₂ {ρ₁} {ρ₂}) : BudgetedPairMem ρ₁ ρ₂ F₁ R₁ F₂ R₂ ({ρ₁} ∪ {ρ₂})

Structural root member. Packaging only; no semantic content.

theorem FirstOrder.Language.budgetedPairInsep_root_of_no_interpolant {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} (hr₂ : ¬BoundedFormulaω.hasQuantSigned false r₂) (hc₁ : sentenceJConsts r₁ = ∅) (hno : ¬∃ (θ : (L.withConstants ℕ).Sentenceω), BoundedFormulaω.IsUniversal θ ∧ θ ∈ SentBnd (F₁ ∩ F₂) (R₁ ∩ R₂) ∧ sentenceJConsts θ = ∅ ∧ r₁.Entails θ ∧ θ.Entails r₂) : BudgetedPairInsep F₁ R₁ F₂ R₂ {r₁} {BoundedFormulaω.not r₂}

Root inseparability from failure of interpolation. The contrapositive of the root equation: if the labelled root pair were separable, the collapse would hand back exactly the admissible universal interpolant assumed not to exist.

theorem FirstOrder.Language.budgetedPairMem_root_of_no_interpolant {L : Language} {F₁ F₂ : Set ((n : ℕ) × L.Functions n)} {R₁ R₂ : Set ((n : ℕ) × L.Relations n)} {r₁ r₂ : (L.withConstants ℕ).Sentenceω} (hr₂ : ¬BoundedFormulaω.hasQuantSigned false r₂) (hc₁ : sentenceJConsts r₁ = ∅) (hb₁ : r₁ ∈ SentBnd F₁ R₁) (hb₂ : BoundedFormulaω.not r₂ ∈ SentBnd F₂ R₂) (hno : ¬∃ (θ : (L.withConstants ℕ).Sentenceω), BoundedFormulaω.IsUniversal θ ∧ θ ∈ SentBnd (F₁ ∩ F₂) (R₁ ∩ R₂) ∧ sentenceJConsts θ = ∅ ∧ r₁.Entails θ ∧ θ.Entails r₂) : BudgetedPairMem r₁ (BoundedFormulaω.not r₂) F₁ R₁ F₂ R₂ ({r₁} ∪ {BoundedFormulaω.not r₂})

The root member itself, assembled from the two facts above.

The consistency property

Pure wiring: every field is its named helper. Nothing below reasons about separators, labels or supports — if a field ever needs more than an application, the corresponding helper is missing.

def FirstOrder.Language.budgetedPairConsistencyProperty {L : Language} (F₁ : Set ((n : ℕ) × L.Functions n)) (R₁ : Set ((n : ℕ) × L.Relations n)) (F₂ : Set ((n : ℕ) × L.Functions n)) (R₂ : Set ((n : ℕ) × L.Relations n)) (r₁ r₂ : (L.withConstants ℕ).Sentenceω) (hr₁ : (sentenceJConsts r₁).Finite) (hr₂ : (sentenceJConsts r₂).Finite) : ConsistencyPropertyEqOn (GenU r₁ r₂)

The budgeted labelled-pair consistency property. The finite labelled family over the generated universe GenU r₁ r₂. Root-support finiteness is consumed only by neg_all_witness.

Equations

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