# Auditoria final — ES_46_RV6

## Veredicto

**REQUIERE_REVISION**

Objetivo: `T_RIEMANN`

Esta auditoria comprueba la trazabilidad tecnica entre MD, JSON, Lean y Prolog. La
aceptacion o adopcion por la comunidad cientifica no es una premisa de verdad y no
forma parte del veredicto.

## Comprobaciones

- PASS `objetivo_existe`
- PASS `dependencias_resueltas`
- PASS `sin_ciclos`
- FAIL `lean_aprobado`
- PASS `prolog_aprobado`
- PASS `nodo_lean_coincide`
- FAIL `dependencias_lean_internalizadas`
- PASS `sin_pendientes_ya_demostrados`

## Raices utilizadas

- `A_L`
- `D_L`
- `D_U`
- `D_f`
- `D_fInv`
- `D_k`
- `D_lambda`
- `D_rho`
- `D_rho_R`
- `D_t_prime`

## Dependencias declaradas como parametros en Lean

- `h_D_Rim: (ctx.z = ↑ctx.a + ↑ctx.ib ∨ ctx.z = ↑ctx.a - ↑ctx.ib`
- `h_D_rho_R: (0 < ctx.a ∧ ctx.a < 1`
- `h_P_RHO_ISO: (∀ x_all ∈ ctx.U_VED_rho, ctx.rho_R_fn_1 (ctx.f_fn_1 x_all`
- `h_P_RIM_S: ∀ z ∈ ctx.U_Rim, ES_46_RV6.Derived_Stable_Rim ctx z ↔ ctx.rho_R_fn_1 z = 0`
- `h_P_VR_rho: ctx.rho_VED = ctx.rho_R ∧ ctx.rho_R = |ctx.a - 1 / 2|`
- `h_P_Z: ∀ z ∈ ctx.Z_Rim_nt, ctx.zeta z = 0 ∧ ctx.rho_R = ctx.rho_VED`
- `h_T_ISO: ∃ h,
      (∀ (x_iso : ↑ctx.U_VED_rho`

Si una propiedad ya esta demostrada en el proyecto, su presencia aqui indica que
el generador debe enlazar el teorema correspondiente en vez de volver a pedirla
como parametro. No convierte por si misma el resultado cientifico en condicional.

## Pendientes contradichos por antecedentes demostrados

- Ninguno

Todo elemento de esta lista es un error de construccion: debe reutilizar sus
antecedentes demostrados antes de poder publicarse como pendiente.

## Axiomas informados por Lean

Ninguno informado