Independent researcher in mathematical physics. No lab, no institution: a laptop, published data, and about two and a half years of asking what can be measured and what cannot.

I want a way to map and measure everything as simply as light does.

The work runs through one idea: a projector, the operator that keeps part of a space and discards the rest, carries both the geometry and the bookkeeping of a physical system. Most of my papers follow that idea into a different problem: entanglement, gravity, knots, many-body motion, arithmetic.

Results are graded by what supports them: proved, derived, recognised or measured. The ones that can be machine-checked are checked in Lean.

Jeromie Beasley · GitHub dicipler-pixel · X @d1c1pler · YouTube @AtlasMemoriae · atlas-memoriae.dicipler.workers.dev · ORCID 0009-0006-4645-5643

How this work is made. The ideas and research direction are mine. AI tools do most of the computation, coding, Lean proof writing and drafting, and every repository says how in its AI_USE.md. The Lean kernel, not the AI, is what checks the proofs: every repository's CI builds them, replays them in Lean's independent kernel checker, and audits for sorry and extra axioms. What is not proved is listed in each LIMITATIONS.md.

• sqrt-lower-bound-lean: a complete Lean proof of a published theorem (Pozsgay and Vona's square-root lower bound on operator entanglement, finite core). 661 theorems.
• coboundary-k3-lean: the Sym(3) coboundary constant of the complete complex is k/3 for 4 ≤ k ≤ 8, both bounds checked in Lean.
• coxeter-rank2-lean: rank-two Coxeter groups are dihedral, against Mathlib's own objects.
• nonnormality-connection-energy-lean: the newest paper; non-normality of a graph operator equals its connection energy.

Repository	What it is	Check
sqrt-lower-bound-lean	A complete, dependency-closed Lean 4 proof of the square-root lower bound on operator entanglement (Pozsgay and Vona) for the finite rectangular core to which their Lemma 4.1 reduces an integrable brickwork circuit.
coboundary-k3-lean	Lean 4 proofs that the Sym(3) permutation coboundary constant of the complete complex K_k equals k/3 for 4 ≤ k ≤ 8: explicit cochains attain the Chapman–Lubotzky bound, and gauge minima are checked exhaustively in the kernel.
coxeter-rank2-lean	Lean 4 proofs that the rank-two Coxeter group I₂(m+2) is the dihedral group of order 2(m+2), checked against Mathlib's own Coxeter and dihedral objects, with exact integral certificates for the finite and affine rank-two cases.
nonnormality-connection-energy-lean	Lean 4 formalization of Non-Normality Is Connection Energy (Jeromie Beasley)
arithmetic-kakeya-finite-bridges	Lean 4 proofs of two finite bridges for the Epoch FrontierMath arithmetic Kakeya problem: rational forcing equals integer forcing, and every completed configuration leaves two independent surviving labels on each nonempty cut. Companion to the Certified Obstructions paper.
dirac-time-lean	Lean 4 proofs of the finite mathematics behind 'The Dirac Time of the Gigantefermion': the predictive quotient of a linear continuation map and observation, and related results. What is not formalized is listed in LIMITATIONS.md.
electron-screening-lean	Lean 4 proofs for 'Electron Screening in Metal Deuterides': for an increasing, convex rate, yield-space averaging never gives a fit below the campaign mean, and a two-energy ratio cancels energy-independent factors.
elemental-peeling-lean	Lean 4 proofs of the finite algebra behind 'Elemental Peeling and What the Boundary Retains': what a specified removal takes away, what later records can recover, force recovery from readings, and exclusion certificates.
emergent-transport-lean	Lean 4 proofs for 'Intrinsic Emergent Transport Geometry': off-diagonality of projector commutators, first variation of the trace-log ledger, the projector–metric correspondence, and subspace overlap as a squared Frobenius norm.
event-horizon-lean	Lean 4 proofs for 'Beyond the Event Horizon': four-body shape space as qutrit Bures geometry, the coplanar wall w₃ = 0 where the metric blows up as 1/(6w₃), the triangular transport block, and a nonnegative discriminant away from the wall.
filament-fracture-lean	Lean 4 proofs for a five-dimensional non-normal stability operator: the embedding of an exact Jordan block, the factorised characteristic polynomial, a closed-form resolvent norm 1/ε on |z|² = ε|μ| + ε², and the transient-growth threshold |μ| > 2b.
foft-lean	Lean 4 proofs for 'Foundational Operator Field Theory on Stratified Manifolds': the isotropic vacuum operator K₀ = −ΛI, the regularised ledger offset, vanishing odd moments under chirality, and the exact stress-budget rate of the relaxation flow.
gravity-ledger-lean	Lean 4 proofs of the finite projector algebra behind 'The Ledger Outlives the Metric': projector tangents, the signed metric, the reciprocal determinant, the local overlap cap and the projector-overlap Taylor bridge.
iqgt-grassmannian-lean	Lean 4 proofs that the quantum geometric tensor Tr(ΠVW) is a Frobenius inner product, so its Gram matrix is positive semidefinite and the Berry curvature is bounded by the quantum metric, in every finite dimension.
light-ledger-lean	Lean 4 proofs of the finite algebra behind 'Light Keeps the Ledger': boundary elimination, the transition census, optical response as a reweighted metric, and scope counterexamples.
matter-at-a-scale-lean	Lean 4 proofs for 'Matter at a Scale': stretching or shifting an operator leaves its eigenspaces unchanged and its departure from normality is a pure ratio; plus the units relations around the Bohr rod a₀m = ħ/(αc).
neutrinos-leave-lean	When the Neutrinos Leave: decoupling history and the PBH formation threshold. Code, run logs, data and Lean. Jeromie Beasley
offset-lean	Lean 4 formalization of the Offset results
price-of-a-direction-lean	Lean 4 proofs of the exact finite results of 'The Price of a Direction': two unit directions at angle θ overlap as cos²θ and separate by sin²θ, trackability thresholds, and what survives when two directions coalesce.
ramanujan-challenge-lean	Lean 4 proofs of the exact algebra in Jeromie Beasley's Ramanujan Challenge (Technion, 2026) submissions: determinant identities, a Pochhammer product, a telescoping cubic, nilpotent leading-order algebra and a partial-fraction decomposition. Limits rely on numerics.
relational-atlas-lean	Lean 4 proofs of the bridges in 'The Operator-First Relational Atlas' that are graded THEOREM and whose content is finite algebra.
small-diophantine-lean	Lean 4 certificates for the surfaces z² + (y² + a)z + x³ + bx + c = 0 from the Epoch 'smallest unsolved equations' problem, and the integrality of an explicit rational section.
spectral-stability-lean	Lean 4 proofs for 'Spectral Stability Across Obstruction Interfaces': the transport part A = αJ ⊗ Δ₁ is symmetric with real spectrum, so every departure from normality of H_N(ε) comes from εE and starts at first order in ε.
spectral-stress-lean	Lean 4 proofs for 'Spectral Stress on a Conservative Matrix Field': band curvatures of a flat connection sum to zero exactly, pair terms factorise under one operator relation, and the amplitude −5√2/16 and 4:1 ratio follow in ℚ(√2).
square-case-lean	Lean 4 proofs of the finite algebra behind the four-body binary-collision wall and 'The Square Case': when the intrinsic flow keeps a tangent on the wall σ_L(W) = LWLᵀ, and kernel consequences for positive-semidefinite W.
suns-lean	Lean 4 proofs for 'Transient Structure at Solar Rigidity Interfaces': the square-root law at an exceptional point, the pair exchange recorded by a loop around it, the single-valued ledger, and modal decay versus transient growth.
three-body-lean	Lean 4 proofs for 'The Three-Body Problem, Operator-First': the Gram operator of the 120° distance projection has spectrum {cos²ϑ, 1}, so syzygy and equilateral degeneracies are of different kinds.
upg-lean	Lean 4 proofs of the finite feedback algebra behind 'Universal Projector Geometry': [H, P] = 0 exactly when the coupling block B = 0, and the commutator, redistribution operator and memory Gram BBᵀ vanish together.
votkp-lean	lean 4 proofs for VOTKP (The Vector of Traits Kept under Peeling) and Two Trees in One Ball — Jeromie Beasley
what-russell-saw-lean	Lean 4 proofs for 'What Russell Saw', a reading of Walter Russell's paired-motion universe: oscillator energy conservation (not the reading itself) and that his planet speeds v ∝ 1/a correspond to an inverse-cube pull.
what-tesla-saw-lean	Lean 4 proofs of what Tesla's own circuit laws imply (period law, tuning rule, octave, magnification m = pL/R), checked against numbers from the Colorado Springs Notes and his patents, with every hypothesis written out.
what-transport-keeps-lean	Lean 4 proofs of the exact algebra of 'What Transport Keeps': conserved pairings, the Catalan cancellation and its certificates, the reconstructed Catalan matrix field, and stress, projector and boundary-response identities.
yang-mills-lean	Research record for 'Retained Geometry and Certified Gauge Cutoffs': the Sept 8 paper and scripts, Sept 9 spatial SU(3) calculations, and Lean 4 checks of specified finite algebra. No continuum mass gap is claimed.

Mathlib. Two pull requests to Mathlib were closed without being merged: #43703 (rank-two Coxeter groups are dihedral) was closed on 7 October 2026 under Mathlib's policy on AI use, and #43951 (a trace identity for differences of idempotents) was closed by a reviewer on 18 September 2026. Because this work is AI-assisted, these results now live in standalone repositories that depend on Mathlib, as Mathlib's contribution guide suggests.

Elsewhere. Proposed to Lean Pool and to the Tau Ceti roadmap (both awaiting review).

All 35 Zenodo records listed here (newest first). Each concept DOI always opens the latest version.

• ramanujan-normality-diagnostic: builds the companion matrix of a linear recurrence and splits it into symmetric and skew parts, a quick signal for whether a simple closed form is likely to exist.
• earth-moon-kakeya-certificates: certificates and reproduction supplement for Certified Obstructions and Exact Forcing.
• formula-pictures: pictures that are equations; every pixel is computed from a formula.

• rhythm-game-one: a four-key rhythm game in plain HTML, Canvas and Web Audio.
• Oceans-Journey: a small ocean adventure game.

Copyright (c) 2026 Jeromie Beasley. Code and proofs: MIT. Written text: CC BY 4.0. See LICENSING.md.