Let R be a commutative ring with a distinguished element ε satisfying ε ≠ 0 and ε² = 0. This is the algebra of dual numbers k[ε]/(ε²) — the simplest non-trivial quotient of a polynomial ring. It is the algebraic incarnation of first-order perturbation theory, automatic differentiation, and the tangent bundle of a point.
The claim of this paper is that this single axiom — encoded in Lean 4 as the typeclass NilSquare — forces a seventeen-layer tower of algebraic structure, from elementary ring theory through representation theory, homological algebra, deformation theory, A-infinity structures, and operadic Koszul duality, all the way to a concrete bridge connecting abstract algebra to lambda-calculus reduction. Every theorem in the tower is machine-checked. The sorry count in the core tower files is zero.
The entire tower grows from one Lean 4 typeclass:
Three fields. A commutative ring R, a distinguished element ε that is not zero, and the axiom ε * ε = 0. From eps_sq alone, layer by layer, the entire tower is forced. No design choices — each layer is a consequence of the previous.
Immediate consequences (all in Epsilon.lean): ε is nilpotent (witness: exponent 2). ε is a zero divisor (witness: itself). And the automatic differentiation property: (a + bε)(c + dε) = ac + (ad + bc)ε. The cross-term bdε² vanishes, leaving only the first-order perturbation. This is not a feature — it is forced by the axiom.
| Layer | File | What it proves |
|---|---|---|
| 1 | Epsilon.lean | The axiom. Nilpotency, zero-divisor property, automatic differentiation: (a + bε)(c + dε) = ac + (ad + bc)ε |
| 2 | EpsilonModule.lean | Exactness. The map r ↦ εr is a chain complex (ε² = 0 ⟹ d² = 0). Under NilSquareLocal: ker(·ε) = im(·ε), giving the 1-periodic resolution ⋯ → R →·ε R →·ε R → k → 0 |
| 3 | EpsilonDeriv.lean | Entanglement. For any derivation D, the Leibniz rule on ε² = 0 forces ε · D(ε) = 0 (in char ≠ 2). Position and velocity cannot simultaneously be nonzero. Ω¹(R/k) ≅ k |
| 4 | EpsilonDeform.lean | Universal deformation. The family η² = tη has singular fiber (t = 0) recovering ε² = 0. At t invertible, η/t is idempotent and the algebra splits as k × k. The singularity resolves |
| 5 | EpsilonVariations.lean | Uniqueness. ε³ = 0 sees second derivatives (AD fails). Two nilpotents generate dimension 4. Only one nilpotent of order exactly 2 gives: minimal dimension, exact first derivative, 1-dimensional deformation space |
| 6 | EpsilonHamming.lean | Error detection. The ideal (ε) is a square-zero code: every codeword squares to zero, the product of any two codewords is zero. Nilpotency = single-error detection |
| 7 | EpsilonTernary.lean | Kraft saturation. Seven TLC constructors with lengths [1,2,2,2,2,2,2] have Kraft sum 1/3 + 6/9 = 1. Prefix-free and saturating over the ternary alphabet. The dual numbers over F₃ have unit group Z/6Z |
| 8 | ThreeIndecomposables.lean | Representation theory. Exactly three indecomposable modules: M₁ = R/(ε), M₂ = (ε), M₃ = R. Every idempotent is 0 or 1. The short exact sequence 0 → (ε) → R → R/(ε) → 0 does not split |
| 9 | ARQuiver.lean | Singularity category. The AR-quiver is the A₂ Dynkin diagram: 2 vertices, 1 arrow, no loops. Ext¹ is generated by ε. The second syzygy Ω²(k) ≅ k — the resolution is periodic |
| 10 | Cotangent.lean | Cotangent cohomology. T¹(R/k, k) ≅ k. The chain: T¹ = Ext¹(Ω¹, k) = Ext¹(k, k) = ker(ε·)/im(ε·) = k. One-dimensional — one deformation direction |
| 11 | Knorrer.lean | Knoerrer periodicity. The stabilization e ↦ e·d in k[e,d]/(e², d²) preserves dual-number arithmetic. The periodic resolutions over R₁ and R₂ have identical algebraic structure |
| 12 | MatrixFactorization.lean | K-theory. Matrix factorizations of ε² = 0 collapse to 2-periodic complexes. The flip (φ,ψ) ↦ (ψ,φ) has order 2. Two classes (even/odd) give K₀ ≅ Z/2Z |
| 13 | Hochschild.lean | Hochschild cohomology. Every differential is zero (by the cocycle condition). HHⁿ ≅ k for all n, period 1. HH² ≅ k means the deformation η² = tη from Layer 4 is universal |
| 14 | KoszulDual.lean | Koszul duality. Ext*(k, k) ≅ k[x] — the polynomial ring. The simplest singularity (ε² = 0) is Koszul-dual to the simplest smooth algebra (no relations). Five characterizing properties proved |
| 15 | AInfinity.lean | A∞ minimality. m₂ ≠ 0 (multiplication exists), m₃ ≠ 0 (the triple Massey product ⟨ε,ε,ε⟩ = 2ε detects the singularity), m₄ = 0 (higher obstructions vanish by periodicity). Exactly one nonzero higher operation |
| 16 | ChurchRosser.lean | Confluence. NilSquare residuals anti-commute; in a commutative ring, they annihilate. Diverging reduction paths cannot interact. Church-Rosser for TLC beta-reduction follows |
| 17 | CompositionOperad.lean | Koszul composition operad. The operadic structure completing the tower |
The formalization extends beyond the core tower with several additional modules:
| File | What it adds |
|---|---|
| HeckeHodgeFunctor.lean | Filtered triples. Three endomorphisms (p, n, m) with p idempotent, n nilpotent of order 2, p and n orthogonal. The NilSquare ring yields the Hodge triple (0, ·ε, id). Includes concrete Hecke eigenvalue verification for X₀(11) with Ramanujan bound checks |
| SpectralDegeneration.lean | Depth filtrations. Every depth filtration on an Artinian module stabilizes (by the descending chain condition). Graded pieces past stabilization are trivial |
| ComplexityNilSquare.lean | Determinism as NilSquare. Deterministic step functions yield NilSquare residuals in TrivSqZeroExt; nondeterministic step relations may not. An algebraic signature, not a complexity-theoretic result |
| NilSquareTruncation.lean | 1-truncation. ε² = 0 means the residual-of-a-residual is zero — 2-cells carry no information. The evaluation path space is a 1-type. UIP for residual equality |
| MotivicGalois.lean | Motivic Galois group. Z/2Z as the motivic Galois group of the tower |
| CompositionOperad.lean | Koszul composition. The operadic structure on the tower's algebraic data |
The bridge connects abstract algebra to concrete computation — instantiating the entire NilSquare tower for TLC lambda-calculus reduction. The construction has three parts: a falsification, a correct bridge, and a universal realization.
The natural idea is to define the reduction residual as (id − nf₁) and hope that (id − nf₁)² = 0. This is false, and the falsification is proved in Lean (KrivineNilSquareFalsification.lean).
The obstruction is concrete: the term app(id, app(app(id, id), id)) takes three beta-steps to normalize. The totalized weak-head step does not stabilize after two iterations. The linearized residual on the free abelian group of terms is not square-zero. Four separate witnesses are constructed and packaged as raw_reduction_not_nilSquare_bridge_ready.
The fix is to lift from terms to the trivial square-zero extension (KrivineNilSquare.lean):
where TermVector = TLC →₀ Z is the free abelian group on TLC terms. The key steps:
1. Define nf1 as a bounded normal-form projector (not the raw one-step operator). Prove nf1_idem: the projector is idempotent.
2. The residual of a term t is [t] − [nf₁(t)] in TermVector, lifted into the nilpotent ideal of TrivSqZeroExt via inr.
3. The square of any lifted residual is zero — by TrivSqZeroExt.inr_mul_inr, elements in the nilpotent ideal always multiply to zero.
4. The distinguished nilpotent krivineEpsilon is the residual of app(id, id). It is proved nonzero (the witness genuinely reduces) and square-zero. This gives the NilSquare instance on ReductionDual.
The entire 17-layer tower now applies to ReductionDual. The Hodge triple, the periodic resolution, the Ext algebra, the A-infinity structure — all instantiate automatically.
KrivineNilSquareUniversal.lean constructs a generic algebra homomorphism from ReductionDual into any NilSquare ring R, sending krivineEpsilon to ε. Key results:
realizeIn: the algebra homomorphism from ReductionDual to R.
realizeHodgeMorphism: a filtered-triple morphism from the concrete TLC Hodge triple to the abstract Hodge triple of any NilSquare ring.
bridgeEquiv: the strong (nf₁-based) and machine (Krivine-projector-based) bridges present the same TrivSqZeroExt, proved via mutual inverse algebra homomorphisms.
reductionSingularFiber: the singular fiber of the abstract deformation tower, specialized to the TLC residual ring.
The tower terminates in self-measurement. The proof term witnessing ε² = 0 is:
"Lambda epsilon, mul(epsilon, epsilon)." After hash-consing into a DAG, the five nodes are: const 22 (multiplication), var 0 (epsilon — shared, referenced twice), app(0,1), app(2,1) (reuses Node 1), lam(3). Upper bound: 5 nodes. Lower bound: all five are structurally distinct — no further sharing is possible. Both bounds are proved in Lean.
K_epsSq_tight). Upper = lower bound, proved in Lean.
This value is universal across all axiom systems of the form x² = c. All three order-2 algebras — nilpotent (ε² = 0), involution (j² = 1), idempotent (e² = e) — share K = 5. A strict gap of 2 separates them from K ≥ 7 for anything more complex. No equation has K = 6. Order 2 is the K-optimal algebraic structure.
| Equation | Tree nodes | DAG nodes |
|---|---|---|
| x² = c | 6 | 5 |
| x³ = c | 8 | 7 |
| (x²)² = c | 10 | 7 |
| x² + x = c | 8 | 8 |