pith. machine review for the scientific record. sign in
theorem proved term proof

regge_action_flat

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 163theorem regge_action_flat (hinges : List HingeData)
 164    (h_flat : ∀ h ∈ hinges, deficit_angle h = 0) :
 165    regge_action hinges = 0 := by

proof body

Term-mode proof.

 166  unfold regge_action
 167  suffices h : (hinges.map (fun h => h.area * deficit_angle h)) = hinges.map (fun _ => 0) by
 168    rw [h]; simp
 169  apply List.map_congr_left
 170  intro h hm
 171  rw [h_flat h hm, mul_zero]
 172
 173/-- The Regge equations: stationarity of S_Regge with respect to edge
 174    lengths L_e gives the discrete Einstein equations.
 175
 176    delta S_Regge / delta L_e = sum_h (dA_h/dL_e * delta_h + A_h * d(delta_h)/dL_e) = 0
 177
 178    In Regge calculus, the remarkable identity (Regge 1961, Schläfli):
 179    sum_h A_h * d(delta_h)/dL_e = 0
 180
 181    So the Regge equations simplify to:
 182    sum_h (dA_h/dL_e) * delta_h = 0 -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (13)

Lean names referenced from this declaration's body.