regge_equations_statement

formal source

 180
 181    So the Regge equations simplify to:
 182    sum_h (dA_h/dL_e) * delta_h = 0 -/
 183def regge_equations_statement : Prop :=
 184  ∀ (hinges : List HingeData),
 185    ∃ (dA_dL : List ℝ),
 186      dA_dL.length = hinges.length ∧
 187      (List.zipWith (· * ·) dA_dL (hinges.map deficit_angle)).sum = 0
 188
 189/-- The Schläfli identity: the sum of A_h * d(delta_h)/dL_e vanishes
 190    identically. This is a geometric identity, not a dynamical equation. -/
 191def schlafli_identity : Prop :=
 192  ∀ (hinges : List HingeData),
 193    ∀ (d_delta_dL : List ℝ),
 194      (List.zipWith (· * ·) (hinges.map HingeData.area) d_delta_dL).sum = 0
 195
 196/-! ## Connection to RS -/
 197
 198/-- In the RS framework, the edge lengths are determined by the J-cost
 199    defect field. For a lattice with spacing a and defect density rho:
 200    L_e = a * (1 + kappa_RS * rho(x))^(1/D) approximately.
 201
 202    The exact relationship is:
 203    L_e^2 = a^2 * g_{mu nu}(x) * dx^mu * dx^nu
 204
 205    where g = eta + h is the full metric and h is determined by J-cost. -/
 206noncomputable def rs_edge_length (a : ℝ) (g_component : ℝ) : ℝ :=
 207  a * Real.sqrt g_component
 208
 209theorem rs_edge_length_pos (a : ℝ) (g : ℝ) (ha : 0 < a) (hg : 0 < g) :
 210    0 < rs_edge_length a g :=
 211  mul_pos ha (Real.sqrt_pos.mpr hg)
 212
 213/-- The RS Regge action inherits kappa = 8*phi^5 from the defect-to-metric