bridge_chain_complete

formal source

 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. -/
 116theorem bridge_chain_complete {n : ℕ} (a : ℝ) (ha : 0 < a)
 117    (G : WeightedLedgerGraph n) :
 118    -- Discharge: `ReggeDeficitLinearizationHypothesis` holds.
 119    ReggeDeficitLinearizationHypothesis
 120      (cubicDeficitFunctional n) a ha (cubicHinges G) G ∧
 121    -- Identity: J-cost Dirichlet energy = (1/κ_E) · Regge sum.
 122    (∀ ε : LogPotential n,
 123      laplacian_action G ε
 124      = (1 / Constants.kappa_einstein) *
 125          regge_sum (cubicDeficitFunctional n)
 126            (conformal_edge_length_field a ha ε) (cubicHinges G)) ∧
 127    -- Flat vacuum: both sides zero.
 128    (laplacian_action G (fun _ => (0 : ℝ)) = 0 ∧
 129      regge_sum (cubicDeficitFunctional n)
 130        (conformal_edge_length_field a ha (fun _ => (0 : ℝ))) (cubicHinges G) = 0) ∧
 131    -- Coupling value: κ_Einstein = 8 φ⁵.
 132    Constants.kappa_einstein = 8 * Constants.phi ^ (5 : ℝ) ∧
 133    -- Coupling positivity: κ_Einstein > 0.
 134    0 < Constants.kappa_einstein := by
 135  refine ⟨cubic_linearization_discharge a ha G, ?_, ?_, Constants.kappa_einstein_eq,
 136          Constants.kappa_einstein_pos⟩
 137  · intro ε
 138    exact field_curvature_identity_einstein a ha G ε
 139  · refine ⟨laplacian_action_flat G, flat_regge_sum_zero a ha G⟩
 140
 141/-! ## §3. Master certificate -/
 142
 143/-- **CONTINUUM FIELD-CURVATURE CERTIFICATE.**
 144
 145    The single artifact to cite when invoking the field-curvature
 146    identity with the Einstein coupling. Combines: