Structure Computer
Checking the compute server…

Structure Computer

For discrete dynamical systems written with rational maps, it answers how many steps state t is from state s — or that it is never reached — with a certificate that an independent checker verifies.

The answer is one of “t = σⁿ s ⇔ n ≡ r (mod M)”, “no path” or “s is not regular”, over a finite field 𝔽_q or the rationals ℚ. For the known families it answers from theorems proved in Lean, even for q so large that following the orbit would take years.

Try itSee examplesRead the docs

Families it answers

Kind of systemHow it is answered
Lyness mapfrom theorems (no orbit is followed, even for large q)
Euler top discretised by Kahan's methodfrom theorems (no orbit is followed, even for large q)
Linear maps with determinant 1 (such as a discretised oscillator)from theorems (no orbit is followed, even for large q)
One discretisation of geodesics on a hyperboloidfrom theorems (no orbit is followed, even for large q)
A family above, written in other coordinatesrecognised, and answered from theorems in the same way
Any other systemby following the orbit (“no result” beyond the limit)

How the answers are guaranteed

The part that computes the answers is built so that it does not have to be trusted. What makes an answer correct is the independent checker and theorems proved in Lean beforehand.

  1. 1
    Compute

    The computing part produces the answer and cheap hints to confirm it.

  2. 2
    Certificate

    The question, the answer, its kind, the hints, the presuppositions and the names of the theorems relied on go into a certificate.

  3. 3
    Independent check

    A separate program, the checker, re-checks the answer from the definitions, using only the certificate.

  4. 4
    An answer with its certainty

    Certain, probably certain, reconstructed, statistical, or no result. A failed check is recomputed; if it fails again, the answer is “no result” with the reason.

This site