def definition def or abbrev

`regge_equations_statement`

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

formal statement (Lean)

 183def regge_equations_statement : Prop :=

proof body

Definition body.

 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. -/

depends on (14)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
identity in IndisputableMonolith.Foundation.ObserverForcing decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
deficit_angle in IndisputableMonolith.Gravity.ReggeCalculus decl_use
HingeData in IndisputableMonolith.Gravity.ReggeCalculus decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
map in IndisputableMonolith.Measurement.RSNative.Core decl_use
identity in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use