EEML mathematics verification, 16 September 2026, website v0.23

NL
Dit dossier maakt de rekencontrole reproduceerbaar. De oorspronkelijke
bronnen staan in a6/, lean-kern/ en de twee losse scripts in de hoofdmap.
Zij zijn ongewijzigd en kunnen historische claims en fouten bevatten.
De nieuwe controles en de ruwe resultaten staan in math-audit-20260916/.
De webpagina's /wiskunde, /fysica, /artikel en /axiom-audit geven de actuele
interpretatie. Niet ieder oud onderzoek is hier opnieuw uitgevoerd.

EN
This bundle makes the verification reproducible. Original sources in a6/,
lean-kern/ and the two root scripts are unchanged historical material.
They can contain incorrect claims and implementation errors. New checks
and raw outputs are in math-audit-20260916/. Current interpretations are
on /wiskunde, /fysica, /artikel and /axiom-audit. This is not a reproduction
of every earlier research project, a new converged K3 spectrum, or a
physical derivation of alpha. No observational outcomes were audited.

PYTHON REPRODUCTION (from the extracted bundle directory)
Tested: Python 3.14.4, NumPy 2.3.5, SciPy 1.18.1, SymPy 1.14.0, mpmath 1.3.0.
Create an isolated environment and install requirements.txt, then run:

python -m venv .venv
.venv/bin/python -m pip install -r requirements.txt
OPENBLAS_NUM_THREADS=2 .venv/bin/python math-audit-20260916/audit_checks.py
OPENBLAS_NUM_THREADS=2 .venv/bin/python math-audit-20260916/spectrum_check.py
.venv/bin/python math-audit-20260916/run_originals.py

Scripts overwrite only their local output files. The spectrum check uses
1600 points (400 random complex lines), seed 20260916, and the stored k=3
metric G. It compares the original energy matrix with an independently
assembled real-coordinate Dirichlet form on the same data. The constant
basis combination is checked directly, as are analytic derivatives by
finite differences. It is a diagnostic, not a replacement production run.
The old k=3,...,6 eigenvalue files are included as historical inputs.

KEY RESULTS
* Kern.lean and Orthogonaliteit.lean: exit 0, no sorry/admit/new axioms.
* Exponential weight is conditional on the theorem's half-line assumptions.
* Four derivative/symmetry statements hold, not a universal S=A+K+I split.
* Quartic K3: chi=24, signature=-16; Ricci-flat scalar a4=4/15;
  scalar zeta(0)=-11/15 after excluding the single constant zero mode.
* Laplace example left mass tends to sqrt(3)/(1+sqrt(3)).
* Eta product and partition arithmetic reproduce, with limited scope.
* Old energy matrix gives the constant function a nonzero Rayleigh quotient.
* alpha_u_toets.py has a factor-two mismatch between equation and function.
* Gauge-only running mismatch reproduces. Measured couplings are inputs;
  adding a measured low-energy difference is not an alpha(0) prediction.
* The original group script reproduces algebraic degeneracy blocks, not
  a physical nine-line gravitational-wave prediction.
* Full a6 curvature runs, classification scans, high-k convergence and
  all empirical predictions are outside this completed check.

LEAN REPRODUCTION
Toolchain: leanprover/lean4:v4.34.0-rc1
Mathlib commit: e2d86c683b522c3f887029ed2335a0838cb71b8c
Dependency manifest: mathlib-lake-manifest.json (copied from checked build).
Use an installation of elan/lake and a checkout of mathlib4 at this commit.
Obtain its dependency/cache files as required by Mathlib, then from that
checkout run (replace /path/to/bundle with the extracted absolute path):

lake env lean /path/to/bundle/lean-kern/Kern.lean
lake env lean /path/to/bundle/lean-kern/Orthogonaliteit.lean

Both original files compiled unchanged in the recorded audit. Printed
axiom dependencies: propext, Classical.choice, Quot.sound. These are
standard Lean foundations, not new EEML physical axioms. Formal claims
are the actual theorem statements; prose comments can overinterpret them.

FILE INTEGRITY
manifest.json records SHA-256 hashes of the included files. The manifest
and ZIP cannot include their own hashes. A matching hash establishes file
identity, not mathematical validity. Numerical roundoff may vary across
BLAS and library environments. The full private website backups, media,
Git metadata and server configuration are deliberately not in this bundle.
