Kleis
Universal Verification Platform for Mathematics, Business Rules, and Beyond
🔬 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.
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)