The logic action of S∞ = Equiv.Perm ℕ on the structure space (issue #27, algebraic layer)

The topology-free core of issue #27: S∞ = Equiv.Perm ℕ acts on StructureSpace L by relabeling the carrier, orbits coincide with decoded-structure isomorphism, and action-invariance coincides with the repository's IsomorphismInvariant.

Frozen convention (the inverse must be pinned before any invariance / measurable API is built on it): (σ • c) ⟨R, v⟩ = c ⟨R, σ⁻¹ ∘ v⟩. Then the orbit of c is exactly its decoded isomorphism class.

The Fin n analogue (Descriptive/FiniteCarrier.lean, permSmul/iso_iff_orbit) is the pilot; this is the ℕ-tier that issue #27 packages (and that #28 will build its σ-algebra on). The topology, Polish-group structure, and ContinuousSMul are the next milestones of #27, not here.

The action

@[implicit_reducible]

instance FirstOrder.Language.instSMulPermStructureSpace {L : Language} : SMul (Equiv.Perm ℕ) L.StructureSpace

S∞ = Equiv.Perm ℕ acts on StructureSpace L by relabeling the carrier: (σ • c) ⟨R, v⟩ = c ⟨R, σ⁻¹ ∘ v⟩.

Equations

• FirstOrder.Language.instSMulPermStructureSpace = { smul := fun (σ : Equiv.Perm ℕ) (c : L.StructureSpace) (q : L.RelQueryOn ℕ) => c ⟨q.fst, ⇑σ⁻¹ ∘ q.snd⟩ }

@[simp]

theorem FirstOrder.Language.logicAction_apply {L : Language} (σ : Equiv.Perm ℕ) (c : L.StructureSpace) (R : (l : ℕ) × L.Relations l) (v : Fin R.fst → ℕ) : (σ • c) ⟨R, v⟩ = c ⟨R, ⇑σ⁻¹ ∘ v⟩

@[implicit_reducible]

instance FirstOrder.Language.instMulActionPermNatStructureSpace {L : Language} : MulAction (Equiv.Perm ℕ) L.StructureSpace

Equations

• FirstOrder.Language.instMulActionPermNatStructureSpace = { toSMul := FirstOrder.Language.instSMulPermStructureSpace, mul_smul := ⋯, one_smul := ⋯ }

def FirstOrder.Language.ActionInvariant {L : Language} (B : Set L.StructureSpace) : Prop

Action invariance of a class of coded structures.

Equations

• FirstOrder.Language.ActionInvariant B = ∀ (σ : Equiv.Perm ℕ) (c : L.StructureSpace), c ∈ B ↔ σ • c ∈ B

Orbits are decoded-structure isomorphism

theorem FirstOrder.Language.orbit_iff_iso {L : Language} [L.IsRelational] (c d : L.StructureSpace) : (∃ (σ : Equiv.Perm ℕ), σ • c = d) ↔ Nonempty (L.Equiv ℕ ℕ)

Orbit = isomorphism: two codes lie in the same S∞-orbit iff their decoded structures are L-isomorphic.

Action invariance = isomorphism invariance

theorem FirstOrder.Language.actionInvariant_iff_isomorphismInvariant {L : Language} [L.IsRelational] (B : Set L.StructureSpace) : ActionInvariant B ↔ IsomorphismInvariant B

The equivalence (issue #27, milestone 10): action-invariance and isomorphism-invariance of a class of coded structures coincide.