Fundamentos y verificación
Estado acreditado
667 unidades humanas cerradas, 2573 dependencias directas y 297 candidatos seleccionados. TLOG tiene 0 resultados compilados o verificados en Lean. El inventario cubre todas las unidades; la preparación comprueba identidad, fuentes y dependencias, no aceptación del kernel.
Obligaciones
| Obligación | Estado | Alcance |
|---|---|---|
| AG-03 | Abierta | Revisión independiente completa de las pruebas |
| AG-04 | En curso | Rama RM PA, wire PR χ_T, generadores aritméticos y Prov* seleccionado |
| AG-05 | Abierta | Revisión editorial integral; el render web tiene QA específico |
R01 y R02 aportan 236 y 815 regresiones Python. Son evidencia operacional, no verificación Lean. Los códigos grandes se acompañan de circuitos exactos y límites explícitos.
M_ext es ZF clásica sin AC/BPI. ZF_obj, PA_obj y RM se mantienen separados. Verdad de Lean, satisfacción de una estructura y existencia de derivación objeto son relaciones distintas. No se presupone consistencia ni existencia de modelos de ZF_obj.
Classical.choice como axioma del kernel en una prueba externa no equivale automáticamente a AC objeto, pero debe justificarse que no fortalece la afirmación atribuida a ZF sin elección. Se auditan por separado axiomas del kernel, axiomas objeto y puentes de interpretación.
La evidencia futura exige módulo real importado por la biblioteca, commit, fuente y manifest fijos, lake build –wfail, #check y #print axioms, ausencia de sorryAx y de axiomas personalizados no revisados, revisión de firma y correspondencia, hipótesis y alcance. Compilación y revisión semántica son puertas separadas. Un build no verifica automáticamente un capítulo entero.