# Evaluacion Lean - ES_46_RV6

## Veredicto

**COMPILA; TRADUCCION PARCIAL**

Fecha UTC: `2026-09-22T22:54:46+00:00`
Codigo de salida: `0`
Compilacion Lean: **CORRECTA**
Cobertura de traduccion: **PARCIAL**
Salida completa: `logs\LEAN_ES_46_RV6.log`
Diagnostico: Lean compilo el archivo generado sin errores. Hay formulas del Markdown no integradas o no traducidas; se detallan por nodo. La compilacion no juzga la verdad matematica.
Accion: Revisar primero la extraccion y la seleccion de cada formula pendiente; separar fallos del traductor de condiciones que el Markdown deja abiertas.
Estado matematico: **NO DETERMINADO**. Un fallo de traduccion o de prueba no es una contradiccion del Markdown.

## Archivos Lean evaluados

- `ES_46_RV6.lean`

## Teorema resultado

No identificado.
Resultado pendiente: `ES_46_RV6.Node_T_RIEMANN`
Construccion fiel completa: **no**
Demostracion completa: **no**

## Aseveraciones

- `D_U`: construccion **COMPLETA**; demostracion **NO APLICA**
- `D_t_prime`: construccion **INCOMPLETA**; demostracion **NO INICIADA**
- `A_L`: construccion **COMPLETA**; demostracion **PENDIENTE**
- `D_lambda`: construccion **COMPLETA**; demostracion **NO APLICA**
- `D_L`: construccion **COMPLETA**; demostracion **NO APLICA**
- `D_k`: construccion **COMPLETA**; demostracion **NO APLICA**
- `D_rho`: construccion **INCOMPLETA**; demostracion **NO INICIADA**
- `D_Rim`: construccion **INCOMPLETA**; demostracion **NO INICIADA**
- `D_rho_R`: construccion **INCOMPLETA**; demostracion **NO INICIADA**
- `D_f`: construccion **INCOMPLETA**; demostracion **NO INICIADA**
- `D_fInv`: construccion **INCOMPLETA**; demostracion **NO INICIADA**
- `P_COORD`: construccion **INCOMPLETA**; demostracion **NO INICIADA**
- `T_ISO`: construccion **COMPLETA**; demostracion **PENDIENTE**
- `P_ST`: construccion **COMPLETA**; demostracion **PENDIENTE**
- `P_RHO_ISO`: construccion **COMPLETA**; demostracion **PENDIENTE**
- `P_v`: construccion **AMBIGUA**; demostracion **NO INICIADA**
- `P_RIM_S`: construccion **INCOMPLETA**; demostracion **NO INICIADA**
- `P_a`: construccion **COMPLETA**; demostracion **PENDIENTE**
- `P_VED_Inv`: construccion **INCOMPLETA**; demostracion **NO INICIADA**
- `P_VED_E`: construccion **COMPLETA**; demostracion **PENDIENTE**
- `P_VED_I`: construccion **INCOMPLETA**; demostracion **NO INICIADA**
- `P_VR_rho`: construccion **COMPLETA**; demostracion **PENDIENTE**
- `P_VED_K_E`: construccion **COMPLETA**; demostracion **PENDIENTE**
- `P_VR_E`: construccion **INCOMPLETA**; demostracion **NO INICIADA**
- `P_VED_K_I`: construccion **COMPLETA**; demostracion **PENDIENTE**
- `P_Z`: construccion **COMPLETA**; demostracion **PENDIENTE**
- `P_VED_R_C`: construccion **COMPLETA**; demostracion **PENDIENTE**
- `T_RIEMANN`: construccion **INCOMPLETA**; demostracion **NO INICIADA**
- `P_VED_Completo`: construccion **INCOMPLETA**; demostracion **NO INICIADA**
- `P_VS`: construccion **INCOMPLETA**; demostracion **NO INICIADA**
- `P_F`: construccion **COMPLETA**; demostracion **PENDIENTE**
- `P_F1`: construccion **COMPLETA**; demostracion **PENDIENTE**
- `P_W`: construccion **INCOMPLETA**; demostracion **NO INICIADA**
- `P_F2`: construccion **AMBIGUA**; demostracion **NO INICIADA**
- `P_F3`: construccion **COMPLETA**; demostracion **PENDIENTE**
- `D_Lap`: construccion **INCOMPLETA**; demostracion **NO INICIADA**
- `P_Lap_Z`: construccion **COMPLETA**; demostracion **PENDIENTE**

## Afirmaciones de origen pendientes

- `D_rho` formula 2 (ES_46_RV6.md:316:D_rho:formula-2): **FORMALIZED_UNPROVEN**; origen: `\boxed{ 0\le\rho\le\frac12. }`
- `D_Rim` formula 4 (ES_46_RV6.md:912:D_Rim:formula-4): **UNTRANSLATED**; origen: `\boxed{ Z_{\rm Rim}^{\rm triv} = \{-2,-4,-6,\ldots\} = \{-2m:m\in\mathbb N^+\}. }`
- `D_rho_R` formula 3 (ES_46_RV6.md:1003:D_rho_R:formula-3): **FORMALIZED_UNPROVEN**; origen: `\boxed{ 0\le\rho_R<\frac12, }`
- `D_rho_R` formula 4 (ES_46_RV6.md:1003:D_rho_R:formula-4): **FORMALIZED_UNPROVEN**; origen: `\boxed{ a = \frac12+\varepsilon\rho_R. }`
- `D_rho_R` formula 5 (ES_46_RV6.md:1003:D_rho_R:formula-5): **FORMALIZED_UNPROVEN**; origen: `\boxed{ z_{\varepsilon,\pm} = \frac12 + \varepsilon\rho_R \pm ib. }`
- `D_rho_R` formula 6 (ES_46_RV6.md:1003:D_rho_R:formula-6): **FORMALIZED_UNPROVEN**; origen: `\boxed{ \rho_R = \left| \Re(z)-\frac12 \right|. }`
- `D_fInv` formula 1 (ES_46_RV6.md:1100:D_fInv:formula-1): **FORMALIZED_UNPROVEN**; origen: `\boxed{ f^{-1}:U_{\rm Rim}^{\rho}\longrightarrow U_{\rm VED}^{\rho}. }`
- `P_RIM_S` formula 2 (ES_46_RV6.md:1169:P_RIM_S:formula-2): **FORMALIZED_UNPROVEN**; origen: `\boxed{ z\in Z_{\rm Rim}^{\rm nt} \Longrightarrow \operatorname{Stable}_{\rm Rim}(z) \Longrightarrow \rho_R(z)=0. }`
- `P_VED_I` formula 2 (ES_46_RV6.md:418:P_VED_I:formula-2): **FORMALIZED_UNPROVEN**; origen: `\boxed{ \rho=\frac12 }`
- `P_VR_E` formula 2 (ES_46_RV6.md:1312:P_VR_E:formula-2): **FORMALIZED_UNPROVEN**; origen: `\boxed{ \text{estado estable} \iff a=\frac12. }`
- `T_RIEMANN` formula 2 (ES_46_RV6.md:1472:T_RIEMANN:formula-2): **FORMALIZED_UNPROVEN**; origen: `\boxed{ a=\frac12. }`
- `P_VED_Completo` formula 2 (ES_46_RV6.md:494:P_VED_Completo:formula-2): **UNTRANSLATED**; origen: `n\to\infty`
- `P_VS` formula 3 (ES_46_RV6.md:557:P_VS:formula-3): **UNTRANSLATED**; origen: `\boxed{ \lim_{n\to\infty}G(n)=0. }`
- `P_W` formula 8 (ES_46_RV6.md:639:P_W:formula-8): **UNTRANSLATED**; origen: `\boxed{ dt'\to0. }`
- `D_Lap` formula 9 (ES_46_RV6.md:764:D_Lap:formula-9): **UNTRANSLATED**; origen: `\boxed{ Z_{\rm VED\to Lap} = \left\{ \frac12 \pm i\frac{2\pi}{k\lambda} : k\in\mathbb N^+ \right\}. }`

## Condiciones logicas pendientes

- `P_RIM_S` (ES_46_RV6.md:1169:P_RIM_S:formula-2): `\boxed{ z\in Z_{\rm Rim}^{\rm nt} \Longrightarrow \operatorname{Stable}_{\rm Rim}(z) \Longrightarrow \rho_R(z)=0. }`. A -> (B -> C) no permite concluir C solo a partir de A: tambien hay que establecer B. Esta condicion no esta verificada.

## Alcance

Lean 4 solo certifica las definiciones, teoremas e inferencias formalizadas en los archivos Lean evaluados.

La ausencia de verificacion no equivale a refutacion. Este evaluador distingue la compilacion global del estado individual de cada aseveracion; no presenta como falsas las que no haya podido comprobar.

## ADEC

Evaluacion manual; no automatizada hasta que ADEC admita url_json.