`as`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge
domain: Foundation
line: 130 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge on GitHub at line 130.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 127For small deficit angles (weak field), δ_h ≈ Σ_σ∋h (ε_σ − ε_σ') · geometry_factor.
 128
 129This means S_Regge is QUADRATIC in the perturbation, with the same
 130structure as the Laplacian action. The identification is:
 131
 132  (1/2) Σ_{i~j} w_ij · (ε_i − ε_j)² = (1/κ) Σ_h δ_h · A_h
 133
 134with w_ij = A_ij / (κ · vol_i) where A_ij is the shared face area
 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. -/

papers checked against this theorem

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