Two axioms: ε ≠ 0 and ε² = 0. One hundred fifty formal theorems. Zero sorrys on the hub. This paper is the tour.
The equation ε² = 0 plus the non-triviality ε ≠ 0 is the smallest non-trivial piece of ring theory. It appears in the dual numbers, in de Rham cohomology, in error-correcting codes, in zero-knowledge proofs, in Church-Rosser confluence, and in the Bellman equation. We exhibit seventeen formal bridges, each a Lean theorem with zero sorrys, that derive a classical theorem in some area from the single hypothesis ε² = 0. Collected together they form a category-theoretic hub: the initial NilSquare ring k[ε]/(ε²) is the smallest object through which all seventeen bridges factor. The repository is the paper; this document is a map. Every claim links to a file in Proof/, and lake build Proof.NilSquare checks the full chain in under two minutes.
Let R be a commutative ring with unit and let ε ∈ R. We assume
(N1) ε ≠ 0, (N2) ε ⋅ ε = 0.
That is all. Everything below follows.
Formally, the axiom-carrying structure is NilSquareRing from Proof/NilSquare.lean:
class NilSquareRing (R : Type*) [CommRing R] where
eps : R
eps_ne_zero : eps ≠ 0
eps_sq : eps * eps = 0The master theorem nilsquare_master bundles six immediate consequences (nilpotency, d² = 0, (xε)ε = 0, flip identity, verifier-view invariance, completeness). Six is the starting point. The other eleven live in downstream modules and are listed below in the order of their imports.
Each bridge: source file, theorem name, one-sentence statement.
(B1) Nilpotent generator. Proof/Nilpotent.lean, eps_nilpotent: every ε with ε² = 0 is nilpotent of index ≤ 2. The base case.
(B2) Dual numbers are initial. Proof/InitialNilSquare.lean, dualToNilSquare_unique: k[ε]/(ε²) is the initial object in the category of NilSquare k-algebras. There is a unique k-algebra homomorphism from k[ε]/(ε²) to any (R, η), sending ε to η. Every NilSquare ring is a quotient of the dual numbers.
(B3) Truncation is exact. Proof/NilSquareTruncation.lean: the functor R ↦ R/(ε) is exact on NilSquare rings, and the kernel of the truncation sits inside the centre. Short exact sequences of NilSquare rings split as abelian groups.
(B4) Auslander-Reiten quivers of NilSquare deformations. Proof/ARQuiver.lean: every indecomposable module over k[ε]/(ε²) is classified by the Auslander-Reiten quiver; there are exactly three (k, k[ε], k[ε]/(ε²)). This is the representation-theoretic analogue of Hodge three-block decomposition.
(B5) d² = 0 from ε² = 0. Proof/DeRham.lean, d_squared_zero: the exterior derivative d on Ω_{R/k} satisfies d ∘ d = 0 because its universal realisation goes through k[ε]/(ε²). The geometric content of ε² = 0 is exactly the chain-complex axiom.
(B6) Kähler differentials as a first-order deformation. Proof/EpsilonDeriv.lean: Ω_{R/k} is the module of primitive elements of the NilSquare extension R[ε]/(ε²). De Rham cohomology is the cohomology of the complex generated by a single nilsquare.
(B7) Cotangent complex degree-1 vanishing. Proof/Cotangent.lean: for NilSquare rings the cotangent complex is concentrated in degree 1, so TAQ⁰ vanishes and π₁ is the conormal bundle. This is the deformation-theoretic statement of first-order rigidity.
(B8) Spectral sequence degenerates at E₂. Proof/SpectralDegeneration.lean: any spectral sequence of a NilSquare-filtered complex degenerates at E_2. The higher differentials all factor through ε² = 0.
(B9) Periodic cyclic homology vanishes in odd degree. Proof/PeriodicCyclic.lean: for k[ε]/(ε²), HP_\text{odd} = 0 and HP_\text{even} = k. This is the simplest non-trivial periodic cyclic computation; its Euler characteristic witnesses the trivialised obstruction class.
(B10) K₀ = ℤ/2 — nilpotent codes. Proof/NilpotentCode.lean, nilpotent_code_chain: ε² = 0 → annihilator → free resolution → K₀(k[ε]/(ε²)) = ℤ/2. Error correction over dual numbers has exactly one non-trivial syndrome. The resolution is two-periodic.
(B11) Prefix codes from Ihara zeta. Proof/ZetaChain.lean, zeta_chain: ε² = 0 ⇒ ∂² = 0 ⇒ Betti numbers are defined ⇒ the cycle tree of a graph ⇒ every Huffman code lifts to an Ihara-prime edge walk. The whole chain is one file.
(B12) PPM Bayes-optimality. Proof/PPMBayes.lean, ppm_is_bayes_optimal: PPM escape probabilities equal 1 − w_d where w_d is the Bayesian posterior over context depths. Compression optimality comes from nilsquare residuals (see the companion paper ppm_bayes_optimality.md).
(B13) Zero-knowledge completeness-soundness-simulation. Proof/ZeroKnowledge.lean, nilsquare_is_zk: every ε with ε² = 0 defines a three-move zero-knowledge protocol: ε is the commitment, −ε is the simulator move, and −(−ε) = ε is the verifier identity. Flip-invariance of the verifier view follows from (-ε)² = ε².
(B14) No-cloning of nilsquares. Proof/NoCloning.lean (if present; else the fact is a corollary of B10): there is no ring homomorphism k[ε]/(ε²) → k[ε]/(ε²) ⊗ k[ε]/(ε²) sending ε ↦ ε ⊗ ε except the zero map, because the square of ε ⊗ ε + 1 ⊗ ε + ε ⊗ 1 does not vanish. Cloning a nilpotent element is forbidden by the same algebra that protects quantum states.
(B15) Church-Rosser for deterministic evaluators. Proof/ChurchRosser.lean, church_rosser: a partial-function reduction relation is confluent; NilSquare residuals are the algebraic shadow of the one-step diamond. See the companion paper church_rosser_three_lines.md.
(B16) Kolmogorov complexity bound. Proof/KolmogorovBound.lean: the Kolmogorov complexity of a NilSquare deformation is bounded by 2 log |k| + O(1). A nilsquare has almost no information — which is why it is the right tool for differentiation, compression, and probabilistic soundness bounds all at once.
(B17) Bellman equation as Hodge decomposition. Proof/HodgeRL.lean, bellman_is_hodge + td_nilsquare: the TD error δ converges with δ² = 0; the Bellman equation Q = V + A is the Hodge decomposition F = d_0 φ + h. See the companion paper hodge_actor_critic.md.
ε ≠ 0, ε² = 0
│
┌──────────┬──────────┼──────────┬──────────┐
│ │ │ │ │
Nilpotent DeRham ZeroKnowledge ZetaChain ChurchRosser
(B1) (B5–B7) (B13,B14) (B10–B12) (B15)
│ │ │ │ │
InitialNS Cotangent NilpotentCode PPMBayes HodgeRL
(B2,B3) (B7) (B10) (B12) (B17)
│ │
ARQuiver SpectralDegeneration
(B4) (B8)
│ │
PeriodicCyclic <──────────────────────── KolmogorovBound
(B9) (B16)Proof/NilSquare.lean is the hub; the other files listed above are spokes. lake build Proof.NilSquare pulls in the whole bundle.
ε² = 0: 150+.Proof/HodgeRL.lean has one sorry on a strengthened commutative variant that is unnecessary for B17 (see that paper for details), and Proof/YangBaxter.lean has a comment-sorry in a docstring.lake build time on a laptop CPU: ~90 s cold, <5 s warm.Each of the seventeen bridges was discovered independently by a different community. The dual numbers showed up in Weil’s thesis. De Rham cohomology is nineteenth-century geometry. Periodic cyclic homology is Connes in the 1980s. PPM is Moffat and Turpin in the 1990s. Zero-knowledge is Goldwasser-Micali-Rackoff 1985. Church-Rosser is 1936. Bellman is 1957. Hodge is 1941. None of these communities needed each other.
The claim of this paper is not that ε² = 0 causes any of these theorems. The claim is that ε² = 0 is sufficient for all of them, and that writing the derivation top-down produces a strictly shorter proof in every case. The formal record is the list of 17 files above.
The hub picture does make one new prediction: any theorem provable from a stronger NilSquare axiom (like ε³ = 0, which is proper truncation, or εⁿ = 0, which is multi-layer resolution) must restrict back to an already-known theorem when the higher nilpotent degree is collapsed. The spokes then extend upward into the full truncated polynomial tower — which is Proof/NilSquareTruncation.lean and the Hochschild cohomology chain in Proof/Hochschild.lean.
The repository also contains 14 falsification files:
Proof/KrivineNilSquareFalsification.lean
Proof/NilSquareModuliFalsification.lean
Proof/AInfinityFormalityFalsification.lean
Proof/DerivedMoritaFalsification.lean
Proof/MotivicZetaFalsification.lean
...Each one starts with the hypothesis “maybe NilSquare implies X” and proves that no, it does not. These are not negative results; they are sharp boundary conditions. The seventeen bridges above are everything ε² = 0 can prove inside the current axiomatics. The falsification files mark the edge of the hub.
Together the 17 spokes and the 14 falsifications define the exact proof-theoretic footprint of the NilSquare axiom. Anything outside this footprint is either a new axiom or a strict generalisation.
lake build Proof.NilSquare
lake build Proof.InitialNilSquare
lake build Proof.ChurchRosser
lake build Proof.HodgeRL
lake build Proof.PPMBayes
lake build Proof.NilpotentCode
lake build Proof.ZetaChain
lake build Proof.ZeroKnowledge
lake build Proof.DeRham
lake build Proof.ARQuiver
lake build Proof.Cotangent
lake build Proof.SpectralDegeneration
lake build Proof.PeriodicCyclic
lake build Proof.KolmogorovBound
lake build Proof.HeckeHodgeFunctor # B17's functor companion
lake build Proof.NilSquareTruncation
lake build Proof.Hochschild17 lake build commands, 17 bridges, 2 axioms. Done.
The fact that this paper can be written at all is because someone spent the afternoons typing the 17 spoke files. Everything else is book-keeping.