regge_sum_flat_under_linearization
The theorem shows that whenever the Regge deficit linearization hypothesis holds, the Regge sum vanishes for the flat vacuum configuration of the conformal edge-length field. Researchers deriving the field-curvature identity between J-cost Dirichlet energy and linearized Regge action cite it to confirm normalization of the overall constant. The proof is a one-line wrapper that instantiates the hypothesis at zero log-potential, substitutes the flat Laplacian identity, and reduces by algebraic simplification.
claimLet $D$ be a deficit-angle functional on $n$ vertices, let $a>0$, let $H$ be a list of hinge data, and let $G$ be a weighted ledger graph. If the linearization hypothesis holds for these data, then the Regge sum of $D$ evaluated on the conformal edge-length field at zero log-potential equals zero.
background
A DeficitAngleFunctional supplies, for any edge-length field, the deficit angle and area at each hinge; the Regge sum is then the weighted sum of area times deficit. The ReggeDeficitLinearizationHypothesis is the statement that this sum equals a fixed multiple of the Laplacian action of the log-potential around the flat vacuum. The conformal_edge_length_field converts a log-potential ε into an edge-length assignment via the scale a and the exponential map, so that ε ≡ 0 recovers the flat metric. The module supplies the missing map from recognition potential ψ to geometric edge lengths that turns the J-cost Dirichlet energy into a genuine Regge action once the linearization hypothesis is discharged. Upstream results include the definition of the gravitational constant G in RS-native units and the flat Laplacian identity laplacian_action_flat.
proof idea
The proof is a one-line wrapper. It applies the linearization hypothesis to the zero log-potential, rewrites the resulting expression using the flat Laplacian identity, and concludes by ring simplification.
why it matters in Recognition Science
The result is invoked inside edgeLengthFromPsiCert as the flat_regge component that completes the field-curvature identity. It corresponds to the consistency check in the Gravity from Recognition draft §5 that fixes the constant in the identification of J-cost with the linearized Regge action at coupling κ = 8 φ^5. It touches the open question of discharging the linearization hypothesis itself via explicit Cayley-Menger determinants or the Piran-Williams 3+1 split.
scope and limits
- Does not discharge the ReggeDeficitLinearizationHypothesis.
- Does not supply explicit deficit angles or areas.
- Does not address curvature terms beyond linear order.
- Does not extend the identity to non-flat background configurations.
Lean usage
theorem flat_regge_component (D : DeficitAngleFunctional n) (a : ℝ) (ha : 0 < a) (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n) (hLin : ReggeDeficitLinearizationHypothesis D a ha hinges G) : regge_sum D (conformal_edge_length_field a ha (fun _ => (0 : ℝ))) hinges = 0 := regge_sum_flat_under_linearization D a ha hinges G hLinformal statement (Lean)
239theorem regge_sum_flat_under_linearization
240 {n : ℕ} (D : DeficitAngleFunctional n) (a : ℝ) (ha : 0 < a)
241 (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n)
242 (hLin : ReggeDeficitLinearizationHypothesis D a ha hinges G) :
243 regge_sum D (conformal_edge_length_field a ha (fun _ => (0 : ℝ))) hinges = 0 := by
proof body
Term-mode proof.
244 have h := hLin (fun _ => (0 : ℝ))
245 rw [h, laplacian_action_flat]
246 ring
247
248/-! ## §5. The recognition-potential dictionary
249
250A thin convenience: the map from `ψ : Fin n → ℝ₊` to `ε : Fin n → ℝ` via
251the logarithm, with the property that flat `ψ ≡ 1` gives flat `ε ≡ 0`. -/
252
253/-- Log-potential from a strictly positive recognition-potential assignment. -/