 135and vol_i is the simplex volume. -/
 136
 137/-- The Regge action density at a hinge. -/
 138structure HingeContribution where
 139  deficit_angle : ℝ
 140  area : ℝ
 141  area_pos : 0 < area
 142
 143/-- Regge action as sum over hinges. -/
 144def regge_action_from_hinges (hinges : List HingeContribution) : ℝ :=
 145  hinges.foldl (fun acc h => acc + h.deficit_angle * h.area) 0
 146
 147/-- The J-cost normalization factor relating J-cost action to Regge action.
 148    Since J''(1) = 1 (the calibration axiom A3), and the Regge action
 149    has normalization 1/(8πG) = 1/κ, the factor is exactly κ = 8φ⁵. -/
 150def jcost_to_regge_factor : ℝ := 8 * phi ^ 5
 151
 152/-- κ = 8φ⁵ is the unique normalization matching J-cost to Regge. -/
 153theorem jcost_to_regge_factor_eq : jcost_to_regge_factor = 8 * phi ^ 5 := rfl
 154
 155/-- The normalization factor is positive. -/
 156theorem jcost_to_regge_factor_pos : 0 < jcost_to_regge_factor := by
 157  unfold jcost_to_regge_factor
 158  exact mul_pos (by norm_num : (0:ℝ) < 8) (pow_pos phi_pos 5)
 159
 160/-- The normalization factor does not vanish. -/
 161theorem jcost_to_regge_factor_ne_zero : jcost_to_regge_factor ≠ 0 :=
 162  ne_of_gt jcost_to_regge_factor_pos
 163
 164/-! ## The Bridge Theorem
 165
 166The central result: J-cost stationarity on the simplicial ledger
 167is equivalent to the Regge equations, up to the normalization factor κ.
 168

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.