Miranda Dynamics
Machine-checked formalization of computational universality in dynamical systems. Billiard trajectories encode Turing computation via a 4-layer TKFT categorical architecture with ReachingRel. Based on Professor Eva Miranda's research on billiards, Euler flows, and Navier-Stokes.
Billiard Trajectories
Interactive
Proof Architecture
Lean 4 Verified
A 2D rectangular billiard table with orange-glowing borders. Balls bounce deterministically, encoding computation through their trajectories.
Color-coded trails follow each ball. Orange, cyan, and magenta paths show the history of bounces and reflections across the table.
Semi-transparent orange bands highlight periodic regions where Cantor set encoding emerges from the billiard dynamics.
Green curved arcs connect trajectory revisit points, visualizing the ReachingRel categorical structure from the TKFT layer.
The schematic shows HeytingTuring (magenta), TKFT (orange), three domain columns, and the validation bar with pulsing data flow connections.
Zero sorry statements in the entire codebase. All theorems are machine-checked with complete proof chains.
Computational Universality in Dynamical Systems
The key result: billiard trajectories encode Turing computation. Eva Miranda's work shows that certain smooth dynamical systems -- billiards with specific boundary geometries, Euler flows on Riemannian manifolds, and solutions to the Navier-Stokes equations -- are computationally universal.
This is a machine-checked proof in Lean 4 using a 4-layer architecture: the TKFT categorical framework provides ReachingRel as a functor between dynamical system categories, HeytingTuring bridges Heyting algebras with Turing machines, and the Seismic layer validates predictions against real earthquake data.
The categorical framework for reaching relations in dynamical systems. Defines ReachingRel as a functor capturing how trajectories revisit regions of phase space.
TKFT.Reaching.reachingRel_categorySTA/LTA seismic event detection validated on real IRIS/USGS data. Proves correctness of the short-term/long-term average ratio algorithm for P-wave arrival picking.
Seismic.Validation.sta_lta_correctCausal invariance in discrete rewriting systems, connecting Wolfram Physics to the dynamical systems framework through abstract rewriting confluence.
Wolfram.CausalInvariance.causal_invarianceThe unifying correspondence between Heyting algebras and Turing machines. Bridges intuitionistic logic with computational universality at the top of the architecture.
HeytingTuring.CorrespondenceSeismic STA/LTA detection validated against real earthquake data from the IRIS/USGS global seismographic network.