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. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.