Papers · Atlas · Data

NilSquare: Seventeen consequences of ε² = 0

Research note

Richard Hoekstra · April 2026

The claim

Two axioms — ε ≠ 0 and ε² = 0 — suffice to derive seventeen classical theorems spanning algebra, differential geometry, coding theory, logic, and reinforcement learning. The dual-number ring k[ε]/(ε²) is the initial object in the category of NilSquare algebras: every NilSquare ring is a quotient, and every bridge factors through it. The repository contains 150+ formal Lean theorems with zero sorrys on the hub.

The two axioms

Let R be a commutative ring with unit and let ε ∈ R. Assume:

Axioms (N1) ε ≠ 0, (N2) ε · ε = 0.

In Lean, the axiom-carrying structure is:

class NilSquareRing (R : Type*) [CommRing R] where
  eps : R
  eps_ne_zero : eps ≠ 0
  eps_sq      : eps * eps = 0

The master theorem nilsquare_master bundles six immediate consequences: nilpotency, d² = 0, (xε)ε = 0, flip identity, verifier-view invariance, and completeness. The remaining eleven live in downstream modules.

The seventeen bridges

Algebra and representation theory (B1–B4)

Bridge	File	Statement
B1	Nilpotent.lean	Every ε with ε² = 0 is nilpotent of index ≤ 2
B2	InitialNilSquare.lean	k[ε]/(ε²) is initial: unique k-algebra homomorphism to any NilSquare ring
B3	NilSquareTruncation.lean	The functor R ↦ R/(ε) is exact; kernel sits inside the centre
B4	ARQuiver.lean	Exactly three indecomposable modules over k[ε]/(ε²): k, k[ε], k[ε]/(ε²)

Differential geometry (B5–B7)

Bridge	File	Statement
B5	DeRham.lean	d ˆ d = 0 because the universal realisation factors through k[ε]/(ε²)
B6	EpsilonDeriv.lean	Ω_R/k is the module of primitive elements of R[ε]/(ε²)
B7	Cotangent.lean	Cotangent complex concentrated in degree 1; TAQ&sup0; vanishes

Homological algebra (B8–B9)

Bridge	File	Statement
B8	SpectralDegeneration.lean	Any spectral sequence of a NilSquare-filtered complex degenerates at E₂
B9	PeriodicCyclic.lean	HP_odd = 0 and HP_even = k for k[ε]/(ε²)

Coding and information theory (B10–B12)

Bridge	File	Statement
B10	NilpotentCode.lean	K₀(k[ε]/(ε²)) = Z/2Z; error correction has exactly one non-trivial syndrome
B11	ZetaChain.lean	ε² = 0 ⇒ ∂² = 0 ⇒ Betti numbers defined ⇒ every Huffman code lifts to an Ihara-prime edge walk
B12	PPMBayes.lean	PPM escape probabilities equal 1 − w_d where w_d is the Bayesian posterior over context depths

Logic and computation (B13–B16)

Bridge	File	Statement
B13	ZeroKnowledge.lean	ε defines a three-move ZK protocol: commitment ε, simulator −ε, verifier identity −(−ε) = ε
B14	NoCloning.lean	No ring homomorphism sends ε ↦ ε ⊗ ε except the zero map
B15	ChurchRosser.lean	A partial-function reduction relation is confluent; NilSquare residuals are the algebraic diamond
B16	KolmogorovBound.lean	Kolmogorov complexity of a NilSquare deformation is bounded by 2 log \|k\| + O(1)

Analysis and RL (B17)

Bridge	File	Statement
B17	HodgeRL.lean	Bellman Q = V + A is the Hodge decomposition F = d₀φ + h; TD convergence gives δ² = 0

The hub diagram

                         ε ≠ 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)

Counts

Metric	Value
Proof files in the hub	23 (17 spokes + 6 internal)
Lean theorems from ε² = 0	150+
Sorrys in the hub	0
Total lines of Lean	~2,500
lake build time (cold)	~90 s
lake build time (warm)	<5 s

The boundary: 14 falsification files

The repository also contains 14 falsification files (e.g. KrivineNilSquareFalsification.lean, NilSquareModuliFalsification.lean) that prove certain consequences do not follow from ε² = 0. Together the 17 spokes and 14 falsifications define the exact proof-theoretic footprint of the NilSquare axiom. Anything outside this footprint requires a new axiom or a strict generalisation.

Why the hub picture matters

Each of the seventeen bridges was discovered independently by a different community: Weil (dual numbers), de Rham (cohomology), Connes (periodic cyclic homology), Moffat-Turpin (PPM), Goldwasser-Micali-Rackoff (zero-knowledge), Church (1936), Bellman (1957), Hodge (1941). None needed each other.

The claim 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 17 files, 17 lake build commands, 2 axioms.

Prediction Any theorem provable from a stronger NilSquare axiom (ε³ = 0 or εⁿ = 0) must restrict back to an already-known theorem when the higher nilpotent degree is collapsed. The spokes extend into the full truncated polynomial tower.

Reproducibility

lake build Proof.NilSquare           # the hub
lake build Proof.InitialNilSquare    # initiality
lake build Proof.ChurchRosser        # confluence
lake build Proof.HodgeRL             # Bellman = Hodge
lake build Proof.PPMBayes            # PPM optimality
lake build Proof.ZeroKnowledge       # ZK protocol
lake build Proof.KolmogorovBound     # complexity bound

Full paper (HTML) PDF