Equivariance of the local EM quotient (the issue #11 spike)

An order automorphism e : J ≃o J acts on Λ[[J]]-terms by renaming skeleton constants (locJRename, via Mathlib's lhomWithConstantsMap). The spike question for the countably-many-types project: does the DEFINING semantic equivalence LocalEMEq of the local EM quotient commute with this action? The three test lemmas, in the order of risk:

• locJSupport_locJRename — the finite skeleton support maps by Finset.image e;
• deepRank_image_orderIso — the support's internal rank enumeration is invariant: an order automorphism preserves each element's rank in a finite support;
• locDeepInterp_locJRename — the deep interpretation of the renamed term over the renamed support EQUALS (not merely relates to) that of the original — pointwise in the depth d.

Consequently LocalEMEq_locJRename_iff: the setoid is preserved AND reflected by renaming — the two ∀ᶠ propositions are pointwise equal, so the critical gate of the spike holds with no reconstruction of semantic truth outside the quotient's defining fragment. The verdict is that the existing quotient (LocalEMContext.Carrier) is the correct vehicle for the induced automorphisms.

The packaging (issue #11 step 3) follows in the same file: functoriality of the renaming action (locJRename_refl/_trans/inverses), the descended carrier equivalence (LocalEMContext.carrierEquiv, computing on classes and sending [c_j] to [c_{e j}]), the targeted expanded-language equivariance (carrierEquiv_funMap under the renamed symbol, carrierEquiv_relMap for base relations), the acceptance theorem LocalEMContext.baseAutomorphism : Carrier ≃[Λ] Carrier over the base reduct structureBase, and the semantic endpoint realize_carrierEquiv: every base-language infinitary formula is invariant under the induced automorphism.

def FirstOrder.Language.locJRename (Λ : Language) (J : Type) [LinearOrder J] (e : J ≃o J) {α : Type} (t : (Λ.withConstants J).Term α) : (Λ.withConstants J).Term α

The skeleton-constant renaming action of an order automorphism on closed Λ[[J]]-terms.

Equations

• Λ.locJRename J e t = (Λ.lhomWithConstantsMap ⇑e).onTerm t

Functoriality of the renaming action

The descended automorphism of the local EM quotient

noncomputable def FirstOrder.Language.LocalEMContext.carrierEquiv {Λ : Language} {J : Type} [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) (e : J ≃o J) : Carrier Λ J ctx ≃ Carrier Λ J ctx

The descended carrier equivalence: an order automorphism of the skeleton acts on the local EM quotient by renaming representatives — well-defined by the equivariance gate.

Equations

• ctx.carrierEquiv e = Quotient.congr (FirstOrder.Language.locJRenameEquiv✝ e) ⋯

theorem FirstOrder.Language.LocalEMContext.carrierEquiv_mkClass {Λ : Language} {J : Type} [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) (e : J ≃o J) (t : (Λ.withConstants J).Term Empty) : (ctx.carrierEquiv e) (mkClass Λ J ctx t) = mkClass Λ J ctx (Λ.locJRename J e t)

theorem FirstOrder.Language.LocalEMContext.realize_carrierEquiv {Λ : Language} {J : Type} [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) (e : J ≃o J) {α : Type} {n : ℕ} (φ : Λ.BoundedFormulaω α n) (v : α → Carrier Λ J ctx) (xs : Fin n → Carrier Λ J ctx) : φ.Realize v xs ↔ φ.Realize (⇑(ctx.carrierEquiv e) ∘ v) (⇑(ctx.carrierEquiv e) ∘ xs)

The semantic endpoint of the packaging: every base-language infinitary formula is invariant under the induced automorphism.