pith. machine review for the scientific record. sign in
theorem proved term proof

bridge_chain_complete

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Term-mode proof.

 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:
 147
 148    - discharge of the linearization hypothesis,
 149    - exact identity `∑ψ/∑κ = 1/κ_Einstein · ∑regge`,
 150    - flat-vacuum consistency,
 151    - coupling value κ_Einstein = 8 φ⁵,
 152    - coupling positivity.
 153-/

depends on (33)

Lean names referenced from this declaration's body.

… and 3 more