Carrier transport for infinitary formulas

Infinitary formulas fix one branching carrier per formula (Infinitary/Syntax.lean); this file provides the transport layer between carriers, along IndexCodings:

• BoundedFormulaInf.iInfAlong, iSupAlong: an ι-indexed conjunction/disjunction at a larger carrier κ, padding undecodable branches with ⊤/⊥ — semantically neutral (realize_iInfAlong, realize_iSupAlong).
• BoundedFormulaInf.reindex: whole-formula transport, functorial (reindex_id, reindex_trans — proved from the generic pad laws with no decoder analysis) and semantics-preserving (realize_reindex). Equivalence codings give genuine syntactic transport with an exact round trip (reindexEquiv); reindexing fixes the image of the finitary embedding (reindex_toInf), replacing the embedding triangle of a two-inductive design.
• BoundedFormulaInf.toOmega: recoding an encodable-carrier formula into L_{ω₁ω}.

Karp's theorem is the motivating consumer: its M-indexed and N-indexed separating conjunctions are iInfAlong at the two sum codings into the single carrier M ⊕ N.

def FirstOrder.Language.BoundedFormulaInf.iInfAlong {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : IndexCoding ι κ) (φs : ι → L.BoundedFormulaInf κ α n) : L.BoundedFormulaInf κ α n

An ι-indexed infinitary conjunction at carrier κ, along a coding: decoded indices select their conjunct, undecodable ones are padded with ⊤.

Equations

• FirstOrder.Language.BoundedFormulaInf.iInfAlong c φs = FirstOrder.Language.BoundedFormulaInf.iInf (c.pad ⊤ φs)

def FirstOrder.Language.BoundedFormulaInf.iSupAlong {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} (c : IndexCoding ι κ) (φs : ι → L.BoundedFormulaInf κ α n) : L.BoundedFormulaInf κ α n

An ι-indexed infinitary disjunction at carrier κ, along a coding: decoded indices select their disjunct, undecodable ones are padded with ⊥.

Equations

• FirstOrder.Language.BoundedFormulaInf.iSupAlong c φs = FirstOrder.Language.BoundedFormulaInf.iSup (c.pad ⊥ φs)

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_iInfAlong {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M} {c : IndexCoding ι κ} {φs : ι → L.BoundedFormulaInf κ α n} : (iInfAlong c φs).Realize v xs ↔ ∀ (i : ι), (φs i).Realize v xs

The ⊤-padding of a coded conjunction is semantically neutral, generically in the coding.

@[simp]

theorem FirstOrder.Language.BoundedFormulaInf.realize_iSupAlong {L : Language} {ι : Type uι} {κ : Type uκ} {α : Type u'} {n : ℕ} {M : Type w} [L.Structure M] {v : α → M} {xs : Fin n → M} {c : IndexCoding ι κ} {φs : ι → L.BoundedFormulaInf κ α n} : (iSupAlong c φs).Realize v xs ↔ ∃ (i : ι), (φs i).Realize v xs

The ⊥-padding of a coded disjunction is semantically neutral, generically in the coding.