flat_regge_sum_zero
The theorem shows that the Regge sum of the cubic deficit functional vanishes on the conformal edge-length field generated by the zero perturbation. Researchers assembling the linearized Einstein equations from the Recognition Composition Law would cite it to anchor the flat-vacuum baseline. The term proof reduces the sum via the cubic linearization discharge to a multiple of the Laplacian action on the zero field, which is zero by the flat-action lemma.
claimLet $n$ be a natural number, $a>0$ a real scalar, and $G$ a weighted ledger graph. Then the Regge sum of the cubic deficit functional on the conformal edge-length field produced by the zero perturbation equals zero: $$regge_sum(cubicDeficitFunctional(n), conformal_edge_length_field(a, zero), cubicHinges(G)) = 0.$$
background
The ContinuumTheorem module assembles Phase D of the program to realize the paper's Theorem 5.1 as an unconditional result. It composes the cubic linearization discharge with the normalization of the bridge factor to the Einstein coupling. The J-cost Dirichlet energy is realized as the Laplacian action on a perturbation field ε, while the Regge sum integrates the cubic deficit over the hinges of G. The upstream cubic_linearization_discharge equates the Regge sum to the scaled Dirichlet energy for arbitrary ε, and laplacian_action_flat records that the action on the zero field is identically zero. The module documentation states that the construction yields the exact linearized identity with the Einstein coupling and the flat-vacuum baseline.
proof idea
The proof is a short term-mode reduction. It applies cubic_linearization_discharge a ha G (zero field) to obtain equality with jcost_to_regge_factor times laplacian_action G (zero field), then rewrites the second factor via laplacian_action_flat and concludes by multiplication with zero.
why it matters in Recognition Science
The corollary supplies the flat_regge component inside the ContinuumFieldCurvatureCert and is invoked by bridge_chain_complete. It confirms the vanishing at the flat vacuum required by the module documentation on the complete cubic bridge chain. The result closes the zero-energy case in the forcing sequence that runs from the Recognition Composition Law through J-uniqueness and φ-forcing to the linearized Einstein equations with coupling κ_Einstein = 8 φ^5.
scope and limits
- Does not treat the full nonlinear Regge action on refined triangulations.
- Does not supply quantitative convergence rates under mesh refinement.
- Does not extend beyond cubic hinge structures.
- Does not incorporate Lorentzian signatures or time-dependent fields.
formal statement (Lean)
94theorem flat_regge_sum_zero {n : ℕ} (a : ℝ) (ha : 0 < a)
95 (G : WeightedLedgerGraph n) :
96 regge_sum (cubicDeficitFunctional n)
97 (conformal_edge_length_field a ha (fun _ => (0 : ℝ))) (cubicHinges G)
98 = 0 := by
proof body
Term-mode proof.
99 have h_disch : regge_sum (cubicDeficitFunctional n)
100 (conformal_edge_length_field a ha (fun _ => (0 : ℝ))) (cubicHinges G)
101 = jcost_to_regge_factor * laplacian_action G (fun _ => (0 : ℝ)) :=
102 cubic_linearization_discharge a ha G (fun _ => (0 : ℝ))
103 rw [h_disch, laplacian_action_flat, mul_zero]
104
105/-! ## §2. The composed bridge chain
106
107For documentation: this is the complete assembly of the cubic-lattice
108bridge from the Recognition Composition Law to Einstein's field equations
109in the linearized regime. -/
110
111/-- **THE COMPLETE CUBIC BRIDGE CHAIN.**
112
113 Given the RCL → J uniqueness → φ forced → constants (all proved
114 upstream), the linearization identity holds exactly with the Einstein
115 coupling and vanishes at the flat vacuum. -/