Papers and technical documents

For a rational map σ of a finite-dimensional space over a field K and two states s, t, we determine the set Id(s, t) = {n ∈ ℤ : σⁿ s = t} of step counts—the hom-set from s to t in the action groupoid of the dynamics—without iterating the map. For the Lyness map, the Kahan–Hirota–Kimura discretisation of the Euler top, area-preserving linear maps and a Kahan discretisation of hyperbolic geodesics, we prove, in Lean 4 with Mathlib and for every field (characteristic ≠ 2 where needed), that on every level set of the conserved quantities the map is a translation by a fixed element P of an abelian group A attached to the level, along an injective coordinate ψ. Hence σⁿ s = t if and only if ψ(t) − ψ(s) = nP: step counts are discrete logarithms, Id(s, t) is empty or a residue class modulo the order of P, and the class of ψ(s) modulo ⟨P⟩ is a complete invariant of the orbits. The theorems also cover the degenerate levels (nodal and reducible curves, and the levels of the Euler top with vanishing coordinates). Two further results make the theory usable as a decision procedure. First, the states at which the map is undefined are finitely many explicit states of each level, so whether an orbit ever meets a division by zero (that is, whether the state is regular) is decided by a few more discrete logarithms, in both time directions, and a non-regular state’s finite chain is read off the same logarithms. Second, a reduction theorem for partial rational maps lifts regularity and the absence of paths from the reductions modulo primes to ℚ and reduces step counts from ℚ modulo primes, so that, given a bound on |n|, questions over ℚ, including the negative answer “never”, are settled by finitely many primes and one exact iteration. The dynamics is also axiomatised as a small Martin-Löf theory with a path constant path : Πx. Id(x, step x) and interpreted in the groupoid model of HoTTLean, where the identity type between s and t is exactly the set Id(s, t). The development comprises 1,146 theorems with no sorry and only the standard axioms, and includes an executable certificate checker whose soundness is itself proved in Lean. It is the mathematical foundation of Structure Computer, which answers these questions with independently checkable certificates: on a 2-core machine, a state 7.9 × 10¹⁵ steps away over 𝔽_{2⁶¹−1} is located in 0.4 s, where iteration would take about a century.

Structure Computer answers structural questions about discrete dynamical systems given by rational maps—first among them “after how many steps, if ever, does state s reach state t?”—exactly, over finite fields and over the rationals, and attaches to every answer a certificate that an independent checker verifies without trusting the program that computed it. For the Lyness map, the Kahan–Hirota–Kimura discretisation of the Euler top, area-preserving linear maps and a Kahan discretisation of hyperbolic geodesics, the answer is computed from theorems proved in Lean, as a discrete logarithm on a group attached to the level set of the conserved quantities: orbits of 10¹⁷ states are settled in a fraction of a second, including the answer “never”, which over ℚ no iteration can give. The same procedure (compute, certify, check independently, and label each result with the kind of guarantee it carries) applies to eleven further questions: invertibility, period structure, integrability, discovery and verification of conserved quantities, holonomy, reconstruction of integer invariants, equivalence of paths and of systems, transport of checked results along conjugacies, and the evaluation of closed terms of a type theory in the dynamics. Systems are given by name or as short text files, and a system written in unfamiliar coordinates is recognised as a known family up to affine changes of coordinates, with the change recorded in the certificate and re-verified by the checker. For the Lyness map over 𝔽_q the checker exists in a second form, written in Lean and proved sound. Long walks can optionally be certified by STARK proofs that are verified in milliseconds. In a brute-force comparison over small fields, 12,156 state pairs agreed with the truth read off the orbits and 5,950 certificates passed the checker; in a tamper test the checker rejected all 1,363 altered certificates; the Lean checker and the independent checker did not disagree on any of 2,004 certificates and 14,025 alterations that both could read. On a 2-core machine, a Lyness state 7.9 × 10¹⁵ steps away over 𝔽_{2⁶¹−1} is located, certified and checked in 0.4 s.