lean-workspaces

Lean 4 formalizations of original results in information geometry, algebraic stratification, and fractal dimension theory.

77 source files. ~960 machine-verified theorems. 3 intentional sorry.

All code compiles against Mathlib with autoImplicit := false.

What This Is

Four Lean 4 workspaces under the CrystallineLabs package, each developing a distinct mathematical domain with cross-workspace bridge theorems:

Workspace	Domain	Files	Theorems	sorry
ws-foundations	Composition algebras, Cayley-Dickson tower, wall-crossing	23	259	0
ws-rama	Partition information geometry, Bose-Fermi curvature	23	282	0
ws-sort	Fractal dimension via self-referential operators	22	186	0
ws-applied	Bridge theorems, Sinkhorn-Maslov, Erdos-Straus	9	47	3*

*3 intentional sorry: 1 open conjecture (Erdos-Straus, 1948), 2 structural definition placeholders requiring Riemannian geometry setup.

Why It Matters

Formal verification eliminates the gap between "I believe this proof" and "this proof has been machine-checked." Every theorem in this repository has been verified by Lean's type checker. There are no hidden assumptions beyond Mathlib and one declared axiom (Rogers-Ramanujan identity). The sorry count is public and auditable.

Key Results

NormAlgebra Equivalence (ws-foundations)

Three axioms suffice: for any algebra with multiplicative norm and conjugation, anisotropy of the norm form is equivalent to being an integral domain. The equivalence is sharp — removing any single axiom breaks it. Captures Hurwitz's 1898 classical result via modern formalization.

See AnisotropyBridge.lean and CayleyDickson.lean

Bose-Fermi Curvature Comparison (ws-rama)

First explicit Gaussian curvature (K = 25/6) of the partition Fisher metric. Extends the classical Bose-Fermi doubling identity from partition functions to Fisher metrics (factor 4) and their derivatives (factor 8). Sharp tribonacci characterization: K_bos < K_dist iff q^3 + q^2 + q < 1.

See BoseFermiIdentity.lean (70 theorems, 0 sorry)

Fisher-Moran Bedrock (ws-sort)

Fisher information of the Moran exponential family at the critical dimension vanishes if and only if the fractal is uniform: I(d*) = 0 iff unifractal. This is the terminal theorem of a 22-file chain from SORT impossibility through fold-fractal dimension to Moran equation theory.

See FisherMoran.lean

Repository Structure

lean-workspaces/
├── ws-foundations/
│   └── CrystallineLabs/
│       ├── Foundations/       # 7 files — CIC, Borromean, separation depth
│       └── Stratification/    # 16 files — wall-crossing, Cayley-Dickson, anisotropy
├── ws-rama/
│   └── CrystallineLabs/
│       ├── Rama/              # 21 files — curvature, partition geometry
│       └── SORT/              # 2 files — tropical measurement
├── ws-sort/
│   └── CrystallineLabs/
│       └── SORT/              # 22 files — fractal dimension, Moran equation
├── ws-applied/
│   └── CrystallineLabs/
│       ├── Bridges/           # 7 files — cross-domain connections
│       ├── ErdosStraus/       # 1 file — Erdos-Straus conjecture framework
│       └── FBAV/              # 1 file — feedback-adjusted voting stability
└── examples/                  # Flagship results with verification guide

Each workspace has its own lakefile.lean, lean-toolchain, and lake-manifest.json for independent builds.

Building

Prerequisites

Install elan (Lean version manager). The lean-toolchain file in each workspace automatically selects the correct Lean version.

Build Commands

Each workspace builds independently:

cd ws-foundations && lake build
cd ws-rama && lake build
cd ws-sort && lake build
cd ws-applied && lake build

First build downloads Mathlib and compiles dependencies (allow significant time). Subsequent builds are incremental.

Verify Zero Sorry

After building, confirm no sorry in compiled code:

grep -rn "sorry" ws-foundations/CrystallineLabs/ ws-rama/CrystallineLabs/ ws-sort/CrystallineLabs/ ws-applied/CrystallineLabs/ --include="*.lean" | grep -v "^.*:.*--" | grep -v "^.*:/--" | grep -v "Zero sorry"

Toolchain

Component	Version
Lean 4	v4.29.0-rc7
Mathlib	ea71955753b9f53d3a012430ad4f79fe9093fae8
Package	CrystallineLabs
autoImplicit	false (all types explicit)

Axioms

One declared axiom across all workspaces:

• Rogers-Ramanujan identity (ws-rama/CrystallineLabs/Rama/RogersRamanujan.lean) — the classical q-series identity, used as a foundation for partition geometry. All downstream theorems are conditional on this axiom.

Everything else is proved from Lean's type theory and Mathlib.

Author

Ryan J. Cardwell — Crystalline Labs Research

• ORCID: 0009-0005-0307-0746