Reading the results, and a glossary
How to read the results shown on the Try page, and what the terms used on this site mean.
Reading a result card
“Compute everything” lays out one card per question.
- Top row: the question's tag (Id, Q1–Q11) and name, a label with the kind of result, and the time taken.
- Summary: the answer in one line.
- Details: opens the answer's explanation, the checker's notes, the Lean theorems it rests on, whichever of value, presupposition, assumption, error bound, statistic and reason it has, and the whole certificate. The certificate can be downloaded and checked again from here (“Certificates and checking”).
- Above the list: “Certain n/total” shows how many answers are certain.
Besides answers, a card can show these states:
| Shown | Meaning |
|---|---|
| Computing, Waiting, Queued | being computed, waiting for another answer, or waiting for its turn on the compute server; “Cancel” stops it |
| Skipped | not computed, e.g. Q5 when Q4 found no conserved quantity |
| Not applicable | the question does not apply to this system, e.g. Q6 for a system that declares no symmetry |
| Error | the input could not be read, for example; the reason is shown |
Computed results are kept as a history in this browser (“Clear” removes them).
The kinds of result
| Kind | Meaning | Comes with |
|---|---|---|
| Certain | a mathematical statement that passed the check and follows from theorems proved in Lean | a presupposition (if any) |
| Probably certain | guaranteed correct up to a bound on the chance of error | the error bound |
| Reconstructed | a value that is unique under the stated assumption | the assumption (e.g. the step count is at most B in size) |
| Statistical | an estimate from samples; not a theorem | the statistic |
| No result | no claim | the reason (e.g. the orbit is longer than the walk limit, or the check failed) |
Presupposition: even a certain answer can carry a presupposition. For example, when it cannot be decided for a large q whether s or t is regular, the answer presupposes that they are. The presupposition is stated with the answer.
The forms of the answer to Id(s, t)
| Answer | How to read it |
|---|---|
| t = σⁿ s ⇔ n ≡ r (mod M) | n steps reach t exactly when n leaves remainder r on division by M; M is usually the period of the orbit |
| No path | no number of steps, forwards or backwards, reaches t |
| s is not regular (t is reached in n steps) | the orbit of s breaks off where the formulas become undefined; t is reached before that in n steps (and in no other number) |
| s is not regular | as above, and t is not reached before the orbit breaks off |
| (over ℚ) t = σⁿ s, n = −3 (every solution: n ≡ r (mod M)) | t is reached in n steps over ℚ (here 3 steps back), confirmed by computing them exactly; any other solution would have the form n ≡ r (mod M) |
Glossary
| Term | Meaning |
|---|---|
| System | a set of states together with the rule that takes one step |
| State | a tuple of numbers, e.g. (2, 5); one entry per variable |
| Step (σ) | one use of the rule; σⁿ is n uses, running backwards when n is negative |
| Orbit | the states reached from a state by going forwards and backwards |
| Period | over a finite field, the number of steps until the orbit comes back |
| Cycles and chains | over a finite field, every state lies on a cycle with a period or on a finite chain that breaks off at both ends (except states where the rule is not defined at all) |
| Regular | a state where the formulas stay defined however far one goes, forwards or backwards; the Try page also calls it “a state of the groupoid”. Over a finite field, the same as lying on a cycle |
| No path | t appears at no step count |
| Id(s, t) | the set of paths (step counts) from s to t; the notation is borrowed from the symbol for the evidence of equality in type theory |
| Finite field 𝔽_q | arithmetic with the remainders on division by a prime q; every value is a whole number from 0 to q − 1, with no error |
| Rationals ℚ | arithmetic with fractions kept exactly as fractions |
| Step bound B | over ℚ, the range |n| ≤ B searched for the step count n |
| Conserved quantity | a formula whose value does not change along an orbit |
| Invertible (birational) | there are formulas that run a step backwards |
| Integrable | there are as many independent conserved quantities as the number of variables minus one, so every orbit lies on a curve |
| Symmetry | a set of transformations that turn the states without changing the system; declared in a system file by the quadratic expression it preserves (e.g. x^2 + y^2) |
| Identity | an equality of formulas that holds whatever values are put in; Structure Computer proves many of its claims in this form |
| Holonomy | how far the state has been turned when the orbit comes back up to the symmetry |
| Generators and words | in a system with several steps (generators), the paths made by stringing them together, e.g. r s^-1 r^2 |
| Affine change of coordinates | a change of coordinates of the form x ↦ Mx + c (M an invertible matrix) |
| Known family | a kind of system answered from theorems without following the orbit, even for large q: the Lyness map, a discretisation of the Euler top, linear maps with determinant 1, and one discretisation of geodesics on a hyperboloid; recognised even when written in other coordinates |
| System file | a short text giving the variables, the parameters, the step's formulas and so on (“Writing system files”) |
| Certificate | a JSON document with the answer and the hints to confirm it |
| Checker | a program, separate from the computing part, that confirms the answer again using only the certificate |
| Lean | a proof assistant in which a computer checks a mathematical proof line by line |
| Seed | the number the random choices of a computation are drawn from; the same seed gives the same certificate |
| Walk limit | for a system that is not a known family, the most steps the orbit is followed |