== Proyecto: ES_46_RV6 ==
INICIO [Lean ES_46_RV6.lean]: lake env lean Proyectos\ES_46_RV6\ES_46_RV6.lean
Directorio: C:\Users\vedq\Desktop\desarrollo\SRC-VED\DEMUESTRA
EN CURSO [Lean ES_46_RV6.lean]: 15 s sin nueva salida; el proceso sigue activo.
EN CURSO [Lean ES_46_RV6.lean]: 30 s sin nueva salida; el proceso sigue activo.
EN CURSO [Lean ES_46_RV6.lean]: 45 s sin nueva salida; el proceso sigue activo.
EN CURSO [Lean ES_46_RV6.lean]: 60 s sin nueva salida; el proceso sigue activo.
EN CURSO [Lean ES_46_RV6.lean]: 75 s sin nueva salida; el proceso sigue activo.
Proyectos\ES_46_RV6\ES_46_RV6.lean:131:20: warning: Variable name `ctx` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _ctx

Note: This linter can be disabled with `set_option linter.unusedVariables false`
Proyectos\ES_46_RV6\ES_46_RV6.lean:181:16: warning: Variable name `ctx` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _ctx

Note: This linter can be disabled with `set_option linter.unusedVariables false`
Proyectos\ES_46_RV6\ES_46_RV6.lean:199:16: warning: Variable name `ctx` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _ctx

Note: This linter can be disabled with `set_option linter.unusedVariables false`
Proyectos\ES_46_RV6\ES_46_RV6.lean:246:18: warning: Variable name `ctx` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _ctx

Note: This linter can be disabled with `set_option linter.unusedVariables false`
Proyectos\ES_46_RV6\ES_46_RV6.lean:284:14: warning: Variable name `ctx` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _ctx

Note: This linter can be disabled with `set_option linter.unusedVariables false`
Proyectos\ES_46_RV6\ES_46_RV6.lean:316:20: warning: Variable name `ctx` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _ctx

Note: This linter can be disabled with `set_option linter.unusedVariables false`
Proyectos\ES_46_RV6\ES_46_RV6.lean:425:25: warning: Variable name `ctx` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _ctx

Note: This linter can be disabled with `set_option linter.unusedVariables false`
Proyectos\ES_46_RV6\ES_46_RV6.lean:469:14: warning: Variable name `ctx` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _ctx

Note: This linter can be disabled with `set_option linter.unusedVariables false`
Proyectos\ES_46_RV6\ES_46_RV6.lean:478:15: warning: Variable name `ctx` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _ctx

Note: This linter can be disabled with `set_option linter.unusedVariables false`
Proyectos\ES_46_RV6\ES_46_RV6.lean:507:16: warning: Variable name `ctx` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _ctx

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ES_46_RV6.Node_T_RIEMANN (ctx : ES_46_RV6.FormalContext) : Prop
FIN [Lean ES_46_RV6.lean]: OK, codigo 0, duracion 92.1 s.

DEMOSTRACION PENDIENTE: ES_46_RV6.lean compila, pero su resultado principal aun no esta demostrado.

Construccion Lean valida: 1 archivo(s) compilado(s); 1 con demostracion pendiente.

Construccion global correcta, con demostraciones pendientes en: ES_46_RV6
2026-09-23 00:53:13,206 - Demuestra - INFO - ==================================================
2026-09-23 00:53:13,206 - Demuestra - INFO - Sistema DEMUESTRA inicializado.
2026-09-23 00:53:13,207 - Demuestra - INFO - Raiz Lake compartida: C:\Users\vedq\Desktop\desarrollo\SRC-VED\DEMUESTRA
2026-09-23 00:53:13,207 - Demuestra - INFO - Log guardado en: C:\Users\vedq\Desktop\desarrollo\SRC-VED\DEMUESTRA\logs\demuestra.log
2026-09-23 00:53:14,356 - Demuestra - INFO - Lake disponible: Lake version 5.0.0-src+819816b (Lean version 4.33.1)
2026-09-23 00:53:14,362 - Demuestra - INFO - Compilando C:\Users\vedq\Desktop\desarrollo\SRC-VED\DEMUESTRA\Proyectos\ES_46_RV6\ES_46_RV6.lean desde C:\Users\vedq\Desktop\desarrollo\SRC-VED\DEMUESTRA
2026-09-23 00:54:46,529 - Demuestra - INFO - Construccion Lean valida con 1 demostracion(es) pendiente(s).