Layer 7a: the schema-template Ω-witness bridge

The first, abstract chunk of the schema-level completion pivot (Layer 7). It connects a template-level witness property — TailTemplateOmegaWitnessed, the ⋁/⋀ witnessing of tailTemplateOfSeq a on the exact de-substituted formulas the source-side normal form uses — to LocalEMContext.OmegaCompleteForColim, the hard input of the local-EM realization tailTemplateRealizable_of_localEMContext.

The route deliberately goes through the existing LocalEMOmegaHomogeneous normal form, not directly to OmegaCompleteForColim: omegaCompleteForColim_of_omegaHomogeneous already converts LocalEMOmegaHomogeneous into OmegaCompleteForColim, so all this file must supply is TailTemplateOmegaWitnessed → LocalEMOmegaHomogeneous, shuttled across the tail-template truth collapse (IsLomega1omegaIndiscernibleOnTail.tailTemplateOfSeq_truth_iff): template truth of a canonDeForm ⇔ its eventual truth on the consecutive deep tuples k ↦ a (d+k).

No enumeration, Zorn, or term model appears here — this is the interface milestone that fixes the shape the ω-stage completion (Layer 7b) must produce.

structure FirstOrder.Language.TailTemplateOmegaWitnessed (s₀ : LocalStage) {M : Type} [(localColim s₀).Structure M] (a : ℕ → M) : Prop

The schema-template Ω-witness property. For the schema template tailTemplateOfSeq a, over the canonical de-substituted formulas of colimit-family connectives: a disjunction's template truth yields one component's template truth, and joint component template truth yields the conjunction's. This is the countable, J-free witnessing the ω-stage Henkin completion will establish; here it is the input to the normal-form bridge.

• iSup_witnessed {m : ℕ} (φs : ℕ → (localColim s₀).BoundedFormulaω Empty m) : ⟨m, BoundedFormulaω.iSup φs⟩ ∈ ΓlocalColim s₀ → ∀ {p : ℕ} (g : Fin m → (localColim s₀).Term (Fin p)), (tailTemplateOfSeq a).truth ((localColim s₀).canonDeForm (BoundedFormulaω.iSup φs) g) → ∃ (i : ℕ), (tailTemplateOfSeq a).truth ((localColim s₀).canonDeForm (φs i) g)

  A family disjunction's canonDeForm template-true ⟹ some component's is.

• iInf_witnessed {m : ℕ} (φs : ℕ → (localColim s₀).BoundedFormulaω Empty m) : ⟨m, BoundedFormulaω.iInf φs⟩ ∈ ΓlocalColim s₀ → ∀ {p : ℕ} (g : Fin m → (localColim s₀).Term (Fin p)), (∀ (i : ℕ), (tailTemplateOfSeq a).truth ((localColim s₀).canonDeForm (φs i) g)) → (tailTemplateOfSeq a).truth ((localColim s₀).canonDeForm (BoundedFormulaω.iInf φs) g)

  All components' canonDeForm template-true ⟹ the family conjunction's is.

theorem FirstOrder.Language.canonDeForm_mem_ΓEMlocal {s₀ : LocalStage} {m : ℕ} {φ : (localColim s₀).BoundedFormulaω Empty m} (hφ : ⟨m, φ⟩ ∈ ΓlocalColim s₀) {p : ℕ} (g : Fin m → (localColim s₀).Term (Fin p)) : ⟨p, (localColim s₀).canonDeForm φ g⟩ ∈ ΓEMlocal s₀

A canonical deForm of a colimit-family member lands in ΓEMlocal (its canonDeForms component).

theorem FirstOrder.Language.tailTemplate_truth_iff_eventually {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] {a : ℕ → M} (hTail : IsLomega1omegaIndiscernibleOnTail a (ΓEMlocal s₀)) {p : ℕ} {ψ : (localColim s₀).BoundedFormulaω Empty p} (hψ : ⟨p, ψ⟩ ∈ ΓEMlocal s₀) : (tailTemplateOfSeq a).truth ψ ↔ ∀ᶠ (d : ℕ) in Filter.atTop, ψ.Realize Empty.elim fun (k : Fin p) => a (d + ↑k)

The tail-template truth collapse (on the family ΓEMlocal): template truth of a member formula is exactly its eventual truth on the consecutive deep tuples k ↦ a (d+k). Forward is "consecutive tuples are strictly-monotone deep tuples"; backward is the tail indiscernibility (all sufficiently deep strict-mono tuples agree).

theorem FirstOrder.Language.TailTemplateOmegaWitnessed.to_localEMOmegaHomogeneous {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] {a : ℕ → M} (hTail : IsLomega1omegaIndiscernibleOnTail a (ΓEMlocal s₀)) (h : TailTemplateOmegaWitnessed s₀ a) : LocalEMOmegaHomogeneous s₀ a

The normal-form bridge: the schema-template Ω-witness property, plus tail indiscernibility of a on ΓEMlocal, implies the source-side normal form LocalEMOmegaHomogeneous. Each clause is shuttled across the truth collapse: eventual consecutive truth of the disjunction's deForm ⇒ its template truth ⇒ (witnessed) a component's template truth ⇒ its eventual consecutive truth. canonDeForm distributes over the connectives definitionally, so realize_iSup/realize_iInf move between the connective and its components.

theorem FirstOrder.Language.TailTemplateOmegaWitnessed.omegaCompleteForColim {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] {J : Type} [LinearOrder J] {a : ℕ → M} (hTail : IsLomega1omegaIndiscernibleOnTail a (ΓEMlocal s₀)) (h : TailTemplateOmegaWitnessed s₀ a) (ctx : (localColim s₀).LocalEMContext J) (hctxa : ctx.a = a) : LocalEMContext.OmegaCompleteForColim s₀ J ctx

The packaged corollary (the milestone): the schema-template Ω-witness property + tail indiscernibility deliver OmegaCompleteForColim for any LocalEMContext whose sequence is the schema sequence, by composing the normal-form bridge with the existing reduction theorem. This is exactly the hard input tailTemplateRealizable_of_localEMContext consumes.