`cubic_linearization_discharge`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.SimplicialLedger.CubicDeficitDischarge
domain: Foundation
line: 277 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.SimplicialLedger.CubicDeficitDischarge on GitHub at line 277.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 274/-- **MAIN THEOREM.** The `ReggeDeficitLinearizationHypothesis` is
 275    discharged unconditionally for any weighted ledger graph `G` using
 276    the cubic deficit functional and hinge list. -/
 277theorem cubic_linearization_discharge {n : ℕ} (a : ℝ) (ha : 0 < a)
 278    (G : WeightedLedgerGraph n) :
 279    ReggeDeficitLinearizationHypothesis
 280      (cubicDeficitFunctional n) a ha (cubicHinges G) G := by
 281  intro ε
 282  rw [regge_sum_cubicHinges a ha ε G, laplacian_action_as_prod_sum G ε]
 283  ring
 284
 285/-! ## §9. The paper's Theorem 5.1 on the cubic lattice -/
 286
 287/-- **THE FIELD-CURVATURE IDENTITY (cubic lattice).** -/
 288theorem field_curvature_identity_cubic {n : ℕ} (a : ℝ) (ha : 0 < a)
 289    (G : WeightedLedgerGraph n) (ε : LogPotential n) :
 290    laplacian_action G ε
 291    = (1 / jcost_to_regge_factor) *
 292        regge_sum (cubicDeficitFunctional n)
 293          (conformal_edge_length_field a ha ε) (cubicHinges G) :=
 294  field_curvature_identity_under_linearization
 295    (cubicDeficitFunctional n) a ha (cubicHinges G) G
 296    (cubic_linearization_discharge a ha G) ε
 297
 298/-! ## §10. Certificate -/
 299
 300structure CubicFieldCurvatureCert where
 301  discharge : ∀ {n : ℕ} (a : ℝ) (ha : 0 < a) (G : WeightedLedgerGraph n),
 302    ReggeDeficitLinearizationHypothesis
 303      (cubicDeficitFunctional n) a ha (cubicHinges G) G
 304  identity : ∀ {n : ℕ} (a : ℝ) (ha : 0 < a) (G : WeightedLedgerGraph n)
 305    (ε : LogPotential n),
 306    laplacian_action G ε
 307    = (1 / jcost_to_regge_factor) *

papers checked against this theorem

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