The Polish logic action of S∞ on the structure space (issue #27, commit 3)

The capstone: the algebraic action of S∞ = Equiv.Perm ℕ on StructureSpace L (from LogicAction.lean) is jointly continuous for the pointwise topology on Equiv.Perm ℕ (PermPolishGroup.lean) and the existing product topology on StructureSpace L (Topology.lean) — packaged as a ContinuousSMul instance. Together with the Polish structures already in place this exhibits StructureSpace L as a Polish S∞-space.

Main results

• FirstOrder.Language.continuous_smul_action and the ContinuousSMul instance: the action (σ, c) ↦ σ • c is jointly continuous. No countability or relationality hypothesis is needed.
• FirstOrder.Language.isPolishSInftySpace: under [Countable (Σ l, L.Relations l)], StructureSpace L is a Polish S∞-space — Equiv.Perm ℕ is a Polish topological group, StructureSpace L is Polish, and the action is continuous.

Design

Joint continuity factors coordinatewise, exactly as anticipated: for a fixed relation query ⟨R, v⟩, the value (σ • c) ⟨R, v⟩ = c ⟨R, σ⁻¹ ∘ v⟩ reads c at a query whose tuple depends on σ through the finitely many continuous evaluations σ⁻¹ (v i). On the clopen neighborhood where those are frozen, the map reduces to a single continuous evaluation of c. The countability hypothesis for Polishness of StructureSpace L lives only in the final packaging — never on the action, the algebra, or the orbit equivalence.

theorem FirstOrder.Language.continuous_smul_query {L : Language} (R : (l : ℕ) × L.Relations l) (v : Fin R.fst → ℕ) : Continuous fun (p : Equiv.Perm ℕ × L.StructureSpace) => (p.1 • p.2) ⟨R, v⟩

Per-query continuity. For a fixed relation query ⟨R, v⟩, the map (σ, c) ↦ (σ • c) ⟨R, v⟩ is continuous: near (σ₀, c₀) the tuple σ⁻¹ ∘ v is frozen at i ↦ σ₀⁻¹ (v i) on a clopen neighborhood, where the map is the single evaluation c ↦ c ⟨R, m⟩.

theorem FirstOrder.Language.continuous_smul_action {L : Language} : Continuous fun (p : Equiv.Perm ℕ × L.StructureSpace) => p.1 • p.2

Joint continuity of the logic action (σ, c) ↦ σ • c.

instance FirstOrder.Language.instContinuousSMulPermStructureSpace {L : Language} : ContinuousSMul (Equiv.Perm ℕ) L.StructureSpace

The logic action of S∞ on StructureSpace L is jointly continuous.

theorem FirstOrder.Language.isPolishSInftySpace {L : Language} [Countable ((l : ℕ) × L.Relations l)] : PolishSpace (Equiv.Perm ℕ) ∧ IsTopologicalGroup (Equiv.Perm ℕ) ∧ PolishSpace L.StructureSpace ∧ ContinuousSMul (Equiv.Perm ℕ) L.StructureSpace

Packaged Polish S∞-space. For a countable relational vocabulary, StructureSpace L is a Polish S∞-space: Equiv.Perm ℕ is a Polish topological group, StructureSpace L is Polish, and the logic action is jointly continuous. The countability hypothesis appears here and nowhere upstream — the action, its MulAction laws, and the orbit/isomorphism identification are all hypothesis-free.