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

theorem FirstOrder.Language.locJConstOf_lhomWithConstantsMap (Λ : Language) (J : Type) [LinearOrder J] (e : J ≃o J) {n : ℕ} (f : (Λ.withConstants J).Functions n) : Λ.locJConstOf J ((Λ.lhomWithConstantsMap ⇑e).onFunction f) = Finset.image (⇑e) (Λ.locJConstOf J f)

Renaming carries each function symbol's skeleton constant by Finset.image e.

theorem FirstOrder.Language.locJSupport_locJRename (Λ : Language) (J : Type) [LinearOrder J] (e : J ≃o J) {α : Type} (t : (Λ.withConstants J).Term α) : Λ.locJSupport J (Λ.locJRename J e t) = Finset.image (⇑e) (Λ.locJSupport J t)

Test lemma 1: the skeleton support of the renamed term is the image of the support.

theorem FirstOrder.Language.deepRank_image_orderIso (J : Type) [LinearOrder J] (e : J ≃o J) (S : Finset J) (j : J) : deepRank J (Finset.image (⇑e) S) (e j) = deepRank J S j

Test lemma 2: an order automorphism preserves the internal rank enumeration of a finite support: the rank of e j in S.image e is the rank of j in S.

theorem FirstOrder.Language.constantsToVars_locJRename (Λ : Language) (J : Type) [LinearOrder J] (e : J ≃o J) {α : Type} (t : (Λ.withConstants J).Term α) : (Λ.locJRename J e t).constantsToVars = Term.relabel (Sum.map (⇑e) id) t.constantsToVars

De-substitution intertwines skeleton renaming with variable relabeling: the constantsToVars of the renamed term is the relabel of the original's along Sum.map e id.

theorem FirstOrder.Language.locDeepInterp_locJRename (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (a : ℕ → M) (e : J ≃o J) (d : ℕ) (S : Finset J) (t : (Λ.withConstants J).Term Empty) : Λ.locDeepInterp J a d (Finset.image (⇑e) S) (Λ.locJRename J e t) = Λ.locDeepInterp J a d S t

Test lemma 3: the deep interpretation of the renamed term over the image support equals that of the original term over the original support — pointwise in the depth d, not merely eventually.

theorem FirstOrder.Language.LocalEMEq_locJRename_iff (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (a : ℕ → M) (e : J ≃o J) (t u : (Λ.withConstants J).Term Empty) : Λ.LocalEMEq J a (Λ.locJRename J e t) (Λ.locJRename J e u) ↔ Λ.LocalEMEq J a t u

The critical gate: the defining semantic equivalence of the local EM quotient is preserved AND reflected by skeleton renaming — the two eventual equalities are pointwise equivalent propositions. The existing quotient is equivariant.

theorem FirstOrder.Language.LocalEMContext.setoid_locJRename_iff (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) (e : J ≃o J) (t u : (Λ.withConstants J).Term Empty) : (setoid Λ J ctx) (Λ.locJRename J e t) (Λ.locJRename J e u) ↔ (setoid Λ J ctx) t u

The setoid form of the gate, for a full local EM context: renamed representatives are related exactly when the originals are.

Functoriality of the renaming action

theorem FirstOrder.Language.locJRename_refl {Λ : Language} {J : Type} [LinearOrder J] {α : Type} (t : (Λ.withConstants J).Term α) : Λ.locJRename J (OrderIso.refl J) t = t

theorem FirstOrder.Language.locJRename_trans {Λ : Language} {J : Type} [LinearOrder J] (e₁ e₂ : J ≃o J) {α : Type} (t : (Λ.withConstants J).Term α) : Λ.locJRename J e₂ (Λ.locJRename J e₁ t) = Λ.locJRename J (e₁.trans e₂) t

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

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

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

The renaming action as an equivalence of closed terms.

Equations

• FirstOrder.Language.locJRenameEquiv e = { toFun := Λ.locJRename J e, invFun := Λ.locJRename J e.symm, left_inv := ⋯, right_inv := ⋯ }

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.carrierEquiv_const {Λ : Language} {J : Type} [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) (e : J ≃o J) (j : J) : (ctx.carrierEquiv e) (mkClass Λ J ctx (func (Sum.inr j) Fin.elim0)) = mkClass Λ J ctx (func (Sum.inr (e j)) Fin.elim0)

The skeleton-class equation: the descended automorphism sends the class of the skeleton constant c_j to the class of c_{e j}.

theorem FirstOrder.Language.LocalEMContext.carrierEquiv_funMap {Λ : Language} {J : Type} [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) (e : J ≃o J) {n : ℕ} (f : (Λ.withConstants J).Functions n) (xs : Fin n → Carrier Λ J ctx) : (ctx.carrierEquiv e) (Structure.funMap f xs) = Structure.funMap ((Λ.lhomWithConstantsMap ⇑e).onFunction f) fun (i : Fin n) => (ctx.carrierEquiv e) (xs i)

Equivariance of function interpretation under the language renaming induced by e: the targeted expanded-language fact (the base-reduct automorphism consumes its Sum.inl case).

theorem FirstOrder.Language.LocalEMContext.carrierEquiv_relMap {Λ : Language} {J : Type} [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) (e : J ≃o J) {n : ℕ} (R : Λ.Relations n) (xs : Fin n → Carrier Λ J ctx) : (Structure.RelMap (Sum.inl R) fun (i : Fin n) => (ctx.carrierEquiv e) (xs i)) ↔ Structure.RelMap (Sum.inl R) xs

Equivariance of base-relation interpretation: the descended map preserves and reflects every base relation — via the pointwise deep-interpretation equality over the image support.

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

The acceptance theorem: the descended equivalence is a genuine automorphism of the base-language (Λ-reduct) structure on the local EM carrier — every order automorphism of the skeleton induces a structure automorphism sending [c_j] to [c_{e j}] (carrierEquiv_const).

Equations

• ctx.baseAutomorphism e = { toEquiv := ctx.carrierEquiv e, map_fun' := ⋯, map_rel' := ⋯ }

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.