Home / Lean
Kernel-checked formal layer
Complete WCT Lean Coverage Lean coverage is generated from the same registry used by the equation and SymPy pages. The symbolic outcome remains separate from kernel-checked declarations.
142 canonical objects
80 mapped definitions or declarations
62 unmapped or incomplete
Boundary: mapped does not mean equal proof strength. Dimensional lemmas, algebraic support, definitions, partial theorems, counterexamples, and TODOs remain distinct.
Registry v2.0.0 · generated 2026-08-21T08:57:49+00:00 · machine-readable registry
M1 Curvature-locking functional PROVED · PARTIAL SUPPORT M2 Nonsingular curvature operator and Lyapunov candidate PROVED · PARTIAL SUPPORT M3 Finite-band spectral selector PROVED · PARTIAL SUPPORT M4 Dimensional stability threshold PROVED · PARTIAL SUPPORT M5 Curvature-bounded computation PROVED · PARTIAL SUPPORT M6A Unified linear operator DEFINITION M6B Nonlinear curvature operator PROVED · ALGEBRAIC SUPPORT M7 Full curvature-wavefield equation PROVED · PARTIAL SUPPORT M8 Curvature-acoustic cosmology system UNMAPPED E1A Curvature-rate density PROVED · DIMENSIONAL SUPPORT E1B Curvature spectral rate PROVED · DIMENSIONAL SUPPORT E2 Weighted loop average PROVED · ALGEBRAIC SUPPORT E3 Loop-locking action PROVED · ALGEBRAIC SUPPORT E4 Covariant locking solution PROVED · PARTIAL SUPPORT E5 Effective-wavenumber chain PROVED · ALGEBRAIC SUPPORT E6 Mass-curvature law PROVED · DIMENSIONAL SUPPORT E7 Solenoidal mass law PROVED · DIMENSIONAL SUPPORT E8 Corrected weighted-lock identity PROVED · PARTIAL SUPPORT E9 Phase-flux constitutive relation PROVED · ALGEBRAIC SUPPORT E10 Radial shell quantization PROVED · ALGEBRAIC SUPPORT E11 Phase winding PROVED · ALGEBRAIC SUPPORT E12 Finite-band dispersion rail PROVED · ALGEBRAIC SUPPORT E13 Band-pass amplitude evolution PROVED · PARTIAL SUPPORT E14 Band-pass Lyapunov functional PROVED · PARTIAL SUPPORT E15 Modal growth bound UNMAPPED E16 Linear spectral concentration PROVED · PARTIAL SUPPORT E17 Nonsingular curvature-feedback operator PROVED · PARTIAL SUPPORT E18 WCT Lyapunov candidate PROVED · PARTIAL SUPPORT E19 Gap-curvature scaling PROVED · PARTIAL SUPPORT E20 Higher-order cavity quadratic sector PROVED · PARTIAL SUPPORT E21 Second-derivative Euler-Lagrange equation UNMAPPED E22 Effective metric ansatz PROVED · PARTIAL SUPPORT E23 Enthalpic curvature relation UNMAPPED E24 Sobolev embedding threshold PROVED · PARTIAL SUPPORT E25 Critical Sobolev exponent DEFINITION E26 Corrected curvature $L^2$ bound DEFINITION E27 Finite-energy confinement DEFINITION E28 Corrected alpha-drop exponent PROVED · ALGEBRAIC SUPPORT E29 Entropy-drop pruning PROVED · ALGEBRAIC SUPPORT E30 Spectral entropy UNMAPPED E31 Conditional entropy-production bound UNMAPPED E32 Subexponential exploration condition PROVED · ALGEBRAIC SUPPORT E33 Corrected support-entropy relation PROVED · ALGEBRAIC SUPPORT E34 Energy-entropy conversion UNMAPPED E35 Curvature-locked fixed point UNMAPPED E36 Discrete WCC update PROVED · PARTIAL SUPPORT E37 Bandlimit from energy PROVED · PARTIAL SUPPORT E38 Spatial channel capacity PROVED · PARTIAL SUPPORT E39 Polynomial update bound UNMAPPED E40 WCC complexity identification UNMAPPED E41 Curvature-bounded configuration count PROVED · PARTIAL SUPPORT E42 Theta-information relation UNMAPPED E43 Curvature-entropy tradeoff UNMAPPED E44 Theta eigenmode problem UNMAPPED E45 Corrected quality factor PROVED · ALGEBRAIC SUPPORT E46 Plasma-cavity curvature match UNMAPPED E47 Corrected power balance PROVED · ALGEBRAIC SUPPORT E48 Curvature-gap stability criterion UNMAPPED E49 Corrected effective-mass gap law PROVED · ALGEBRAIC SUPPORT E50 Phase-coherence functional PROVED · PARTIAL SUPPORT E51 Curvature-gradient commutator PROVED · ALGEBRAIC SUPPORT E52 Curvature gain and gradient loss UNMAPPED E53 Curvature pressure density PROVED · ALGEBRAIC SUPPORT E54 Resonance-lock condition UNMAPPED E55 Curvature-induced effective potential UNMAPPED E56 Phase-wall criterion UNMAPPED E57 Swift-Hohenberg shell operator PROVED · PARTIAL SUPPORT E58 Band-selective Green kernel PROVED · ALGEBRAIC SUPPORT E59 Projection onto a dominant annulus PROVED · ALGEBRAIC SUPPORT E60 Center-manifold amplitude equation UNMAPPED E61 Pattern-formation threshold PROVED · ALGEBRAIC SUPPORT E62 Spectral energy concentration PROVED · ALGEBRAIC SUPPORT E63 Entropic mode selection UNMAPPED E64 Corrected selected wavelength PROVED · PARTIAL SUPPORT E65 Critical Sobolev exponent DEFINITION E66 Gagliardo-Nirenberg interpolation DEFINITION E67 Failure of $H^2 o L^\infty$ above three dimensions PROVED · PARTIAL SUPPORT E68 Localized energy estimate DEFINITION E69 Corrected high-regularity curvature bound DEFINITION E70 Dimensional stability criterion PROVED · PARTIAL SUPPORT E71 Physical computation resource bound UNMAPPED E72 Curvature-pruned search space PROVED · PARTIAL SUPPORT E73 Polynomial verification UNMAPPED E74 Curvature separation conjecture UNMAPPED E75 Physical-oracle impossibility UNMAPPED E76 WCC complexity equivalence UNMAPPED E77 Mutual-information decay UNMAPPED E78 Fisher-information curvature bound TODO E79 Entropy-production rate UNMAPPED E80 Landauer-type bound UNMAPPED E81 Corrected coherence length DEFINITION E82 Information-geometry tensor UNMAPPED CLE1 Curvature-locking functional UNMAPPED CLE2 Corrected curvature-lock Euler-Lagrange equation UNMAPPED CLE3 Curvature-locking condition UNMAPPED CLE4 Locked-field equation PROVED · ALGEBRAIC SUPPORT CLE5 Thin/product-torus Laplacian PROVED · PARTIAL SUPPORT CLE6 Separation ansatz UNMAPPED CLE7 Periodic angular mode family UNMAPPED CLE8 Selected torus eigenmode PROVED · PARTIAL SUPPORT CLE9 Electron radius from curvature PROVED · ALGEBRAIC SUPPORT CLE10 Curvature scalar chain PROVED · ALGEBRAIC SUPPORT G1 Log-periodic ghost modulation PROVED · ALGEBRAIC SUPPORT EX Logarithmic field representation PROVED · ALGEBRAIC SUPPORT EY Log-curvature evolution PROVED · ALGEBRAIC SUPPORT EZ Cole-Hopf reduction PROVED · ALGEBRAIC SUPPORT FA Filament-localization condition PROVED · ALGEBRAIC SUPPORT CM1 Fundamental field evolution UNMAPPED CM2 Curvature-spectral tilt UNMAPPED CM3 Potential from curvature UNMAPPED CM4 Horizon-entry potential decay UNMAPPED CM5 Curvature-acoustic oscillators UNMAPPED CM6 Sound speed from curvature feedback UNMAPPED CM7 Curvature diffusion UNMAPPED CM8 Initial conditions UNMAPPED CM9 First-order mode system PROVED · ALGEBRAIC SUPPORT CM10 Tight-coupling drag UNMAPPED CM11 Curvature damping envelope PROVED · ALGEBRAIC SUPPORT CM12 Dimensionless power spectrum DEFINITION CM13 Peak metrics DEFINITION CM14 Peak-response interpretation UNMAPPED CM15 WCT angular scaling UNMAPPED CM16 Acoustic horizon DEFINITION CM17 Curvature-energy closure UNMAPPED CM18 Minimal cosmology closure set UNMAPPED CM19 Acoustic speed from curvature equation of state UNMAPPED CM20 Theta-based expansion ansatz UNMAPPED TOP1 Closed spectral-loop representation UNMAPPED TOP2 WCT loop-energy functional UNMAPPED TOP3 Irreversible gradient flow PROVED · PARTIAL SUPPORT TOP4 Emergent-topology criterion UNMAPPED TOP5 WCT dynamical codimension UNMAPPED TOP6 Spectral topology bands UNMAPPED TOP7 Topological mass proxy PROVED · PARTIAL SUPPORT TOP8 Holonomy non-invariance UNMAPPED TOP9 Protein-particle structural correspondence UNMAPPED CORR1 Full Lyapunov candidate UNMAPPED CORR2 Mean-amplitude spectral closure PROVED · ALGEBRAIC SUPPORT CORR3 Spectral-weight notation UNMAPPED CORR4 Macro-micro control parameter UNMAPPED CORR5 Entropy-curvature coupling UNMAPPED CORR6 Isoelectronic-flow alignment UNMAPPED
Equation
Select an equation
UNMAPPED
← Previous Next →