The constant-support calculus for a constant expansion L[[J]] (issue #8 kernel step 2)

The neutral home of the syntactic constant-support machinery, moved and generalized from Methods/MarkerStage.lean (its Layers 2/5 discovered the finite-support problem: an L_{ω₁ω} formula can mention infinitely many constants — ⋁ₙ (dₙ = dₙ) has support all of ℕ — so freshness arguments must CARRY a finite support rather than compute one). Craig interpolation (#8) consumes the same calculus for its InsepAt-parameterized separators.

• the generic functionsIn structural lemmas (relabel / castLE / subst / openBounds / finiteness), verbatim from MarkerStage;
• sentenceJConsts — the constant support of an L'[[J]]-formula — with its monotonicity calculus, verbatim from MarkerStage;
• NEW: term-level support (Term.jConsts), the constant closed term (constTerm), instantiation support bounds, the base-symbol projections (baseFunctionsIn / baseRelationsIn), and stripConsts — a constant-free expansion formula restricts to the base language, with mapLanguage (lhomWithConstants) as left inverse and occurrence transport (the A = ∅ root gate of the interpolation argument).

Structural lemmas for functionsIn (relabel / castLE / subst / openBounds)

The mentioned function symbols are stable under variable renamings and grow only by the substituted terms' symbols under substitution. Generic over the language.

theorem FirstOrder.Language.Term.functionsIn_relabel {L : Language} {α β : Type} (g : α → β) (t : L.Term α) : (relabel g t).functionsIn = t.functionsIn

theorem FirstOrder.Language.Term.functionsIn_subst {L : Language} {α β : Type} (tf : α → L.Term β) (t : L.Term α) : (t.subst tf).functionsIn ⊆ t.functionsIn ∪ ⋃ (a : α), (tf a).functionsIn

theorem FirstOrder.Language.BoundedFormulaω.functionsIn_castLE {L : Language} {α : Type} {m n : ℕ} (h : m ≤ n) (φ : L.BoundedFormulaω α m) : (castLE h φ).functionsIn = φ.functionsIn

theorem FirstOrder.Language.BoundedFormulaω.functionsIn_relabel {L : Language} {α β : Type} {n : ℕ} (g : α → β ⊕ Fin n) {k : ℕ} (φ : L.BoundedFormulaω α k) : (relabel g φ).functionsIn = φ.functionsIn

theorem FirstOrder.Language.BoundedFormulaω.relationsIn_castLE {L : Language} {α : Type} {m n : ℕ} (h : m ≤ n) (φ : L.BoundedFormulaω α m) : (castLE h φ).relationsIn = φ.relationsIn

theorem FirstOrder.Language.BoundedFormulaω.relationsIn_relabel {L : Language} {α β : Type} {n : ℕ} (g : α → β ⊕ Fin n) {k : ℕ} (φ : L.BoundedFormulaω α k) : (relabel g φ).relationsIn = φ.relationsIn

theorem FirstOrder.Language.BoundedFormulaω.functionsIn_subst {L : Language} {α β : Type} (tf : α → L.Term β) {k : ℕ} (φ : L.BoundedFormulaω α k) : (φ.subst tf).functionsIn ⊆ φ.functionsIn ∪ ⋃ (a : α), (tf a).functionsIn

theorem FirstOrder.Language.BoundedFormulaω.functionsIn_openBounds {L : Language} {n : ℕ} (φ : L.BoundedFormulaω Empty n) : functionsIn φ.openBounds = φ.functionsIn

theorem FirstOrder.Language.Term.functionsIn_finite {L : Language} {α : Type} (t : L.Term α) : t.functionsIn.Finite

A term mentions only finitely many function symbols (it is a finite tree).

theorem FirstOrder.Language.Term.functionsIn_subset_subst {L : Language} {α β : Type} (tf : α → L.Term β) (t : L.Term α) : t.functionsIn ⊆ (t.subst tf).functionsIn

Substitution only adds symbols: φ's own symbols survive (only variables are replaced).

theorem FirstOrder.Language.BoundedFormulaω.functionsIn_subset_subst {L : Language} {α β : Type} (tf : α → L.Term β) {k : ℕ} (φ : L.BoundedFormulaω α k) : φ.functionsIn ⊆ (φ.subst tf).functionsIn

theorem FirstOrder.Language.BoundedFormulaω.functionsIn_not {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) : φ.not.functionsIn = φ.functionsIn

Negation does not change the mentioned function symbols (not is imp · ⊥).

theorem FirstOrder.Language.BoundedFormulaω.functionsIn_ex {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α (n + 1)) : φ.ex.functionsIn = φ.functionsIn

Existential quantification (¬∀¬) does not change the mentioned function symbols.

theorem FirstOrder.Language.BoundedFormulaω.relationsIn_not {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α n) : φ.not.relationsIn = φ.relationsIn

Negation does not change the mentioned relation symbols.

theorem FirstOrder.Language.BoundedFormulaω.relationsIn_ex {L : Language} {α : Type} {n : ℕ} (φ : L.BoundedFormulaω α (n + 1)) : φ.ex.relationsIn = φ.relationsIn

Existential quantification does not change the mentioned relation symbols.

theorem FirstOrder.Language.BoundedFormulaω.functionsIn_existsBlock {L : Language} {α : Type} {n k : ℕ} (φ : L.BoundedFormulaω α (n + k)) : φ.existsBlock.functionsIn = φ.functionsIn

A finite existential block does not change the mentioned function symbols.

theorem FirstOrder.Language.BoundedFormulaω.relationsIn_existsBlock {L : Language} {α : Type} {n k : ℕ} (φ : L.BoundedFormulaω α (n + k)) : φ.existsBlock.relationsIn = φ.relationsIn

A finite existential block does not change the mentioned relation symbols.

theorem FirstOrder.Language.BoundedFormulaω.functionsIn_forallBlock {L : Language} {α : Type} {n k : ℕ} (φ : L.BoundedFormulaω α (n + k)) : φ.forallBlock.functionsIn = φ.functionsIn

A finite universal block does not change the mentioned function symbols.

theorem FirstOrder.Language.BoundedFormulaω.relationsIn_forallBlock {L : Language} {α : Type} {n k : ℕ} (φ : L.BoundedFormulaω α (n + k)) : φ.forallBlock.relationsIn = φ.relationsIn

A finite universal block does not change the mentioned relation symbols.

theorem FirstOrder.Language.BoundedFormulaω.functionsIn_top {L : Language} {α : Type} {n : ℕ} : ⊤.functionsIn = ∅

The true formula mentions no function symbols.

theorem FirstOrder.Language.BoundedFormulaω.relationsIn_top {L : Language} {α : Type} {n : ℕ} : ⊤.relationsIn = ∅

The true formula mentions no relation symbols.

theorem FirstOrder.Language.BoundedFormulaω.functionsIn_and {L : Language} {α : Type} {n : ℕ} (φ ψ : L.BoundedFormulaω α n) : (φ.and ψ).functionsIn = φ.functionsIn ∪ ψ.functionsIn

Binary conjunction collects both sides' function symbols.

theorem FirstOrder.Language.BoundedFormulaω.relationsIn_and {L : Language} {α : Type} {n : ℕ} (φ ψ : L.BoundedFormulaω α n) : (φ.and ψ).relationsIn = φ.relationsIn ∪ ψ.relationsIn

Binary conjunction collects both sides' relation symbols.

theorem FirstOrder.Language.BoundedFormulaω.functionsIn_einf {L : Language} {α : Type} {ι : Type u_1} [Encodable ι] {n : ℕ} (φs : ι → L.BoundedFormulaω α n) : (einf φs).functionsIn = ⋃ (i : ι), (φs i).functionsIn

An Encodable-indexed conjunction collects the branches' function symbols (the ⊤ padding of undecodable indices contributes nothing).

theorem FirstOrder.Language.BoundedFormulaω.relationsIn_einf {L : Language} {α : Type} {ι : Type u_1} [Encodable ι] {n : ℕ} (φs : ι → L.BoundedFormulaω α n) : (einf φs).relationsIn = ⋃ (i : ι), (φs i).relationsIn

An Encodable-indexed conjunction collects the branches' relation symbols.

theorem FirstOrder.Language.BoundedFormulaω.functionsIn_of_isRelational {L' : Language} [L'.IsRelational] {α : Type} {n : ℕ} (φ : L'.BoundedFormulaω α n) : φ.functionsIn = ∅

In a relational language no formula mentions a function symbol.

theorem FirstOrder.Language.Term.realize_congr_functionsIn {L : Language} {M : Type} (S S' : L.Structure M) {γ : Type} (t : L.Term γ) : (∀ p ∈ t.functionsIn, ∀ (x : Fin p.fst → M), Structure.funMap p.snd x = Structure.funMap p.snd x) → ∀ (v : γ → M), realize v t = realize v t

Occurrence-aware term-realization congruence: two structure instances agreeing on the function symbols occurring in t realize t identically.

theorem FirstOrder.Language.BoundedFormulaω.realize_congr_symbolsIn {L : Language} {α M : Type} (S S' : L.Structure M) {n : ℕ} (φ : L.BoundedFormulaω α n) : (∀ p ∈ φ.functionsIn, ∀ (x : Fin p.fst → M), Structure.funMap p.snd x = Structure.funMap p.snd x) → (∀ p ∈ φ.relationsIn, ∀ (x : Fin p.fst → M), Structure.RelMap p.snd x ↔ Structure.RelMap p.snd x) → ∀ (v : α → M) (xs : Fin n → M), φ.Realize v xs ↔ φ.Realize v xs

Occurrence-aware realization congruence: two structure instances agreeing on the symbols occurring in φ realize φ identically. The tool that localizes semantic transport to a formula's own vocabulary.

Constant support of a constant-expansion formula

def FirstOrder.Language.sentenceJConsts {L' : Language} {J α : Type} {n : ℕ} (φ : (L'.withConstants J).BoundedFormulaω α n) : Set J

The syntactic constant support of an L'[[J]]-formula: the added constants (arity-0 Sum.inr function symbols) among its mentioned symbols. Only countable in general (functionsIn_countable — countably-branching connectives); freshness arguments demand containment in a finite set rather than computing one. Generic in the base language, so it also serves iterated expansion layers (L := L'[[J]], constants ℕ).

Equations

• FirstOrder.Language.sentenceJConsts φ = {j : J | ⟨0, Sum.inr j⟩ ∈ φ.functionsIn}

theorem FirstOrder.Language.sentenceJConsts_not {L' : Language} {J α : Type} {n : ℕ} (φ : (L'.withConstants J).BoundedFormulaω α n) : sentenceJConsts φ.not = sentenceJConsts φ

Negation does not change the constant support (not is imp · falsum).

theorem FirstOrder.Language.sentenceJConsts_component_iInf {L' : Language} {J α : Type} {n : ℕ} (φs : ℕ → (L'.withConstants J).BoundedFormulaω α n) (k : ℕ) : sentenceJConsts (φs k) ⊆ sentenceJConsts (BoundedFormulaω.iInf φs)

A conjunction component's constant support is contained in the conjunction's.

theorem FirstOrder.Language.sentenceJConsts_component_iSup {L' : Language} {J α : Type} {n : ℕ} (φs : ℕ → (L'.withConstants J).BoundedFormulaω α n) (k : ℕ) : sentenceJConsts (φs k) ⊆ sentenceJConsts (BoundedFormulaω.iSup φs)

A disjunction component's constant support is contained in the disjunction's.

theorem FirstOrder.Language.sentenceJConsts_imp_left {L' : Language} {J α : Type} {n : ℕ} (φ ψ : (L'.withConstants J).BoundedFormulaω α n) : sentenceJConsts φ ⊆ sentenceJConsts (φ.imp ψ)

An implication's antecedent support is contained in the implication's.

theorem FirstOrder.Language.sentenceJConsts_imp_right {L' : Language} {J α : Type} {n : ℕ} (φ ψ : (L'.withConstants J).BoundedFormulaω α n) : sentenceJConsts ψ ⊆ sentenceJConsts (φ.imp ψ)

An implication's consequent support is contained in the implication's.

def FirstOrder.Language.Term.jConsts {L' : Language} {J β : Type} (t : (L'.withConstants J).Term β) : Set J

The constant support of an expansion term.

Equations

• t.jConsts = {j : J | ⟨0, Sum.inr j⟩ ∈ t.functionsIn}

def FirstOrder.Language.constTerm {L' : Language} {J : Type} (j : J) : (L'.withConstants J).Term Empty

The j-th constant of the expansion, as a closed term.

Equations

• FirstOrder.Language.constTerm j = FirstOrder.Language.func (Sum.inr j) Fin.elim0

theorem FirstOrder.Language.constTerm_functionsIn {L' : Language} {J : Type} (j : J) : (constTerm j).functionsIn = {⟨0, Sum.inr j⟩}

theorem FirstOrder.Language.sentenceJConsts_openBounds {L' : Language} {J : Type} {n : ℕ} (φ : (L'.withConstants J).BoundedFormulaω Empty n) : sentenceJConsts φ.openBounds = sentenceJConsts φ

openBounds does not change the constant support.

theorem FirstOrder.Language.sentenceJConsts_ex {L' : Language} {J α : Type} {n : ℕ} (φ : (L'.withConstants J).BoundedFormulaω α (n + 1)) : sentenceJConsts φ.ex = sentenceJConsts φ

Existential quantification does not change the constant support.

theorem FirstOrder.Language.sentenceJConsts_subst_constTerm {L' : Language} {J : Type} (φ : (L'.withConstants J).Formulaω (Fin 1)) (j : J) : sentenceJConsts (BoundedFormulaω.subst φ fun (x : Fin 1) => constTerm j) ⊆ sentenceJConsts φ ∪ {j}

Instantiation support bound: substituting the constant j into a one-variable formula adds at most j to the constant support.

def FirstOrder.Language.BoundedFormulaω.baseFunctionsIn {L' : Language} {J α : Type} {n : ℕ} (φ : (L'.withConstants J).BoundedFormulaω α n) : Set ((n : ℕ) × L'.Functions n)

The base function symbols of an expansion formula (the Sum.inl layer).

Equations

• φ.baseFunctionsIn = {s : (n : ℕ) × L'.Functions n | ⟨s.fst, Sum.inl s.snd⟩ ∈ φ.functionsIn}

def FirstOrder.Language.BoundedFormulaω.baseRelationsIn {L' : Language} {J α : Type} {n : ℕ} (φ : (L'.withConstants J).BoundedFormulaω α n) : Set ((n : ℕ) × L'.Relations n)

The base relation symbols of an expansion formula (the constant layer adds none).

Equations

• φ.baseRelationsIn = {s : (n : ℕ) × L'.Relations n | ⟨s.fst, Sum.inl s.snd⟩ ∈ φ.relationsIn}

Stripping constant-free formulas to the base language

A constant-free L'[[J]]-formula is (the mapLanguage-image of) a base formula. This is the A = ∅ root gate of the interpolation argument: a separator with empty allowed support strips to an interpolant of the base language.

def FirstOrder.Language.Term.stripConsts {L' : Language} {J β : Type} (t : (L'.withConstants J).Term β) : t.jConsts ⊆ ∅ → L'.Term β

Strip a constant-free expansion term to the base language.

Equations

• (FirstOrder.Language.var x_2).stripConsts x_3 = FirstOrder.Language.var x_2
• (FirstOrder.Language.func (Sum.inl f) ts).stripConsts h = FirstOrder.Language.func f fun (i : Fin l) => (ts i).stripConsts ⋯
• (FirstOrder.Language.func (Sum.inr c) _ts).stripConsts h = absurd ⋯ ⋯

theorem FirstOrder.Language.Term.onTerm_stripConsts {L' : Language} {J β : Type} (t : (L'.withConstants J).Term β) (h : t.jConsts ⊆ ∅) : (L'.lhomWithConstants J).onTerm (t.stripConsts h) = t

The withConstants inclusion is a left inverse of term stripping.

theorem FirstOrder.Language.Term.functionsIn_stripConsts {L' : Language} {J β : Type} (t : (L'.withConstants J).Term β) (h : t.jConsts ⊆ ∅) : (t.stripConsts h).functionsIn ⊆ {s : (n : ℕ) × L'.Functions n | ⟨s.fst, Sum.inl s.snd⟩ ∈ t.functionsIn}

Occurrence transport for term stripping: the stripped term's symbols are the base symbols of the original.

def FirstOrder.Language.BoundedFormulaω.stripConsts {L' : Language} {J α : Type} {n : ℕ} (φ : (L'.withConstants J).BoundedFormulaω α n) : sentenceJConsts φ ⊆ ∅ → L'.BoundedFormulaω α n

Strip a constant-free expansion formula to the base language.

Equations

• FirstOrder.Language.BoundedFormulaω.falsum.stripConsts x_4 = FirstOrder.Language.BoundedFormulaω.falsum
• (FirstOrder.Language.BoundedFormulaω.equal t u).stripConsts h = FirstOrder.Language.BoundedFormulaω.equal (t.stripConsts ⋯) (u.stripConsts ⋯)
• (FirstOrder.Language.BoundedFormulaω.rel (Sum.inl R) ts).stripConsts h = FirstOrder.Language.BoundedFormulaω.rel R fun (i : Fin l) => (ts i).stripConsts ⋯
• (φ.imp ψ).stripConsts h = (φ.stripConsts ⋯).imp (ψ.stripConsts ⋯)
• φ.all.stripConsts h = (φ.stripConsts h).all
• (FirstOrder.Language.BoundedFormulaω.iSup φs).stripConsts h = FirstOrder.Language.BoundedFormulaω.iSup fun (i : ℕ) => (φs i).stripConsts ⋯
• (FirstOrder.Language.BoundedFormulaω.iInf φs).stripConsts h = FirstOrder.Language.BoundedFormulaω.iInf fun (i : ℕ) => (φs i).stripConsts ⋯

theorem FirstOrder.Language.BoundedFormulaω.universalSigned_stripConsts {L' : Language} {J α : Type} (s : Bool) {n : ℕ} (φ : (L'.withConstants J).BoundedFormulaω α n) (h : sentenceJConsts φ ⊆ ∅) : universalSigned s (φ.stripConsts h) ↔ universalSigned s φ

Quantifier class is invariant under stripping constants. stripConsts rewrites only terms and the relation tag; it touches no quantifier node, so the signed universal class is exact.

theorem FirstOrder.Language.BoundedFormulaω.mapLanguage_stripConsts {L' : Language} {J α : Type} {n : ℕ} (φ : (L'.withConstants J).BoundedFormulaω α n) (h : sentenceJConsts φ ⊆ ∅) : mapLanguage (L'.lhomWithConstants J) (φ.stripConsts h) = φ

The withConstants inclusion is a left inverse of formula stripping.

theorem FirstOrder.Language.BoundedFormulaω.functionsIn_stripConsts {L' : Language} {J α : Type} {n : ℕ} (φ : (L'.withConstants J).BoundedFormulaω α n) (h : sentenceJConsts φ ⊆ ∅) : (φ.stripConsts h).functionsIn ⊆ φ.baseFunctionsIn

Occurrence transport for formula stripping (function symbols).

theorem FirstOrder.Language.BoundedFormulaω.relationsIn_stripConsts {L' : Language} {J α : Type} {n : ℕ} (φ : (L'.withConstants J).BoundedFormulaω α n) (h : sentenceJConsts φ ⊆ ∅) : (φ.stripConsts h).relationsIn ⊆ φ.baseRelationsIn

Occurrence transport for formula stripping (relation symbols).