Lean 4 · mathlib · standard axioms only

What is proved

The proof library turns the atlas's patterns into theorems. It is about 4,900 lines of Lean, built against mathlib. Every result rests on Lean's standard axioms alone, and none uses sorry. Six of its files were written by AI agents, and are in the library as they wrote them, because Lean accepted them.

The library

select a file

written by the orchestrator written by a pilot's agent generated from the atlas code

The main results

Result	Statement	Theorem	Proved by
The bridge	On an odd torus, the period is the lcm of the orders of the nonzero eigenvalues	`period_eq_eigenLcm`	orchestrator
The bound	The period divides 2^ord(m) − 1, and 2^sord(m) − 1 for a symmetric rule, so it is odd	`period_dvd_two_pow_sub_one_of_symm`	orchestrator
The group ring	Every rule acts on every finite torus through F₂[Z²], so each identity is an identity of rules at every size	`gstep_eq_iterate`, `isEventualPeriod_restrict_iff`	orchestrator
Even sizes	The odd part of the period is the odd torus's period, and the 2-part is bounded, on the square and the atlas's triangular and hexagonal tori	`period_eq_two_pow_mul`	orchestrator
Powers and dilations	Round 2's mechanisms as theorems about periods, at every size	`period_sqN4K8C4`, `period_sqC4self`	orchestrator
The twisted power	If 3 ≡ ±2^k (mod m), VO + T13's odd part is the edge rule's divided by gcd(P, 1 + 2^k)	`atlasTriPeriod_twisted`	orchestrator
The square law's 2-part	P(2^vm) = 2^vP(m) for B1357/S1357, odd m > 1	`period_sqN4D4`	orchestrator
The hexagon law's 2-part	Exactly 2^v+1P(m) on the atlas's hexagonal torus, for m ≥ 5	`hexPeriod_hexH1_exact`	pilot 1's agent
The triangle laws' 2-part	Exactly 2^v+1P(m) for m ≥ 3, for the edge and edge+vertex rules	`atlasTriPeriod_triE_exact`, `atlasTriPeriod_triEVOVS_exact`	pilot 2's agent
The cubes at m = 37	Each of the six rules that puzzled the atlas has period dividing 87,381 = (2¹⁸ − 1)/3 at m = 37, and so does rule 90	`period_w_dvd_87381`, …, `period_r90_dvd`	pilot 4's agent
The cubes at m = 25	Five of the seventeen rules a census left unexplained have period dividing 341 = (2¹⁰ − 1)/3 at m = 25: two by cube certificates, three as twisted pairs	`period_r3096_dvd`, …, `period_r32184_dvd`	pilot 5's agent
Unit times cube	Nine rules that are a unit times a cube have period dividing 87,381 at m = 37, and three of them dividing (2³⁰ − 1)/3 at m = 61	`period_r1112_dvd_37`, …, `period_r18246_dvd_61`	pilot 6's agent
VO + T13's law	2^v+1P(m) for m ≥ 3, and n/2 at n = 2^v; the agent found the law from data first	`atlasTriPeriod_triVOT13_law`	pilot 3's agent

What is not proved

The odd parts. That the square and triangle rules reach the full bound, P(m) = 2^sord(m) − 1, is checked by machine for every odd m up to 999 except ten, and proved for none in general. The hexagon's odd part, rule 90's period, is proved by hand, but not yet in Lean.
Why a rule with no confinement reaches the full bound. At present it is a heuristic: generic elements generate.
The rule-150 analogues. Square D4 + A4 + self has rule 150's period and hexagon H2 + H3 + self twice it. Both are confirmed by registered tests, and unproved.

How a proof is accepted

For the library's own files, lake build must succeed and #print axioms on each main result must list nothing beyond propext, Classical.choice and Quot.sound. An agent's proof faces more: its file is rebuilt against a fresh copy of the real library, the target statement is checked again from a pinned copy, and every library file must match a SHA-256 manifest. The model describes the rest.