Certificates and Lean sources

Five Lean files, 59 theorem declarations. Formal arithmetic, numerical checks and physical assumptions have separate scopes.

Cinco archivos Lean, 59 declaraciones de teoremas. La aritmética formal, las comprobaciones numéricas y las hipótesis físicas tienen alcances distintos.

Full anomaly cancellation and admissible orbifold backgrounds remain open. The lift audit is exact computation, not Lean. Passing a file-integrity check does not replay its mathematical proof.

Download complete evidence bundle / Descargar evidencia · SHA-256 manifest · Archive hash · Verification receipt

Hypothesis comparison / Comparación de hipótesis

Derivations and scope / Derivaciones y alcance · Exact witnesses and checks / Testigos y controles · Replay / Repetición. Ten additional Lean declarations cover rational algebra. Exact CMS covariance factorization and three pointwise derivative enclosures are executable certificates. Full potential error bounds and an observed fit remain pending.

Diez declaraciones Lean adicionales cubren álgebra racional. La factorización exacta de la covarianza CMS y tres cotas puntuales de derivadas tienen certificados ejecutables. Siguen pendientes la cota del error total del potencial y el ajuste observado.

Data structure, downloads and replay / Estructura de datos, descargas y repetición

What measured data can establish / Qué aportan los datos medidos

Measurements can test a physical model that predicts compatible observables. The hypothesis card currently keeps the GHU reconstruction and CMS measurements separate. The quantization module supplies no mass or production-rate prediction. Neither module claims an observed fit.

Las medidas permiten contrastar modelos con predicciones compatibles. La ficha de hipótesis mantiene separadas la reconstrucción GHU y la medición CMS. El módulo de cuantización no aporta predicciones de masas ni tasas. Ninguno afirma un ajuste observado.

How certificates, the module and physics fit together · Cómo encajan certificados, módulo y física. Watch the animated explanation · Ver la explicación animada.

Certified matched profiles / Perfiles certificados tras matching

Download proof and certificate / Descargar demostración y certificado · Functional proof and scope · Independent Sage receipt · Boundary research Demo.

Two finite-width probes, t=1/4 and t=1/2, distinguish uniform and triangular responses after matching the same source, pole s=1/100 and residue R=1/2. Written continuum proof plus 228 independent Sage checks (recorded version 10.8). No new Lean formalization, full GHU certificate, thin-layer rate or experimental fit. Extract the ZIP and run sage -python verify.py receipt.json.

Dos sondas de anchura finita distinguen respuestas uniforme y triangular tras igualar fuente, polo y residuo. Demostración del continuo escrita y 228 comprobaciones Sage independientes (versión registrada 10.8). Sin nueva formalización Lean, certificado GHU completo, tasa de capa delgada ni ajuste experimental.

Finite neutral complex / Complejo neutro finito

Proof, witnesses and verifier / Demostración, testigos y verificador · Written proof · Symbolic verification receipt.

Exact ranks and quotient dimension on s=0 and s!=0. Standard determinant criteria and rank-nullity; no mathematical novelty or continuous-domain certificate. Replay with SymPy: python verify.py certificate.json.

Rangos exactos y dimensión del cociente en s=0 y s!=0. Criterios conocidos de menores y rango-nulidad. No certifica el dominio continuo, una masa del Higgs ni una novedad matemática.

Continuous neutral isolation / Aislamiento neutro continuo

Proof and verifier / Demostración y verificador · Hypotheses and continuous proof · Exact replay receipt · Video · Vídeo.

For 0 < theta ≤ 1/4 in the fixed active block: positive simple isolated first eigenvalue. Means, traces, min-max and Temple inequality; published methods reused. Written analytic proof and 26 exact symbolic checks, with 20 invalid inputs or corruptions rejected. Not a Lean formalization or a Wilson-derivative certificate. Replay with SymPy: python verify.py certificate.json --self-test.

Modelo fijo condicionado; tres ceros desacoplados conservados por separado. La prueba continua y la repetición algebraica tienen alcances distintos. Derivada Wilson, RZW, vacío, corrientes y dirección física del Higgs siguen pendientes.

Archive SHA-256: 84055f3d9bda525b905b7946f27503f92ecd3427985e4d81d97224a135d03f22

Reproduce

Use Lean 4.27.0 and Python 3. For the numerical audits install their documented dependencies; Sage 10.9 is used by the Sage scripts. Run from the extracted bundle root:

python proof/verify_bundle.py
lean proof/su7/SU7Certificates.lean
python proof/quantization/verify_lean.py --check
python proof/quantization/verify_spin.py --check
python proof/u2/verify_lean.py --check
node proof/quantization/test_lab.mjs --check
node proof/quantization/test_spin.mjs --check
python proof/lifts/background_lift_checks.py --check
python proof/boundary-research/certify.py --check
python proof/hypothesis/certify.py --check

The hypothesis replay requires Node, NumPy, SciPy and SymPy. The universal theorems assume the characteristic-class dictionary externally. Closed spin-four periods use Wu parity externally. U(2) integrality does not construct a supergravity spectrum. The 26 SU(7) theorems certify finite weight/seed algebra; the infinite Fourier interval calculation is a separate certificate.

Quantization scope and Sage replay · U(2) scope · Clifford audit · Boundary certificates