import Mathlib

set_option maxHeartbeats 100000

namespace ES_46_RV6

structure FormalContext where
  D : ℝ
  D_rho_R : ℝ
  DivergesToInfinity : ℝ → Prop
  E : ℝ
  F : ℝ
  F3 : ℝ
  G : ℝ
  G_fn_1 : ℝ → ℝ
  I : ℝ
  L : ℝ
  L_fn_2 : ℕ → ℝ → ℝ
  Lap : ℝ
  Mc : ℝ
  P : ℝ
  P_F3 : ℝ
  P_VR : ℝ
  P_VR_fn_1 : ℝ → ℝ
  R_VED : ℝ
  R_VED_fn_2 : ℕ → ℝ → ℝ
  Rim : ℝ
  S : ℝ
  Sch : ℝ
  Stable : ℝ
  Stable_Rim : ℝ
  Stable_Rim_fn_1 : ℂ → Prop
  T : ℝ
  T_fn_2 : ℕ → ℝ → ℝ
  Text_cierre_exacto_en_fase : Prop
  Text_cierre_no_estable : Prop
  Text_clase_estable : Prop
  Text_clase_no_estable : Prop
  Text_clasifica_su_localizaci_n_transversal : Prop
  Text_estado_estable : Prop
  Text_estado_no_estable : Prop
  U : ℝ
  U_Rim : Set (ℂ)
  U_Rim_rho : Set (ℂ)
  U_Sch : ℝ
  U_VED : ℝ
  U_VED_cerrado : ℝ
  U_VED_rho : Set (ℝ)
  VED : ℝ
  VED_to_Lap : ℝ
  VR : ℝ
  Z_Rim : ℝ
  Z_Rim_nt : Set (ℂ)
  Z_Rim_triv : Set (ℝ)
  Z_VED_to_Lap : Set (ℂ)
  a : ℝ
  b : ℝ
  bT : ℝ
  b_fn_2 : ℕ → ℝ → ℝ
  b_k : ℝ
  c : ℝ
  cerrado : ℝ
  d : ℝ
  dist : ℝ
  dist_fn_2 : ℝ → Set (ℕ) → ℝ
  ds : ℝ
  dt : ℝ
  dt_fn_1 : ℝ → ℝ
  dt_prime : ℝ
  dt_prime_to_0 : ℝ
  dv : ℝ
  e : ℝ
  f : ℝ
  f_fn_1 : ℝ → ℂ
  f_inv : ℝ
  f_inv_fn_1 : ℂ → ℝ
  h : ℝ
  hc : ℝ
  i : ℂ
  ib : ℝ
  ibT : ℝ
  k : ℕ
  lambda : ℝ
  ldots : ℝ
  lim : ℝ
  lim_n_to_INFINITY : ℝ
  longleftrightarrow : ℝ
  m : ℕ
  mathcal_E : ℝ
  mathcal_E_VED : Set (ℕ × ℕ)
  mathcal_I : ℝ
  mathcal_I_VED : ℝ
  n : ℝ
  n_s : ℝ
  n_to_INFINITY : ℝ
  nt : ℝ
  onda : ℝ
  rho : ℝ
  rho_R : ℝ
  rho_R_fn_1 : ℂ → ℝ
  rho_VED : ℝ
  rho_VED_fn_1 : ℝ → ℝ
  s : ℂ
  s_PM : ℝ
  sqrt : ℝ → ℝ
  sum : ℝ
  t : ℝ
  t_prime : ℝ
  triv : ℝ
  v : ℝ
  v_onda : ℝ
  v_to_c : ℝ
  varepsilon : ℝ
  x : ℝ
  z : ℂ
  z_varepsilon_PM : ℝ
  zeta : ℂ → ℂ

-- FORMAL_NODE: D_U
-- SOURCE: ES_46_RV6.md:29
-- FORMULA: \boxed{ U=3S+T. }
def Node_D_U (ctx : FormalContext) : Prop := (ctx.U = (((3 : ℝ) * ctx.S) + ctx.T))
-- DEMUESTRA_ASSERTION: D_U|COMPLETA|NO_APLICA

-- FORMAL_NODE: D_t_prime
-- SOURCE: ES_46_RV6.md:65
-- FORMULA: \frac{dt'}{dt}.
-- FORMULA: t'
-- FORMULA: t'
-- FORMULA: dt'
def Node_D_t_prime (ctx : FormalContext) : Prop := True
-- DEMUESTRA_ASSERTION: D_t_prime|INCOMPLETA|NO_INICIADA

-- FORMAL_NODE: A_L
-- SOURCE: ES_46_RV6.md:77
-- FORMULA: dt' = dt \sqrt{ 1-\frac{v^2}{c^2} }.
-- FORMULA: \boxed{ v=\frac{ds}{dt}. }
-- FORMULA: c=1.
-- FORMULA: dt'^2 = dt^2-ds^2,
-- FORMULA: v
def Node_A_L (ctx : FormalContext) : Prop := (ctx.v = (ctx.ds / ctx.dt))
-- DEMUESTRA_ASSERTION: A_L|COMPLETA|PENDIENTE

-- FORMAL_NODE: D_lambda
-- SOURCE: ES_46_RV6.md:174
-- FORMULA: E=\frac{hc}{\lambda},
-- FORMULA: E=Mc^2,
-- FORMULA: Mc^2=\frac{hc}{\lambda},
-- FORMULA: \boxed{ \lambda=\frac{h}{Mc}. }
-- FORMULA: \lambda
def Node_D_lambda (ctx : FormalContext) : Prop := (ctx.lambda = (ctx.h / ctx.Mc))
-- DEMUESTRA_ASSERTION: D_lambda|COMPLETA|NO_APLICA

-- FORMAL_NODE: D_L
-- SOURCE: ES_46_RV6.md:202
-- FORMULA: \boxed{ L=n\lambda. }
-- FORMULA: n\in\mathbb R^+.
-- FORMULA: L
def Node_D_L (ctx : FormalContext) : Prop := (ctx.L = (ctx.n * ctx.lambda))
-- DEMUESTRA_ASSERTION: D_L|COMPLETA|NO_APLICA

-- FORMAL_NODE: D_k
-- SOURCE: ES_46_RV6.md:314
-- FORMULA: k\in\mathbb N^+
def Node_D_k (ctx : FormalContext) : Prop := (ctx.k ∈ {n : ℕ | 0 < n})
-- DEMUESTRA_ASSERTION: D_k|COMPLETA|NO_APLICA

-- FORMAL_NODE: D_rho
-- SOURCE: ES_46_RV6.md:316
-- FORMULA: \boxed{ \rho = \operatorname{dist}(n,\mathbb N^+). }
-- FORMULA: \boxed{ 0\le\rho\le\frac12. }
-- FORMULA: \boxed{ n=k\pm\rho, \qquad k\in\mathbb N^+, \qquad 0\le\rho\le\frac12. }
-- FORMULA: \boxed{ L(k,\rho) = (k\pm\rho)\lambda, }
-- FORMULA: \boxed{ R_{\rm VED}(k,\rho) = \frac{(k\pm\rho)\lambda}{2\pi}. }
-- FORMULA: \rho=1/2
-- DEMUESTRA_SOURCE_CLAIM: {"node": "D_rho", "formula": 2, "location": "ES_46_RV6.md:316:D_rho:formula-2", "source": "\\boxed{ 0\\le\\rho\\le\\frac12. }", "status": "FORMALIZED_UNPROVEN"}
def Node_D_rho_source_2 (ctx : FormalContext) : Prop := ((0 ≤ ctx.rho) ∧ (ctx.rho ≤ ((1 : ℝ) / (2 : ℝ))))
def Node_D_rho_clause_1 (ctx : FormalContext) : Prop := (ctx.rho = (ctx.dist_fn_2 ctx.n {n : ℕ | 0 < n}))
def Node_D_rho_clause_2 (ctx : FormalContext) : Prop := (((ctx.L_fn_2 ctx.k ctx.rho) = ((((ctx.k : ℝ) + ctx.rho) * ctx.lambda)) ∨ (ctx.L_fn_2 ctx.k ctx.rho) = ((((ctx.k : ℝ) - ctx.rho) * ctx.lambda))))
def Node_D_rho_clause_3 (ctx : FormalContext) : Prop := (((ctx.R_VED_fn_2 ctx.k ctx.rho) = (((((ctx.k : ℝ) + ctx.rho) * ctx.lambda) / ((2 : ℝ) * Real.pi))) ∨ (ctx.R_VED_fn_2 ctx.k ctx.rho) = (((((ctx.k : ℝ) - ctx.rho) * ctx.lambda) / ((2 : ℝ) * Real.pi)))))
def Node_D_rho (ctx : FormalContext) : Prop := True
-- DEMUESTRA_ASSERTION: D_rho|INCOMPLETA|NO_INICIADA

-- FORMAL_NODE: D_Rim
-- SOURCE: ES_46_RV6.md:912
-- FORMULA: z=a\pm ib
-- FORMULA: \zeta(s) = \sum_{n=1}^{\infty}\frac1{n^s}
-- FORMULA: \boxed{s=1.}
-- FORMULA: \boxed{ Z_{\rm Rim}^{\rm triv} = \{-2,-4,-6,\ldots\} = \{-2m:m\in\mathbb N^+\}. }
-- FORMULA: \boxed{ Z_{\rm Rim}^{\rm nt} = \{ z\in\mathbb C: \zeta(z)=0, \; 0<\Re(z)<1 \}. }
-- FORMULA: \boxed{ z=a\pm ib, \qquad 0<a<1. }
-- FORMULA: a \longleftrightarrow 1-a.
-- FORMULA: \boxed{ a=\frac12. }
-- FORMULA: \Re(s)>1
-- DEMUESTRA_SOURCE_CLAIM: {"node": "D_Rim", "formula": 4, "location": "ES_46_RV6.md:912:D_Rim:formula-4", "source": "\\boxed{ Z_{\\rm Rim}^{\\rm triv} = \\{-2,-4,-6,\\ldots\\} = \\{-2m:m\\in\\mathbb N^+\\}. }", "status": "UNTRANSLATED"}
def Node_D_Rim_clause_1 (ctx : FormalContext) : Prop := (ctx.s = 1)
def Node_D_Rim_clause_2 (ctx : FormalContext) : Prop := (ctx.Z_Rim_nt = ({z | ((z ∈ (Set.univ : Set ℂ)) ∧ ((ctx.zeta z) = 0)) ∧ ((0 < (Complex.re z)) ∧ ((Complex.re z) < 1))}))
def Node_D_Rim_clause_3 (ctx : FormalContext) : Prop := (ctx.a = ((1 : ℝ) / (2 : ℝ)))
def Node_D_Rim (ctx : FormalContext) : Prop := True
-- DEMUESTRA_ASSERTION: D_Rim|INCOMPLETA|NO_INICIADA

-- FORMAL_NODE: D_rho_R
-- SOURCE: ES_46_RV6.md:1003
-- FORMULA: \qquad \rho_R = \left| a-\frac12 \right|. }
-- FORMULA: 0<a<1,
-- FORMULA: \boxed{ 0\le\rho_R<\frac12, }
-- FORMULA: \boxed{ a = \frac12+\varepsilon\rho_R. }
-- FORMULA: \boxed{ z_{\varepsilon,\pm} = \frac12 + \varepsilon\rho_R \pm ib. }
-- FORMULA: \boxed{ \rho_R = \left| \Re(z)-\frac12 \right|. }
-- FORMULA: \rho_R=1/2
-- FORMULA: \varepsilon=\pm1
-- DEMUESTRA_SOURCE_CLAIM: {"node": "D_rho_R", "formula": 3, "location": "ES_46_RV6.md:1003:D_rho_R:formula-3", "source": "\\boxed{ 0\\le\\rho_R<\\frac12, }", "status": "FORMALIZED_UNPROVEN"}
def Node_D_rho_R_source_3 (ctx : FormalContext) : Prop := ((0 ≤ ctx.rho_R) ∧ (ctx.rho_R < ((1 : ℝ) / (2 : ℝ))))
-- DEMUESTRA_SOURCE_CLAIM: {"node": "D_rho_R", "formula": 4, "location": "ES_46_RV6.md:1003:D_rho_R:formula-4", "source": "\\boxed{ a = \\frac12+\\varepsilon\\rho_R. }", "status": "FORMALIZED_UNPROVEN"}
def Node_D_rho_R_source_4 (ctx : FormalContext) : Prop := (ctx.a = (((1 : ℝ) / (2 : ℝ)) + (ctx.varepsilon * ctx.rho_R)))
-- DEMUESTRA_SOURCE_CLAIM: {"node": "D_rho_R", "formula": 5, "location": "ES_46_RV6.md:1003:D_rho_R:formula-5", "source": "\\boxed{ z_{\\varepsilon,\\pm} = \\frac12 + \\varepsilon\\rho_R \\pm ib. }", "status": "FORMALIZED_UNPROVEN"}
def Node_D_rho_R_source_5 (ctx : FormalContext) : Prop := (((ctx.z_varepsilon_PM) = (((((1 : ℝ) / (2 : ℝ)) + (ctx.varepsilon * ctx.rho_R)) + ctx.ib)) ∨ (ctx.z_varepsilon_PM) = (((((1 : ℝ) / (2 : ℝ)) + (ctx.varepsilon * ctx.rho_R)) - ctx.ib))))
-- DEMUESTRA_SOURCE_CLAIM: {"node": "D_rho_R", "formula": 6, "location": "ES_46_RV6.md:1003:D_rho_R:formula-6", "source": "\\boxed{ \\rho_R = \\left| \\Re(z)-\\frac12 \\right|. }", "status": "FORMALIZED_UNPROVEN"}
def Node_D_rho_R_source_6 (ctx : FormalContext) : Prop := (ctx.rho_R = (abs ((Complex.re ctx.z) - ((1 : ℝ) / (2 : ℝ)))))
def Node_D_rho_R (ctx : FormalContext) : Prop := (ctx.rho_R = (abs (ctx.a - ((1 : ℝ) / (2 : ℝ)))))
-- DEMUESTRA_ASSERTION: D_rho_R|INCOMPLETA|NO_INICIADA

-- FORMAL_NODE: D_f
-- SOURCE: ES_46_RV6.md:1072
-- FORMULA: U_{\rm VED}^{\rho} = \left\{x:\rho_{\rm VED}(x)\in[0,\tfrac12]\right\}
-- FORMULA: U_{\rm Rim}^{\rho} = \left\{z:\rho_R(z)\in[0,\tfrac12]\right\}.
-- FORMULA: \boxed{ f:U_{\rm VED}^{\rho}\longrightarrow U_{\rm Rim}^{\rho} }
-- FORMULA: \rho
-- FORMULA: a=\Re(z)
-- FORMULA: a=1/2
def Node_D_f (ctx : FormalContext) : Prop := ((∀ x_map : ℝ, x_map ∈ ctx.U_VED_rho → (ctx.f_fn_1 x_map) ∈ ctx.U_Rim_rho))
-- DEMUESTRA_ASSERTION: D_f|INCOMPLETA|NO_INICIADA

-- FORMAL_NODE: D_fInv
-- SOURCE: ES_46_RV6.md:1100
-- FORMULA: \boxed{ f^{-1}:U_{\rm Rim}^{\rho}\longrightarrow U_{\rm VED}^{\rho}. }
-- FORMULA: \boxed{ f^{-1}(f(x))=x, \qquad f(f^{-1}(z))=z. }
-- DEMUESTRA_SOURCE_CLAIM: {"node": "D_fInv", "formula": 1, "location": "ES_46_RV6.md:1100:D_fInv:formula-1", "source": "\\boxed{ f^{-1}:U_{\\rm Rim}^{\\rho}\\longrightarrow U_{\\rm VED}^{\\rho}. }", "status": "FORMALIZED_UNPROVEN"}
def Node_D_fInv_source_1 (ctx : FormalContext) : Prop := ((∀ x_map : ℂ, x_map ∈ ctx.U_Rim_rho → (ctx.f_inv_fn_1 x_map) ∈ ctx.U_VED_rho))
def Node_D_fInv (ctx : FormalContext) : Prop := (((ctx.f_inv_fn_1 (ctx.f_fn_1 ctx.x)) = ctx.x) ∧ ((ctx.f_fn_1 (ctx.f_inv_fn_1 ctx.z)) = ctx.z))
-- DEMUESTRA_ASSERTION: D_fInv|INCOMPLETA|NO_INICIADA

-- FORMAL_NODE: P_COORD
-- SOURCE: ES_46_RV6.md:57
-- FORMULA: 3S
def Node_P_COORD (ctx : FormalContext) : Prop := True
-- DEMUESTRA_ASSERTION: P_COORD|INCOMPLETA|NO_INICIADA

-- FORMAL_NODE: T_ISO
-- SOURCE: ES_46_RV6.md:1118
-- FORMULA: \boxed{ U_{\rm VED}^{\rho}\cong U_{\rm Rim}^{\rho}. }
-- FORMULA: f
-- FORMULA: f^{-1}
-- FORMULA: \rho=0
-- FORMULA: 0<\rho\le1/2
def Node_T_ISO (ctx : FormalContext) : Prop := ((∃ h : ↥(ctx.U_VED_rho) ≃ₜ ↥(ctx.U_Rim_rho), (∀ x_iso : ↥(ctx.U_VED_rho), (h x_iso).val = ctx.f_fn_1 x_iso.val) ∧ (∀ z_iso : ↥(ctx.U_Rim_rho), (h.symm z_iso).val = ctx.f_inv_fn_1 z_iso.val)))
-- DEMUESTRA_ASSERTION: T_ISO|COMPLETA|PENDIENTE

-- FORMAL_NODE: P_ST
-- SOURCE: ES_46_RV6.md:114
-- FORMULA: \qquad ds^2=dt^2-dt'^2. }
-- FORMULA: \boxed{ ds^2=(dt-dt')(dt+dt'). }
def Node_P_ST (ctx : FormalContext) : Prop := (ctx.ds ^ 2 = ((ctx.dt - ctx.dt_prime) * (ctx.dt + ctx.dt_prime)))
-- DEMUESTRA_ASSERTION: P_ST|COMPLETA|PENDIENTE

-- FORMAL_NODE: P_RHO_ISO
-- SOURCE: ES_46_RV6.md:1133
-- FORMULA: \boxed{ \rho_R(f(x))=\rho_{\rm VED}(x), \qquad \rho_{\rm VED}(f^{-1}(z))=\rho_R(z). }
-- FORMULA: \rho=0 \iff \text{clase estable},
-- FORMULA: 0<\rho\le\frac12 \iff \text{clase no estable}
-- FORMULA: \rho
-- FORMULA: f
-- FORMULA: f^{-1}
def Node_P_RHO_ISO (ctx : FormalContext) : Prop := (((ctx.rho_R_fn_1 (ctx.f_fn_1 ctx.x)) = (ctx.rho_VED_fn_1 ctx.x)) ∧ ((ctx.rho_VED_fn_1 (ctx.f_inv_fn_1 ctx.z)) = (ctx.rho_R_fn_1 ctx.z)))
-- DEMUESTRA_ASSERTION: P_RHO_ISO|COMPLETA|PENDIENTE

-- FORMAL_NODE: P_v
-- SOURCE: ES_46_RV6.md:138
-- FORMULA: \qquad \frac{ds}{dt}=v. }
-- FORMULA: \frac{d^2s}{dt^2}=0.
-- FORMULA: v
def Node_P_v_clause_1 (ctx : FormalContext) : Prop := ((ctx.ds / ctx.dt) = ctx.v)
def Node_P_v_clause_2 (ctx : FormalContext) : Prop := ((((ctx.d ^ 2 : ℂ) * ctx.s) / (ctx.dt ^ 2 : ℂ)) = 0)
def Node_P_v (ctx : FormalContext) : Prop := True
-- DEMUESTRA_ASSERTION: P_v|AMBIGUA|NO_INICIADA

-- FORMAL_NODE: P_RIM_S
-- SOURCE: ES_46_RV6.md:1169
-- FORMULA: \boxed{ \forall z\in U_{\rm Rim}, \qquad \operatorname{Stable}_{\rm Rim}(z) \iff \rho_R(z)=0. }
-- FORMULA: \boxed{ z\in Z_{\rm Rim}^{\rm nt} \Longrightarrow \operatorname{Stable}_{\rm Rim}(z) \Longrightarrow \rho_R(z)=0. }
-- FORMULA: \rho
-- FORMULA: f
-- FORMULA: f^{-1}
-- FORMULA: U_{\rm Rim}
-- FORMULA: \rho_R(z)\neq0
-- FORMULA: Z_{\rm Rim}^{\rm nt}
-- DEMUESTRA_SOURCE_CLAIM: {"node": "P_RIM_S", "formula": 2, "location": "ES_46_RV6.md:1169:P_RIM_S:formula-2", "source": "\\boxed{ z\\in Z_{\\rm Rim}^{\\rm nt} \\Longrightarrow \\operatorname{Stable}_{\\rm Rim}(z) \\Longrightarrow \\rho_R(z)=0. }", "status": "FORMALIZED_UNPROVEN"}
def Node_P_RIM_S_source_2 (ctx : FormalContext) : Prop := ((ctx.z ∈ ctx.Z_Rim_nt) → ((ctx.Stable_Rim_fn_1 ctx.z) → ((ctx.rho_R_fn_1 ctx.z) = 0)))
def Node_P_RIM_S (ctx : FormalContext) : Prop := (∀ z : ℂ, (z ∈ ctx.U_Rim) → ((ctx.Stable_Rim_fn_1 z) ↔ ((ctx.rho_R_fn_1 z) = 0)))
-- DEMUESTRA_ASSERTION: P_RIM_S|INCOMPLETA|NO_INICIADA

-- FORMAL_NODE: P_a
-- SOURCE: ES_46_RV6.md:154
-- FORMULA: \qquad \frac{d^2s}{dt^2} = \frac{dv}{dt} = a. }
-- FORMULA: t
-- FORMULA: t'
def Node_P_a (ctx : FormalContext) : Prop := (((((ctx.d ^ 2 : ℂ) * ctx.s) / (ctx.dt ^ 2 : ℂ)) = (ctx.dv / ctx.dt)) ∧ ((ctx.dv / ctx.dt) = ctx.a))
-- DEMUESTRA_ASSERTION: P_a|COMPLETA|PENDIENTE

-- FORMAL_NODE: P_VED_Inv
-- SOURCE: ES_46_RV6.md:254
-- FORMULA: L
-- FORMULA: \lambda
-- FORMULA: n
-- FORMULA: \rho
def Node_P_VED_Inv (ctx : FormalContext) : Prop := True
-- DEMUESTRA_ASSERTION: P_VED_Inv|INCOMPLETA|NO_INICIADA

-- FORMAL_NODE: P_VED_E
-- SOURCE: ES_46_RV6.md:394
-- FORMULA: \qquad \rho=0 \iff n=k\in\mathbb N^+ \iff L=k\lambda \iff \text{cierre exacto en fase} \iff \text{estado estable}. }
-- FORMULA: 0<\rho\le\frac12,
def Node_P_VED_E (ctx : FormalContext) : Prop := (((((ctx.rho = 0) ↔ ((ctx.n = ctx.k) ∧ (ctx.k ∈ {n : ℕ | 0 < n}))) ↔ (ctx.L = ((ctx.k : ℝ) * ctx.lambda))) ↔ ctx.Text_cierre_exacto_en_fase) ↔ ctx.Text_estado_estable)
-- DEMUESTRA_ASSERTION: P_VED_E|COMPLETA|PENDIENTE

-- FORMAL_NODE: P_VED_I
-- SOURCE: ES_46_RV6.md:418
-- FORMULA: \qquad 0<\rho\le\frac12 \iff \text{cierre no estable}. }
-- FORMULA: \boxed{ \rho=\frac12 }
-- DEMUESTRA_SOURCE_CLAIM: {"node": "P_VED_I", "formula": 2, "location": "ES_46_RV6.md:418:P_VED_I:formula-2", "source": "\\boxed{ \\rho=\\frac12 }", "status": "FORMALIZED_UNPROVEN"}
def Node_P_VED_I_source_2 (ctx : FormalContext) : Prop := (ctx.rho = ((1 : ℝ) / (2 : ℝ)))
def Node_P_VED_I (ctx : FormalContext) : Prop := (((0 < ctx.rho) ∧ (ctx.rho ≤ ((1 : ℝ) / (2 : ℝ)))) ↔ ctx.Text_cierre_no_estable)
-- DEMUESTRA_ASSERTION: P_VED_I|INCOMPLETA|NO_INICIADA

-- FORMAL_NODE: P_VR_rho
-- SOURCE: ES_46_RV6.md:1272
-- FORMULA: \qquad \rho_{\rm VED} = \rho_R = \left| a-\frac12 \right|. }
-- FORMULA: U_{\rm VED}
def Node_P_VR_rho (ctx : FormalContext) : Prop := ((ctx.rho_VED = ctx.rho_R) ∧ (ctx.rho_R = (abs (ctx.a - ((1 : ℝ) / (2 : ℝ))))))
-- DEMUESTRA_ASSERTION: P_VR_rho|COMPLETA|PENDIENTE

-- FORMAL_NODE: P_VED_K_E
-- SOURCE: ES_46_RV6.md:462
-- FORMULA: \boxed{ \mathcal E_{\rm VED} = \{(k,0):k\in\mathbb N^+\}. }
-- FORMULA: k=1,2,3,\ldots
-- FORMULA: \rho=0
def Node_P_VED_K_E (ctx : FormalContext) : Prop := (ctx.mathcal_E_VED = ({x | ∃ k : ℕ, (k ∈ {n : ℕ | 0 < n}) ∧ (x = ((k, 0)))}))
-- DEMUESTRA_ASSERTION: P_VED_K_E|COMPLETA|PENDIENTE

-- FORMAL_NODE: P_VR_E
-- SOURCE: ES_46_RV6.md:1312
-- FORMULA: \qquad \text{estado estable} \iff \left| a-\frac12 \right| = 0. }
-- FORMULA: \boxed{ \text{estado estable} \iff a=\frac12. }
-- FORMULA: U_{\rm VED}
-- DEMUESTRA_SOURCE_CLAIM: {"node": "P_VR_E", "formula": 2, "location": "ES_46_RV6.md:1312:P_VR_E:formula-2", "source": "\\boxed{ \\text{estado estable} \\iff a=\\frac12. }", "status": "FORMALIZED_UNPROVEN"}
def Node_P_VR_E_source_2 (ctx : FormalContext) : Prop := (ctx.Text_estado_estable ↔ (ctx.a = ((1 : ℝ) / (2 : ℝ))))
def Node_P_VR_E (ctx : FormalContext) : Prop := (ctx.Text_estado_estable ↔ ((abs (ctx.a - ((1 : ℝ) / (2 : ℝ)))) = 0))
-- DEMUESTRA_ASSERTION: P_VR_E|INCOMPLETA|NO_INICIADA

-- FORMAL_NODE: P_VED_K_I
-- SOURCE: ES_46_RV6.md:480
-- FORMULA: \rho=1/2
-- FORMULA: k
def Node_P_VED_K_I (ctx : FormalContext) : Prop := (ctx.rho = ((1 : ℝ) / (2 : ℝ)))
-- DEMUESTRA_ASSERTION: P_VED_K_I|COMPLETA|PENDIENTE

-- FORMAL_NODE: P_Z
-- SOURCE: ES_46_RV6.md:1454
-- FORMULA: \qquad z\in Z_{\rm Rim}^{\rm nt} \Rightarrow \left[ \zeta(z)=0 \ \text{en }U_{\rm Rim} \ \text{y } \rho_R=\rho_{\rm VED} \ \text{clasifica su localización transversal} \right]. }
def Node_P_Z (ctx : FormalContext) : Prop := ((ctx.z ∈ ctx.Z_Rim_nt) → ctx.Text_clasifica_su_localizaci_n_transversal)
-- DEMUESTRA_ASSERTION: P_Z|COMPLETA|PENDIENTE

-- FORMAL_NODE: P_VED_R_C
-- SOURCE: ES_46_RV6.md:482
-- FORMULA: 0\le\rho\le\frac12
-- FORMULA: k
def Node_P_VED_R_C (ctx : FormalContext) : Prop := ((0 ≤ ctx.rho) ∧ (ctx.rho ≤ ((1 : ℝ) / (2 : ℝ))))
-- DEMUESTRA_ASSERTION: P_VED_R_C|COMPLETA|PENDIENTE

-- FORMAL_NODE: T_RIEMANN
-- SOURCE: ES_46_RV6.md:1472
-- FORMULA: z=a\pm ib
-- FORMULA: \boxed{ a=\frac12. }
-- FORMULA: \boxed{ \zeta(z)=0. }
-- FORMULA: \boxed{ \rho_R = \left| a-\frac12 \right| = \rho_{\rm VED}. }
-- FORMULA: \rho_{\rm VED}=0 \iff \text{estado estable},
-- FORMULA: 0<\rho_{\rm VED}\le\frac12 \iff \text{estado no estable}.
-- FORMULA: \boxed{ a\neq\frac12. }
-- FORMULA: \left| a-\frac12 \right| >0.
-- FORMULA: \rho = \left| a-\frac12 \right| >0.
-- FORMULA: \rho>0 \Rightarrow \text{estado no estable}.
-- FORMULA: \boxed{ \rho=0. }
-- FORMULA: a\neq\frac12
-- FORMULA: \boxed{ a=\frac12. }
-- FORMULA: \boxed{ \forall z\in Z_{\rm Rim}^{\rm nt}, \qquad \Re(z)=\frac12. }
-- FORMULA: \boxed{ Z_{\rm Rim}^{\rm nt} \subseteq \left\{ s\in\mathbb C: \Re(s)=\frac12 \right\}. }
-- FORMULA: Z_{\rm Rim}^{\rm nt}
-- FORMULA: Z_{\rm Rim}^{\rm nt}
-- FORMULA: U_{\rm Rim}
-- FORMULA: D_{\rho_R}
-- FORMULA: P_{\rm VR}(\rho)
-- FORMULA: U_{\rm VED}
-- FORMULA: P_{\rm VR}(\rho)
-- FORMULA: U_{\rm VED}
-- FORMULA: \zeta(z)=0
-- FORMULA: U_{\rm Rim}
-- FORMULA: U_{\rm VED}
-- FORMULA: U_{\rm VED}
-- FORMULA: a\neq1/2
-- FORMULA: U_{\rm Rim}
-- FORMULA: U_{\rm VED}
-- FORMULA: \zeta(z)=0
-- FORMULA: z
-- FORMULA: Z_{\rm Rim}^{\rm nt}
-- DEMUESTRA_SOURCE_CLAIM: {"node": "T_RIEMANN", "formula": 2, "location": "ES_46_RV6.md:1472:T_RIEMANN:formula-2", "source": "\\boxed{ a=\\frac12. }", "status": "FORMALIZED_UNPROVEN"}
def Node_T_RIEMANN_source_2 (ctx : FormalContext) : Prop := (ctx.a = ((1 : ℝ) / (2 : ℝ)))
def Node_T_RIEMANN (ctx : FormalContext) : Prop := (∀ z : ℂ, (z ∈ ctx.Z_Rim_nt) → ((Complex.re z) = ((1 : ℝ) / (2 : ℝ))))
-- DEMUESTRA_ASSERTION: T_RIEMANN|INCOMPLETA|NO_INICIADA

-- FORMAL_NODE: P_VED_Completo
-- SOURCE: ES_46_RV6.md:494
-- FORMULA: \quad U_{\rm VED}^{\rm cerrado} = \mathcal E_{\rm VED} \sqcup \mathcal I_{\rm VED}, }
-- FORMULA: n\to\infty
-- DEMUESTRA_SOURCE_CLAIM: {"node": "P_VED_Completo", "formula": 2, "location": "ES_46_RV6.md:494:P_VED_Completo:formula-2", "source": "n\\to\\infty", "status": "UNTRANSLATED"}
def Node_P_VED_Completo (ctx : FormalContext) : Prop := True
-- DEMUESTRA_ASSERTION: P_VED_Completo|INCOMPLETA|NO_INICIADA

-- FORMAL_NODE: P_VS
-- SOURCE: ES_46_RV6.md:557
-- FORMULA: \qquad U_{\rm VED}\cong U_{\rm Sch}. }
-- FORMULA: \boxed{ G(2)=G, }
-- FORMULA: \boxed{ \lim_{n\to\infty}G(n)=0. }
-- FORMULA: n
-- FORMULA: n=2
-- FORMULA: U_{\rm Sch}
-- DEMUESTRA_SOURCE_CLAIM: {"node": "P_VS", "formula": 3, "location": "ES_46_RV6.md:557:P_VS:formula-3", "source": "\\boxed{ \\lim_{n\\to\\infty}G(n)=0. }", "status": "UNTRANSLATED"}
def Node_P_VS (ctx : FormalContext) : Prop := ((ctx.G_fn_1 2) = ctx.G)
-- DEMUESTRA_ASSERTION: P_VS|INCOMPLETA|NO_INICIADA

-- FORMAL_NODE: P_F
-- SOURCE: ES_46_RV6.md:601
-- FORMULA: \qquad F = (dt^2-dt'^2) + \frac{d}{dt}(dt^2-dt'^2). }
-- FORMULA: dt'
-- FORMULA: t
def Node_P_F (ctx : FormalContext) : Prop := (ctx.F = ((ctx.dt ^ 2 - ctx.dt_prime ^ 2) + ((ctx.d / ctx.dt) * (ctx.dt ^ 2 - ctx.dt_prime ^ 2))))
-- DEMUESTRA_ASSERTION: P_F|COMPLETA|PENDIENTE

-- FORMAL_NODE: P_F1
-- SOURCE: ES_46_RV6.md:617
-- FORMULA: \qquad F = dt^2-dt'^2 + 2dt - 2dt'\frac{dt'}{dt}. }
-- FORMULA: dt'
-- FORMULA: dt'/dt
def Node_P_F1 (ctx : FormalContext) : Prop := (ctx.F = (((ctx.dt ^ 2 - ctx.dt_prime ^ 2) + ((2 : ℝ) * ctx.dt)) - (((2 : ℝ) * ctx.dt_prime) * (ctx.dt_prime / ctx.dt))))
-- DEMUESTRA_ASSERTION: P_F1|COMPLETA|PENDIENTE

-- FORMAL_NODE: P_W
-- SOURCE: ES_46_RV6.md:639
-- FORMULA: \qquad v_{\rm onda}=c. }
-- FORMULA: c=1.
-- FORMULA: v=\frac{ds}{dt},
-- FORMULA: \frac{ds}{dt}=1.
-- FORMULA: ds=dt,
-- FORMULA: dt' = dt \sqrt{ 1-\frac{v^2}{c^2} }.
-- FORMULA: v\to c,
-- FORMULA: \boxed{ dt'\to0. }
-- FORMULA: dt'^2\to0,
-- FORMULA: \frac{dt'}{dt}\to0.
-- DEMUESTRA_SOURCE_CLAIM: {"node": "P_W", "formula": 8, "location": "ES_46_RV6.md:639:P_W:formula-8", "source": "\\boxed{ dt'\\to0. }", "status": "UNTRANSLATED"}
def Node_P_W (ctx : FormalContext) : Prop := True
-- DEMUESTRA_ASSERTION: P_W|INCOMPLETA|NO_INICIADA

-- FORMAL_NODE: P_F2
-- SOURCE: ES_46_RV6.md:712
-- FORMULA: \qquad F=dt^2+2dt. }
-- FORMULA: dt^2+2dt = 2dt \left( 1+\frac12dt \right),
def Node_P_F2_clause_1 (ctx : FormalContext) : Prop := (ctx.F = (ctx.dt ^ 2 + ((2 : ℝ) * ctx.dt)))
def Node_P_F2_clause_2 (ctx : FormalContext) : Prop := ((ctx.dt ^ 2 + ((2 : ℝ) * ctx.dt)) = ((2 : ℝ) * (ctx.dt_fn_1 ((1 : ℝ) + (((1 : ℝ) / (2 : ℝ)) * ctx.dt)))))
def Node_P_F2 (ctx : FormalContext) : Prop := True
-- DEMUESTRA_ASSERTION: P_F2|AMBIGUA|NO_INICIADA

-- FORMAL_NODE: P_F3
-- SOURCE: ES_46_RV6.md:733
-- FORMULA: \qquad F = 2dt \left( 1+\frac12dt \right). }
-- FORMULA: \boxed{ \frac12 }
-- FORMULA: F
def Node_P_F3 (ctx : FormalContext) : Prop := (ctx.F = ((2 : ℝ) * (ctx.dt_fn_1 ((1 : ℝ) + (((1 : ℝ) / (2 : ℝ)) * ctx.dt)))))
-- DEMUESTRA_ASSERTION: P_F3|COMPLETA|PENDIENTE

-- FORMAL_NODE: D_Lap
-- SOURCE: ES_46_RV6.md:764
-- FORMULA: \boxed{ s_\pm = a\pm ib. }
-- FORMULA: \boxed{ a=\frac12 }
-- FORMULA: T(k,\rho) = (k\pm\rho)\lambda
-- FORMULA: e^{\pm ibT}=1.
-- FORMULA: bT=2\pi.
-- FORMULA: \boxed{ b(k,\rho) = \frac{2\pi} {(k\pm\rho)\lambda}. }
-- FORMULA: \rho=0,
-- FORMULA: \boxed{ b_k = \frac{2\pi}{k\lambda}. }
-- FORMULA: \boxed{ Z_{\rm VED\to Lap} = \left\{ \frac12 \pm i\frac{2\pi}{k\lambda} : k\in\mathbb N^+ \right\}. }
-- FORMULA: P_{F3}
-- FORMULA: c=1
-- DEMUESTRA_SOURCE_CLAIM: {"node": "D_Lap", "formula": 9, "location": "ES_46_RV6.md:764:D_Lap:formula-9", "source": "\\boxed{ Z_{\\rm VED\\to Lap} = \\left\\{ \\frac12 \\pm i\\frac{2\\pi}{k\\lambda} : k\\in\\mathbb N^+ \\right\\}. }", "status": "UNTRANSLATED"}
def Node_D_Lap_clause_1 (ctx : FormalContext) : Prop := (((ctx.s_PM) = ((ctx.a + ctx.ib)) ∨ (ctx.s_PM) = ((ctx.a - ctx.ib))))
def Node_D_Lap_clause_2 (ctx : FormalContext) : Prop := (ctx.a = ((1 : ℝ) / (2 : ℝ)))
def Node_D_Lap_clause_3 (ctx : FormalContext) : Prop := (((ctx.b_fn_2 ctx.k ctx.rho) = ((((2 : ℝ) * Real.pi) / (((ctx.k : ℝ) + ctx.rho) * ctx.lambda))) ∨ (ctx.b_fn_2 ctx.k ctx.rho) = ((((2 : ℝ) * Real.pi) / (((ctx.k : ℝ) - ctx.rho) * ctx.lambda)))))
def Node_D_Lap_clause_4 (ctx : FormalContext) : Prop := (ctx.b_k = (((2 : ℝ) * Real.pi) / ((ctx.k : ℝ) * ctx.lambda)))
def Node_D_Lap (ctx : FormalContext) : Prop := True
-- DEMUESTRA_ASSERTION: D_Lap|INCOMPLETA|NO_INICIADA

-- FORMAL_NODE: P_Lap_Z
-- SOURCE: ES_46_RV6.md:851
-- FORMULA: \Re(s)=\frac12.
-- FORMULA: U_{\rm VED}
-- FORMULA: k
-- FORMULA: k
def Node_P_Lap_Z (ctx : FormalContext) : Prop := ((Complex.re ctx.s) = ((1 : ℝ) / (2 : ℝ)))
-- DEMUESTRA_ASSERTION: P_Lap_Z|COMPLETA|PENDIENTE

end ES_46_RV6

-- DEMUESTRA_AUDIT_BEGIN
-- DEMUESTRA_CONSTRUCTION_COMPLETE: FALSE
-- DEMUESTRA_PROOF_COMPLETE: FALSE
-- DEMUESTRA_FORMALIZATION_STATUS: PARTIAL
-- DEMUESTRA_RESULT_PENDING: ES_46_RV6.Node_T_RIEMANN
-- DEMUESTRA_JSON_NODE: T_RIEMANN
#check ES_46_RV6.Node_T_RIEMANN
-- DEMUESTRA_AUDIT_END