Equation
Select an object
Lean—
SymPy—
Scope—
Empirical—
Current effective status—
Baseline status—
Kernel-checked formal layer
WCT Lean Coverage
Start with proof strength, then drill into individual canonical objects. Lean coverage is kept separate from symbolic checks and empirical validation.
Wave Confinement Theory (WCT) is a research program developed by Richard J. Reyes beginning in 2025. This page documents the kernel-checked formal-coverage layer within the public WCT research corpus. Publication dates and DOI records are indexed in the publication archive, with claim-level chronology in the priority registry.
Theorem inventory ↗
Registry v2.0.0 · generated 2026-11-04T00:26:03+00:00
Proof-strength map
What has actually been formalized?
These categories describe the strength of Lean coverage, not the truth of WCT as a physical theory. Mapped does not mean equal proof strength.
Stronger formal coverage92 mapped · 50 unmappedNo coverage
Lean coverage against symbolic outcome
The two layers are independent. A SymPy PASS does not imply a Lean proof, and an absence of formal coverage is not evidence of falsity. Select a cell to list its objects.
October 30, 2026 · synchronized Lean registry
New equation-specific proofs
92 of 142 canonical objects have maintained equation-specific Lean support; 50 are registry-only. The current batch adds nine objects beyond the earlier 83-object snapshot: TOP6, CM3, CM4, CM10, CM15, CM20, E44, E60 and E82. Earlier E15, CLE6 and CLE7 reductions are included in the reported count.
These are kernel-checked, narrowly scoped results such as scalar compatibility conditions, contractions, phase obstructions, and Gram positivity. They are not proofs of full nonlinear WCT dynamics, the cosmological equations or physical validation. TOP6 establishes an inverse-square scaling obstruction for the unnormalized statistic; its full geometric knot-isotopy argument is not yet encoded in Lean.
Independent mathematical proof track
Manuscript-scale Lean formalization
The math repository formalizes precise mathematical results on nonlinear PDEs, Fourier operators, spectral dynamics and geometric estimates. These manuscript results are separate from the 142-object WCT registry above. They do not automatically change an object's canonical coverage category; equivalence requires a statement-by-statement match of definitions, domains, hypotheses and conclusions.
14 / 14Original mathematical manuscripts marked complete
5 / 5Additional F11/F12 manuscripts marked complete
6Supplementary manuscripts marked formalized
2,794Source theorem/lemma declarations, including private lemmas
Related proofs and their exact scope
| WCT ID | Separate mathematical manuscript result | Evidence |
|---|---|---|
| E16 | Linear spectral concentration in the fourth-order linear flow, with explicit hypotheses and convergence bounds. | PaperLean |
| M2 / E17 | Smooth regularized curvature multiplier, uniform bounds and controlled small-regularization limits. | PaperLean |
| E26 | Conditional curvature L² estimate, with explicit counterexample for the historical denominator. | PaperLean |
| M3 / E57 | Whole-space Fourier-shell damping semigroup, operator domain and energy identities. | PaperLean |
| E58 | Continuum Green multiplier and sharp L² resolvent bound. | PaperLean |
| E59 | Fixed-annulus orthogonal Fourier projection on the torus, including energy splitting and best approximation. | PaperLean |
| E61 | Swift–Hohenberg spectrum, semigroup and linear stability threshold. | PaperLean |
| E62 | Spectral-energy fractions and exact Fourier projectors, including continuous-spectrum scope. | PaperLean |
| E68 | Localized gradient-energy dimensional classification, corrected estimates and counterexamples. | PaperLean |
Source snapshot: October 30, 2026. The maintained manifest records 154 imported Lean modules using Lean 4.23.0 / Mathlib 4.23.0. Its completion labels describe kernel-checked statements under their encoded assumptions, not peer review or physical validation. E18 and E69 remain listed as unformalized supplementary manuscripts. The canonical object browser below continues to reflect its separately dated WCT registry snapshot.
Object browser
All 142 objectsUNMAPPED