The Swarm Simulator: A Dynamical Systems Model of Collective Intelligence Using the TO/TOGT Operator Pipeline
Version 3, September 2026 (corrections and formal checks)

Pablo Nogueira Grossi, G6 LLC, Newark, NJ. ORCID: 0009-0000-6496-2186
Versions: V1 10.5281/zenodo.19208284; V2 10.5281/zenodo.20230613; V3 (this deposit) 10.5281/zenodo.23027566.
Series root: 10.5281/zenodo.19117399. Formal-verification hub: github.com/TOTOGT/AXLE.

Abstract

The Swarm Simulator is a multi-agent dynamical system whose collective state X_t = (I_t, C_t, M_t, F_t) has four quantities: shared-intent stability, coordination efficiency, type-propagation multiplier and diffusion factor. Four collective operators, motivated by the generative operator pipeline G = U∘F∘K∘C of Topographical Orthogonal Generative Theory (TO/TOGT), govern its evolution. The agent-level pipeline is not formalised in this paper; the collective operators are taken as definitions.

Why version 3

Versions 1 and 2 stated a contraction theorem on R⁴ and a multi-orbit claim of distinct fixed points, and version 1 said that no numerical or unverifiable claims were made. Checking version 2 against Lean 4.32.0 and Mathlib v4.32.0 showed that its Lean file did not compile, that several of its theorems did not concern the swarm map, that Theorem 5.1 as printed is false, and that the two clusters of its multi-orbit figure were not contractive. Version 3 replaces the paper, the Lean file, the simulator and the open-questions table. The V1 and V2 texts are superseded.

What version 3 proves

Lean 4.32.0, Mathlib v4.32.0, no sorry, axioms propext, Classical.choice, Quot.sound only. Write a = f_types·f_agents·(1 − η), c = 1/(1 + D), m = (1 + β·reuse)·avg_quality.

• No global contraction. The map has no global Lipschitz constant, because C_t+1 = C_t·I_t+1/(1 + D) multiplies two state variables (no_global_lipschitz).
• Contraction on a ball. On ‖X‖ ≤ R the Lipschitz constant is λ(R) = max(a(1 + cR), m), which is below 1 for R < (1 − a)/(a·c). For the default parameters the radius is about 3.51 (step_lipschitz_ball, default_radius).
• Decay. ‖X_t‖ ≤ ρ(R)^t‖X₀‖ with ρ(R) = max(a, a·c·R, m). The printed bound L^t‖X₀‖ holds for ‖X₀‖ ≤ 1 and fails from (100, 10, 1) (orbit_nrm_le, paper_bound, printed_bound_fails).
• Fixed point. The only fixed point of (I, C, M) in the ball is 0, and two clusters that satisfy the ball condition share it (fixed_point_zero, two_clusters).
• Diffusion. F_t = 1 + αt has no upper bound, so the four-coordinate system has no fixed point (diffuse_unbounded).

Shared intent decays as I_t = I₀·a^t, the same law as a chain of steps that each hold with probability a.

What version 3 does not do

• No empirical calibration: the default parameters are not fitted to data.
• The multi-orbit claim of distinct fixed points is refuted for this model. A model with a source term would be needed.
• The agent-level pipeline G = U∘F∘K∘C is not formalised here.

Files

• swarm_simulator_v3.pdf, swarm_simulator_v3.tex: the revised paper, with figures/
• SwarmSimulator.lean: the Lean 4 proofs (build with lake build SwarmSimulator) and swarmsimulator.axioms.txt, the axiom report
• swarm_simulator.py: simulator and figures; python swarm_simulator.py --check runs ten numerical checks of the statements proved in Lean
• OPEN_QUESTIONS_SwarmSimulator.md and CHANGES_SwarmSimulator_V3.md

MSC codes: 37C25, 37D10, 47H10, 68T99. Keywords: swarm simulator, collective intelligence, TO/TOGT, contraction on a ball, fixed point, Lean 4.
License: CC BY-NC-ND 4.0 (paper), MIT (code). © 2026 Pablo Nogueira Grossi, G6 LLC.