`flat_regge_sum_zero`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.SimplicialLedger.ContinuumTheorem
domain: Foundation
line: 94 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.SimplicialLedger.ContinuumTheorem on GitHub at line 94.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  91/-- **COROLLARY.** The flat vacuum `ε ≡ 0` has zero J-cost Dirichlet
  92    energy, and therefore (by the identity) the Regge sum on the
  93    conformal edge-length field of the flat vacuum also vanishes. -/
  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
  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. -/
 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) *

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.