HingeContribution
plain-language theorem explainer
The structure recording the deficit angle and positive area at each hinge supplies the local data for the discrete Regge action. Researchers deriving the Einstein equations from J-cost stationarity on simplicial ledgers cite this record when summing contributions over all hinges. The declaration is a direct structure that collects the deficit angle, the area, and the proof that the area is positive.
Claim. A hinge contribution is given by a deficit angle $δ ∈ ℝ$ together with an area $A > 0$.
background
The ContinuumBridge module shows that the J-cost functional on the simplicial ledger coincides with the Regge action up to normalization by κ = 8φ⁵. The upstream deficit_angle definition supplies δ_h = 2π − sum of dihedral angles at each hinge, while the as structure equates the weighted sum of squared log-coordinate differences (1/2) Σ w_ij (ε_i − ε_j)² to the normalized Regge sum (1/κ) Σ δ_h A_h. This identification rests on the quadratic expansion J(e^ε) = ε²/2 + O(ε⁴) that follows from the Recognition Composition Law.
proof idea
The structure is introduced directly by declaring its three fields: deficit angle, area, and the positivity witness. No lemmas or tactics are applied; it functions as a data carrier for the subsequent summation that recovers the total Regge action.
why it matters
This structure is required by the definition of the total Regge action as the sum over hinges of deficit angle times area. It thereby completes the step from the quadratic J-cost (via the Recognition Composition Law and phi-ladder) to the discrete Einstein equations, with normalization κ = 8φ⁵ matching the continuum limit. The module document notes that the field-curvature identity follows as a theorem from the quadratic structure of J-cost rather than an added hypothesis, citing the Cheeger-Müller-Schrader convergence result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.