Miranda Dynamics Program
The Central Question
Can physical dynamical systems perform arbitrary computation? Miranda's program proves yes on two fronts: (1) Billiards — the TKFT framework shows billiard systems are Turing complete via Cantor encoding, with reaching relations forming a category, empirically validated against seismic data at 92.86% accuracy. (2) Navier-Stokes fluids — cosymplectic geometry produces harmonic Reeb fields that solve NS at every viscosity via the Etnyre-Ghrist correspondence, making trajectory prediction and periodicity detection undecidable.
Original Researcher
Departament de Matematiques, UPC Barcelona. PNAS 2021, Advances in Mathematics.
Scientific Context
The connection between dynamical systems and computation has deep roots: Moore (1990) showed certain fluid flows can simulate Turing machines, and Koiran and Moore (1999) extended this to polynomial maps. Miranda's program proves two pillars: billiard systems are Turing complete via Cantor encoding (TKFT), and Navier-Stokes fluids are Turing complete via cosymplectic geometry and the Etnyre-Ghrist correspondence.
Pillar 1 — TKFT layers: (1) Geometry — polygonal billiard tables with elastic reflections, (2) Dynamics — continuous evolution with collision events preserving energy, (3) Encoding — Cantor injection mapping discrete tape states into continuous phase space, (4) Validation — predictions tested against IRIS/USGS seismic data.
Pillar 2 — Fluids chain: Cosymplectic structure (α closed, ω closed, volume form) → harmonic Reeb field → Etnyre-Ghrist correspondence (rotational Beltrami ↔ Reeb up to reparametrization) → viscosity-invariant stationary NS solutions (ΔX = 0 ⇒ ν·ΔX = 0) → halting reduction → undecidable trajectory prediction and periodicity detection.
What formalization provides: Billiards: reaching relations form a category (associative composition), Cantor encoding is injective, observable reaching is compositional, seismic validation achieves 92.86% accuracy. Fluids: Beltrami periodicity transfers to Reeb via calc proof, trajectory and periodicity undecidability via ManyOne reduction from halting, periodicity nucleus carries Mathlib Nucleus structure.
Layer 1: The Mathematical Ground Truth
A billiard system consists of a compact polygonal table Ω ⊂ ℝ² with a point particle moving at constant speed, reflecting elastically off boundaries. The state space is S = Ω × S¹ (position × velocity direction).
- BilliardState: (px, py, vx, vy) ∈ ℝ² × ℝ²
- evolve(A, t): continuous-time evolution with elastic reflections
- reaches(A, B): ∃t. evolve(A, t) = B
- comp(R, S): relational composition — {(a,c) | ∃b. R(a,b) ∧ S(b,c)}
The Cantor encoding maps Turing machine tape states injectively into billiard configurations. The encoding preserves computational structure: a transition in the TM corresponds to an evolution segment in the billiard:
- encode: TapeState ↪ BilliardState (injective)
- billiard_turing_complete: billiard systems simulate any Turing machine
- comp_assoc: reaching relation composition is associative
- collision_energy_invariant: elastic collisions preserve kinetic energy
Reaching.lean — reaches, observableReaches, categorical composition
CantorEncoding.lean — cantor_encoding_injective, TapeState ↪ BilliardState
Dynamics.lean — evolve, collision handling, energy invariant
Observable.lean — observable_comp, observation parameters
Layer 2: Seismic Empirical Validation
The TKFT framework is validated against real seismic data from IRIS/USGS earthquake catalogs. The model predicts reaching relations between seismological stations using the ak135 travel-time model:
VALIDATION RESULTS
M6.0+ earthquakes from the IRIS/USGS global catalog. Travel-time predictions using the ak135 1D velocity model. 92.86% of station-pair reaching predictions match observed arrivals within tolerance. The 7.14% Heyting gap represents cases where the model's idealized geometry diverges from Earth's heterogeneous interior.
FOUR TKFT LAYERS
Layer 1 (Geometry): polygonal table boundaries with elastic reflections. Layer 2 (Dynamics): continuous evolution with discrete collision events. Layer 3 (Encoding): Cantor map from tape states to billiard configurations. Layer 4 (Validation): seismic travel-time predictions vs. observed data.
Project Phases
158 modules formalizing billiard geometry, dynamics/evolution, reaching relations with categorical composition, Cantor encoding, observable reaching, and seismic validation bridge. All theorems proved without sorry/admit.
- ▸comp_assoc: reaching relation composition is associative
- ▸billiard_turing_complete: billiard systems are Turing complete
- ▸cantor_encoding_injective: tape state encoding is injective
- ▸seismic_accuracy_92_86: 92.86% validated on M6.0+ earthquakes
5 modules formalizing Navier-Stokes Turing completeness via cosymplectic geometry and the Etnyre-Ghrist correspondence. 12 structures, 4 proved theorems. Zero sorry, zero axiom. Hostile audit: CLEAN, 0 findings.
- ▸periodic_reeb_of_beltrami_periodic: Beltrami periodicity transfers to Reeb
- ▸fluid_trajectory_undecidable: trajectory prediction is not computable
- ▸fluid_periodicity_undecidable: periodicity detection is not computable
- ▸fluidPeriodicNucleus_fixed_iff: nucleus fixed points = supersets of periodic region
Faithful translation of both pillars to verified C (gcc -Wall -Wextra -Werror: 0 warnings) and safe Rust (cargo test: 8/8 pass). Both billiard and fluids modules transpiled.
- ▸gcc -std=c11 -Wall -Wextra -Werror: PASS (both pillars)
- ▸cargo build: 0 warnings
- ▸cargo test: 8/8 pass (4 billiards + 4 fluids)
- ▸BilliardState + ContactFormData + EtnyreGhrist structs match Lean
All artifacts content-addressed and pinned to IPFS. Lean proofs, verified C, safe Rust archives with CIDv1 identifiers.
- ▸Lean archive: 11 key source files
- ▸C archive: 2 translation units
- ▸Rust archive: 2 crates (billiards + fluids)
- ▸SHA-256 content hashes for all archives
Resources
MENTAT Contribution Certificates
MENTAT Contribution Record
IDEA
Conceptual Contribution
CONTRIBUTION LEVEL: IDEA
Ontological EngineerTKFT: Dynamical Systems as Computation via Reaching Relations
Contributor
Eva Miranda
Universitat Politecnica de Catalunya
Core conceptual insight: dynamical systems — specifically billiard systems on polygonal tables — can simulate Turing machines. Reaching relations between states form a category under composition. The TKFT (Topological-Kinematic Formulation of Turing) framework bridges continuous dynamics to discrete computation via Cantor encoding of tape states into billiard configurations.
MENTAT Contribution Record
THEORY
Mathematical Foundation
CONTRIBUTION LEVEL: THEORY
Ontological EngineerFour-Layer TKFT: Geometry, Dynamics, Encoding, Validation
Contributor
Eva Miranda
Universitat Politecnica de Catalunya
Full mathematical framework: (1) Billiard geometry — polygonal tables, elastic reflections, energy conservation, (2) Dynamics — continuous-time evolution with discrete collision events, (3) Cantor encoding — injective map from Turing machine tape states to billiard position/velocity pairs, (4) Seismic validation — TKFT predictions tested against IRIS/USGS earthquake data using ak135 travel-time model.
Builds Upon
MENTAT Contribution Record
PROOF
Formally Verified
CONTRIBUTION LEVEL: PROOF
Lean 4 Formalization — 158 Modules, 200+ Theorems, 0 Sorry
Contributor
Apoth3osis Labs
R&D Division
Machine-checked Lean 4 formalization of the complete TKFT framework. 158 modules across 4 layers: billiard geometry, dynamics/evolution, reaching relations (categorical composition, associativity, observable reaching), Cantor encoding (injectivity), and seismic validation bridge. All theorems proved without sorry/admit.
Builds Upon
MENTAT Contribution Record
KERNEL
Computationally Verified
CONTRIBUTION LEVEL: KERNEL
Miranda Dynamics Verified Kernel — C & Rust Transpilation
Contributor
Apoth3osis Labs
R&D Division
Verified C and safe Rust transpilations of the core Miranda Dynamics modules. C: gcc -std=c11 -Wall -Wextra -Werror, 0 warnings. Rust: cargo build 0 warnings, cargo test 4/4 pass. BilliardState, evolve, reaches, observable_reaches, and reaching_compose faithfully translated.
Builds Upon
MENTAT Contribution Record
THEORY
Mathematical Foundation
CONTRIBUTION LEVEL: THEORY
Ontological EngineerFluids Lane: NS Turing Completeness via Cosymplectic Geometry
Contributor
Eva Miranda
Universitat Politecnica de Catalunya
Second pillar of Miranda's computational dynamics program: Navier-Stokes equations are Turing complete. The chain: cosymplectic structure (closed α, closed ω, volume form) → harmonic Reeb field → Etnyre-Ghrist correspondence (Nonlinearity 2000) → rotational Beltrami field → viscosity-invariant stationary NS solutions → undecidable trajectory prediction and periodicity detection via halting reduction.
Builds Upon
MENTAT Contribution Record
PROOF
Formally Verified
CONTRIBUTION LEVEL: PROOF
Fluids Lane Lean 4 Formalization — 5 Modules, 4 Theorems, 0 Sorry
Contributor
Apoth3osis Labs
R&D Division
Machine-checked Lean 4 formalization of the full fluids-lane chain. 5 modules (ContactGeometry, CosymplecticGeometry, EtnyreGhrist, HarmonicNS, TuringComplete), 12 structures, 4 proved theorems including fluid_trajectory_undecidable and fluid_periodicity_undecidable. Zero sorry, zero axiom. Hostile audit: CLEAN, 0 findings.
Builds Upon
MENTAT Contribution Record
KERNEL
Computationally Verified
CONTRIBUTION LEVEL: KERNEL
Fluids Lane Verified Kernel — C & Rust Transpilation
Contributor
Apoth3osis Labs
R&D Division
Verified C and safe Rust transpilations of the fluids lane modules. C: gcc -std=c11 -Wall -Wextra -Werror, 0 warnings. Rust: cargo build 0 warnings, cargo test 4/4 pass. Contact, Cosymplectic, EtnyreGhrist, HarmonicNS, and FluidTuringConstruction faithfully translated.
Builds Upon
Governed by MENTAT-CA-001 v1.0 · March 2026