Lean Ridgelet

Lean Ridgelet formalizes the mathematics of neural networks represented by integrals, and the ridgelet transforms that recover their coefficients from a target function. It uses Lean 4, a proof assistant that checks mathematical proofs, and Mathlib, its community mathematics library. The project connects neural-network approximation theory with Fourier analysis, operator theory, and group representations.

Start with the Blueprint. This is a mathematical guide with definitions, theorem statements, and links to the corresponding Lean code. You can read it without installing Lean or knowing its syntax.

The mathematical question

A neural network with one hidden layer has the form

Here is an input, is an activation such as ReLU, and are the network parameters. Its continuous analogue replaces the sum by an integral over weights and biases:

The function assigns a coefficient to each neuron. Given a target , we ask how to construct , when it reconstructs , and how to describe all coefficients representing the same function. A ridgelet transform analyzes against a family of ridge functions:

For compatible activation and analysis functions, the central identity is

An admissible pair has a finite, nonzero reconstruction constant , so dividing the coefficients by this constant reconstructs . The equations above introduce the Euclidean convention; the individual theorems specify their function spaces, integrability, parameter measures, and Fourier normalizations. Some identities hold almost everywhere or as limits in a function-space norm.

For machine-learning researchers, these results explain representation, universality, and parameter nonuniqueness. A nonzero element of changes the coefficients while leaving the represented function unchanged. For analysts, the same questions lead to inversion formulas, adjoints, Hilbert-space decompositions, and intertwining operators. Finite-network approximation requires a further discretization argument, with its own hypotheses. The repository provides formal definitions and proofs; training algorithms and numerical experiments are outside its present scope.

What is formalized

The four theory tracks have complementary roles. Each overview follows the source paper's publication order; the detail pages follow proof dependencies.

The L2 solution geometry is implemented in Operator/UnitarySynthesis.lean: under its stated hypotheses, every solution is the minimum-norm solution plus an element of the synthesis kernel. The general unitary formulation makes this result reusable beyond a particular activation.

In the Schur approach, equivariance means that transforming the input commutes with applying the operator. When the input representation is irreducible, a bounded reconstruction operator with this property is a scalar multiple of the identity. The scalar must still be shown to be nonzero. HA/AdjointReconstruction.lean proves that a bounded, nonzero intertwining analysis operator satisfies with under the irreducibility hypothesis. This gives reconstruction using the adjoint as synthesis.

General-purpose results are developed in LeanRidgelet/ToMathlib/, with Mathlib-only imports, for reuse and possible upstream contribution. They include Radon and Fourier analysis, convolution estimates, integration in , Schur's lemma, Haar measures, and geometry for Helgason--Fourier analysis. The ToMathlib Blueprint organizes these results by topic. Their location in this repository does not imply acceptance into Mathlib.

Proof status and scope

Lean checks a theorem relative to its stated hypotheses and any axioms in its dependencies. A successful build alone does not establish that every theorem has a completed proof: Lean also accepts sorry, an explicit placeholder for an unfinished proof. This project audits those placeholders and their dependencies by declaration name.

The current boundary is recorded in audit/Assumptions.lean:

• L2: four named targets remain for encoding/readout, normalized finite-width approximation, and finite null relations. The Hilbert-space theory uses transported coordinates; extending the classical Fourier-dilation integral identification through the full completion remains separate work.
• L1: the implemented function-level results are proved. The paper's full distributional scope, including some balancing cases and distribution-valued activations, remains outside this pass.
• Fourier slice: three named targets remain: the SVD Jacobian and Helgason--Fourier inversion on real hyperbolic space and the space of positive definite matrices. The conditional reconstruction theorems are proved independently of these placeholders.
• Harmonic analysis: no named target remains. The adjoint reconstruction route is proved under its explicit boundedness, equivariance, irreducibility, and nonzero-transform hypotheses, and the Section 7 quadratic-form endpoint with an activation fixed in advance is proved at a fixed shape matrix (quadratic_fixedShape_reconstruction), with the explicit constant ∫ 𝓕σ(ζ) conj(𝓕ψ(ζ)) π^m / (|2πζ|^m |det A|) dζ; the full-affine-parameter form was withdrawn because the analysis transform has infinite parameter energy there.

Thus the allowlist currently contains seven unfinished proof roots and no dependent endpoint. The audit rejects unlisted uses of sorryAx, source-level project axioms, and unreviewed proposition-valued fields in project structures and typeclasses. Other declarations may use the standard classical axioms propext, Quot.sound, and Classical.choice. Differences from the papers are explained in the affected module's Deviations from the article section and in the Blueprint overview. Consult those statements when reusing a result.

The dependency graph and Blueprint summary help navigate the development; the assumption audit determines the proof-placeholder boundary.

Build the Lean project

The project uses Lean and Mathlib v4.32.0, pinned by lean-toolchain and lake-manifest.json. Install Lean using the official setup guide, then run:

git clone https://github.com/shosonoda/lean-ridgelet.git
cd lean-ridgelet
lake exe cache get
lake build

To inspect statements interactively, open the clone in VS Code with the Lean 4 extension and start with one of the roadmap files linked above. For example, create Explore.lean in the repository root:

import LeanRidgelet.Operator.UnitarySynthesis

#check LeanRidgelet.unitarySynthesis_comp_unitaryRidgelet
#check LeanRidgelet.unitarySolution_iff_kernel_translate
#check LeanRidgelet.unitaryMoorePenroseInverse_unique_minimal
#print axioms LeanRidgelet.unitaryMoorePenroseInverse_unique_minimal

The editor displays the complete hypotheses and conclusion. #print axioms also reports the theorem's transitive axiom dependencies. Check the same file from a terminal with lake env lean Explore.lean. Import a specific module when reusing a result; import LeanRidgelet loads the whole library, including the named unfinished targets.

The Lean badge is generated from the version pinned in lean-toolchain. After changing that file, refresh and check the generated badge block with:

python3 scripts/update-readme-badges.py
python3 scripts/update-readme-badges.py --check

Run the repository-wide audit for proof placeholders, kernel axioms, and proposition-valued fields in project-defined structures and typeclasses with:

./scripts/audit-assumptions.sh

The Assumption audit badge reports the dedicated GitHub Actions workflow that runs this command.

Build the documentation

Generate the Verso Blueprint with:

./scripts/build-blueprint.sh

The build is incremental. LeanRidgeletBlueprint/Parts/ provides separate cached subtrees for L2, L1, Fourier slice, harmonic analysis, and ToMathlib. Child pages use topic-specific imports, and ToMathlib is split into eight independent analytic, geometric, and representation-theoretic pages. Lake can therefore reuse unrelated page and subtree .olean files. The rendered site is cached under _out/blueprint-cache/; an unchanged input fingerprint skips regeneration and postprocessing. Use ./scripts/build-blueprint.sh --force for a complete regeneration.

The documentation workflow also restores the preceding successful run's project and Verso .olean files. Lake validates their dependency hashes and rebuilds only changed modules and their dependents; Mathlib's much larger build tree continues to come from lake exe cache get.

Preview the complete generated site through a local HTTP server:

python3 -m http.server 8000 --directory _out/blueprint

Then open http://localhost:8000/html-multi/. Verso's standard multi-page renderer preserves a five-part hierarchy with twenty-nine theory pages. Its nodes connect the informal statements to their Lean declarations. A direct page URL is, for example, http://localhost:8000/html-multi/l2/foundations/. Stop the server with Ctrl-C. Serving over HTTP ensures that Blueprint preview data and browser modules are loaded correctly. The left sidebar is Verso's generated table of contents: L2, L1, Fourier slice, harmonic analysis, and ToMathlib are the top-level parts, with overview, detail, or topic pages nested beneath them.

Two generated chapters follow them. http://localhost:8000/html-multi/Dependency-Graph/ draws every Blueprint node and its (uses := ...) edges, coloured by formalization status; http://localhost:8000/html-multi/Blueprint-Summary/ reports coverage counts, the most-used statements, and the nodes that carry no Lean declaration yet. The graph page loads d3 and d3-graphviz from a CDN at view time and therefore needs network access in the browser.

Definition panels include the Lean implementation beginning at := when the declaration belongs to this project.

Repository layout

• LeanRidgelet/: formal definitions and proofs
• LeanRidgeletBlueprint/: Verso Blueprint chapters
• audit/: machine-checked assumption audit
• scripts/: build and audit commands
• formalization.yaml: project metadata in the formalization.yaml self-reporting standard (sources, main results, placeholder counts, fidelity, review status)

Generated build and documentation trees are ignored by Git. GitHub Pages builds the Blueprint in Actions and deploys it as an artifact.