Primera tanda, 14 de octubre de 2026. Las demostraciones algebraicas, los certificados de aritmética exacta y las comprobaciones numéricas tienen alcances diferentes. El potencial completo y el contraste experimental siguen pendientes.
Resultados y testigos exactos JSON · Fuente Lean · Repetir comprobaciones · Registro Lean
Con H=fH·δθ y fH constante y distinto de cero, el coeficiente de Hⁿ es V⁽ⁿ⁾(θH)/(n! fHⁿ). La masa al cuadrado es V″/fH²; el coeficiente cuadrático del potencial es mH²/2. El vértice y el coeficiente del potencial difieren por el factorial. Es una expansión local, no la afirmación de que el potencial sea un polinomio cuártico global.
Lean demuestra la identidad polinómica truncada sobre racionales, usando r=1/fH como entrada. SymPy comprueba por separado la sustitución y las derivadas. No se ha formalizado en Lean el cálculo diferencial sobre los reales ni el resto de Taylor de V.
Para D=1+Q cos(nθ), Q independiente de θ y D>0, sean a=D′/D, b=D″/D, c=D‴/D, d=D⁽⁴⁾/D. Entonces (log D)′=a, (log D)″=b−a², (log D)‴=c−3ab+2a³ y (log D)⁽⁴⁾=d−4ac−3b²+12a²b−6a⁴. Las recurrencias usan a′=b−a², b′=c−ab y c′=d−ac. Lean verifica su álgebra; SymPy deriva log D independientemente.
Se leen las 225 cadenas decimales de HEPData como fracciones exactas. El testigo C=L diag(d) Lᵀ reconstruye todas las entradas y sus 15 pivotes son positivos. Como L es triangular con diagonal unidad, para z≠0 se tiene zᵀCz=Σdᵢ(Lᵀz)ᵢ²>0. Esto certifica la matriz publicada redondeada; no elimina la incertidumbre de la medición ni certifica sus dígitos no publicados.
Cᵢⱼ²≤CᵢᵢCⱼⱼ se comprueba exactamente para todos los pares. Con diagonales positivas, implica |ρᵢⱼ|≤1 y ρᵢᵢ=1. El script compara cada entrada con la matriz que utiliza realmente el Lab. La factorización y las 225 entradas se verifican en Python con fracciones; no se presentan como un teorema matricial general en Lean.
Para densidades x y anchuras w, T=wᵀx>0, y=x/T y J=I/T−xwᵀ/T². Se verifica exactamente wᵀy=1, wᵀJ=0, rango(J)=14 y (JCJᵀ)w=0. La positividad semidefinida se sigue de zᵀJCJᵀz=(Jᵀz)ᵀC(Jᵀz)≥0. JCJᵀ es propagación de primer orden; no es la covarianza exacta de cualquier cociente aleatorio. La matriz normalizada oficial sigue siendo una referencia distinta y no se suman ambas mediciones como independientes.
En tres entradas racionales Q=−0,999; −0,95; 0,8, con armónicos 1; 2; 1 y θ=1/10, se acotan seno y coseno mediante polinomios de Taylor y |resto|≤|nθ|ᵏ/k!. Las derivadas de seno y coseno están acotadas por uno. La aritmética de intervalos usa fracciones exactas; se demuestra D>0 en cada intervalo. Las cotas de error comparan el resultado binario del motor con la función matemática en esas entradas decimales exactas e incluyen su conversión a coma flotante.
Estas cotas se refieren a las derivadas del logaritmo en tres puntos. No incluyen el cálculo Bessel de Q, ni una integral completa, ni un dominio continuo de parámetros. El refinamiento de cuadratura de los nueve casos es un diagnóstico de convergencia, no una cota rigurosa. Faltan cotas del integrando cerca de q=0, de la cola infinita y del error de cuadratura, además de justificar el intercambio de derivación e integración. El mínimo global sigue comprobado por muestreo.
Persiste la discrepancia aproximada del 7,4 % entre el ajuste cuártico publicado y su tabla. El motor principal omite bottom y usa entradas electrodébiles aproximadas. No hay certificado de completitud física ni un ajuste observado de estos nueve casos a CMS.
Desde la raíz del repositorio, con Lean 4.27.0, Node, Python, NumPy, SciPy y SymPy instalados: python proof/hypothesis/certify.py --check. Sin --check se regeneran el registro y los resultados. Los SHA-256 vinculan los resultados a las fórmulas, datos y código. La verificación falla si no coincide con el certificado guardado.
Los archivos de esta carpeta y sus entradas forman parte del paquete descargable del Lab. Las pruebas Lean no contienen huecos de demostración; sus dependencias fundacionales se registran para cada teorema.
Fuentes: Funatsu et al., potencial y autoacoplamientos GHU; CMS, matriz de covarianza publicada. Las demostraciones de normalización y las cotas elementales se explican aquí.