Kleis

Universal Verification Platform for Mathematics, Business Rules, and Beyond

557+
Unique Cloners
1416
Commits
29
Architecture Decisions

🔬 Type System

Hindley-Milner type inference with complete algebraic foundations

🎯 Verification

Z3 theorem prover integration for axiom verification

🌐 Universal

Mathematics, business rules, network protocols, and more

📝 Self-Hosting Architecture

Bootstrap in Rust, extensible in Kleis

📄 Research

Machine-verified papers produced entirely in Kleis — axioms, proofs, numerics, and typesetting from a single reproducible source.

The Spectral Comb and the Riemann Hypothesis: A Proof via Fixed-Point Theory

Identifies the completed zeta function ξ(s) with the characteristic polynomial of an antisymmetric matrix. Six theorems, machine-checked in Lean 4, verified by Z3. 11 pages. View source (.kleis)

The Riemann Zeta Function as a Transfer Function: A State-Space Perspective on Hilbert–Pólya

Reframes the spectral comb as a state-space realization of 1/ζ(s). Antisymmetry forces Re = 1/2 by a one-line identity; convergence covered by Connes' theorem and six published spectral approximation results. 18 references, 13 executable tests. View source (.kleis)

Flat Galactic Rotation Curves from Projected Ontology

Derives flat rotation curves and the Tully-Fisher relation (M ∝ v⁴) without dark matter. 14 axioms, 4 theorems, all verified by Z3. View source (.kleis)

Electrodynamics as a Theorem of Projected Ontology

Derives Maxwell's equations from two axioms and d²=0 on a Lorentzian manifold. Identifies the exterior derivative as an admissible POT kernel; classifies electrodynamics as the unique admissible gauge sector. 14 verified examples, 15 pages. View source (.kleis)

Confinement as Fiber Non-Invariance: The Admissibility Boundary in Projected Ontology

Derives structural confinement from kernel non-admissibility without assuming quantum mechanics. Identifies the admissibility defect with the Lie bracket; connects to Wilson loops, the Gauss law, and color singlets. 6 theorems, 19 Z3-verified examples. View source (.kleis)

Admissibility Restoration: The Structural Necessity of Symmetry-Breaking Fields in Projected Ontology

Derives the necessity of Higgs-like fields from kernel admissibility without assuming quantum mechanics. Shows that mass vs. confinement reduces to whether algebraic non-linearity is compensable; the three-class gauge classification emerges as geometry within a single Lie algebra. 7 theorems, 3 figures, 16 Z3-verified examples. View source (.kleis)

The Half-Derivative Gap: Machine-Verified Structural Diagnosis of Navier-Stokes Smoothness

Proves that no scalar Sobolev inequality chain can exclude Navier-Stokes blow-up: the exponent sum theorem shows the critical threshold is a+b=2 while the best scalar bound gives a+b=3. The missing unit of exponent reduction must come from non-scalar geometric structure. 13 Z3-verified tests, 2 figures, 6 tables. View source (.kleis)

Geometric Depletion of Vortex Stretching: Machine-Verified Conditions for Navier-Stokes Regularity

Reduces Navier-Stokes regularity to the sign of a single scalar observable Q — the off-diagonal pressure-Hessian projection — and proves via two vanishing theorems that Q=0 in all z-translationally symmetric flows, localizing the sign mechanism to genuinely 3D vortical geometry. 16-step reduction chain, 5 figures, 7 tables, Z3-verified thresholds. View source (.kleis)

From Self-Protection to Interaction Depletion: The Pressure-Hessian Sign in Curved and Interacting Vortex Tubes

Computes Q for curved vortex tubes and interacting configurations, establishing six results: curvature unlocks Q but is anti-depleting; the tidal gradient mechanism from perpendicular tube interaction produces the first constructive depleting sign with scaling law Q = Cγ²Re²(σ/d)³, C ≈ −0.55. Z3-verified self-consistency shows blow-up is self-undermining: the perturbative regime improves and depletion strengthens as Re → ∞. 13-step reduction chain, 3 Z3-verified theory files, 15 pages. View source (.kleis)

From Interaction Depletion to Conditional Regularity: Angular Averaging, Many-Body Locality, and the Dynamical Closure of the Pressure-Hessian Sign

Closes three remaining gaps in the NS regularity program: isotropic angular averaging preserves the depleting sign (Ciso ≈ −0.43), many-body corrections are bounded by Re−3/2 per extra interaction, and the dynamical closure reduces the enstrophy growth exponent from p = 3/2 to p = 3/4, crossing the critical blow-up threshold p = 1. States a conditional regularity theorem: under the tube-structure hypothesis, interaction depletion prevents finite-time blow-up. Complete 16-step reduction chain, 4 Z3-verified theory files. View source (.kleis)

GRAND FINALE The Self-Undermining Singularity: Unconditional Regularity of 3D Navier-Stokes Solutions

Proves that smooth Navier-Stokes solutions remain smooth for all time under enstrophy-barycenter centering. All five hypotheses (H1–H5) are derived from blow-up dynamics; Propositions 8.4–8.5 are proved from published ingredients. The three analytical gaps (A, B, C) are closed. 214 machine-verified examples across 23 theory files, 153 Z3-verified theorems. 33 pages. View source (.kleis)

EPILOGUE The Kernel and the Fluid: Navier-Stokes Regularity as Projected Ontology

Philosophical epilogue observing that the Biot-Savart kernel K(x) = x/(4π|x|³) is a concrete instance of POT's Green's function projection. Every step of the regularity proof — energy, localization, cancellation, confinement, depletion — is a kernel property. The framework reduces to four statements: physical laws are kernel properties; observables are the image; gauge freedom is the null space; there is nothing else. 8 pages. View source (.kleis)

VOLUME VII Renormalization as Projected Ontology: The Theory That Was Never Divergent

Formalizes QFT renormalization as projection kernels composable via ITCM into a single hypergeometric composite kernel KQFT = FP ∘ Kren ∘ Kpath. Reduces the Yang–Mills mass gap to a spectral condition on Hankel-order asymmetry: Δ > 0 iff μYM ≠ νYM with IR-regular weight function. Numerical demonstration via Bessel operator eigenvalues confirms monotonic gap opening. 34 pages, 4 figures, 40 Z3-verified examples. View source (.kleis)

VOLUME VIII A Conditional Reduction of the Yang–Mills Mass Gap Problem via Integral Transform Composition

Capstone of the 14-file POT program. States the Main Reduction Theorem: under five assumptions A–E, 4D Yang–Mills has a positive mass gap. The mathematical scaffold B+C+D (Level A/B) converts the sign of the gluon anomalous dimension γ > 0 into a Sturm–Liouville spectral gap scaling as σ2/3 · 1.750 for linear confinement. 14 theory files, 400+ Z3-verified examples. View source (.kleis)

VOLUME IX Yang–Mills Vacuum Stability as a Classical Spectral Property

Z3-verified proof that γ > 0 implies a positive spectral gap Δ > 0 for the Bessel–Sturm–Liouville operator. Five lemmas chain IR exponent classification, confining potential growth, Weyl self-adjointness, Rellich–Molchanov discreteness, and gap positivity into a single theorem. For linear confinement (γ = ½), Δ = 1.7498 · σ2/3 from Airy zeros. 12 structures, 34 Z3-checked examples. All mathematics pre-1953. View source (.kleis)

EPILOGUE The Mass Gap as a Classical Spectral Phenomenon: A Reinterpretation

Companion essay to Volume VIII. The mass gap decomposes into a classical spectral mechanism (Sturm–Liouville, Watson, Weyl, Borg — all pre-1946) and a quantum realization problem. No quantization, path integrals, or particle physics appears in the mechanism. QFT contributes one bit — the sign of the anomalous dimension — and one structural bridge. The difficulty was never the mechanism. The difficulty is the realization. View source (.kleis)

VOLUME X Projection Singularities: Why Physics Has No Infinities

All physical infinities — QFT ultraviolet divergences and GR curvature singularities — are projection singularities: terms in a formal series outside the admissible domain of the representation. The Hadamard projection (a coefficient-wise filter on Laurent indices) is the unique linear idempotent that extracts the observable and annihilates the infinity. Two end-to-end worked examples on real QFT loop integrals (Passarino–Veltman A0 and B0) reproduce textbook renormalization with no subtraction. 20 references, 29 Z3-verified structural results, 13 machine-verified computations. View source (.kleis)