theorem proved term proof

`cubic_linearization_discharge`

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

formal statement (Lean)

 277theorem cubic_linearization_discharge {n : ℕ} (a : ℝ) (ha : 0 < a)
 278    (G : WeightedLedgerGraph n) :
 279    ReggeDeficitLinearizationHypothesis
 280      (cubicDeficitFunctional n) a ha (cubicHinges G) G := by

proof body

Term-mode proof.

 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).** -/

used by (10)

From the project-wide theorem graph. These declarations reference this one in their body.

bridge_chain_complete in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumTheorem decl_use
continuumFieldCurvatureCert in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumTheorem decl_use
flat_regge_sum_zero in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumTheorem decl_use
cubicFieldCurvatureCert in IndisputableMonolith.Foundation.SimplicialLedger.CubicDeficitDischarge decl_use
field_curvature_identity_cubic in IndisputableMonolith.Foundation.SimplicialLedger.CubicDeficitDischarge decl_use
refinement_discharge_inherits in IndisputableMonolith.Foundation.SimplicialLedger.CubicSimplicialEquivalence decl_use
exact_flat_agrees_with_linearized in IndisputableMonolith.Foundation.SimplicialLedger.NonlinearBridge decl_use
jcost_stationarity_to_regge_nonlinear in IndisputableMonolith.Foundation.SimplicialLedger.NonlinearBridge decl_use
calibrated_iff_hypothesis in IndisputableMonolith.Foundation.SimplicialLedger.SimplicialDeficitDischarge decl_use
cubic_calibrated_against_graph in IndisputableMonolith.Foundation.SimplicialLedger.SimplicialDeficitDischarge decl_use

depends on (10)

Lean names referenced from this declaration's body.

G in IndisputableMonolith.Constants decl_use
G in IndisputableMonolith.Constants.Codata decl_use
G in IndisputableMonolith.Cost.FunctionalEquation decl_use
WeightedLedgerGraph in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
cubicDeficitFunctional in IndisputableMonolith.Foundation.SimplicialLedger.CubicDeficitDischarge decl_use
cubicHinges in IndisputableMonolith.Foundation.SimplicialLedger.CubicDeficitDischarge decl_use
laplacian_action_as_prod_sum in IndisputableMonolith.Foundation.SimplicialLedger.CubicDeficitDischarge decl_use
regge_sum_cubicHinges in IndisputableMonolith.Foundation.SimplicialLedger.CubicDeficitDischarge decl_use
ReggeDeficitLinearizationHypothesis in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
G in IndisputableMonolith.Gravity.JCostInflaton decl_use