theorem proved term proof

`cubicFieldCurvatureCert`

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

formal statement (Lean)

 313theorem cubicFieldCurvatureCert : CubicFieldCurvatureCert where
 314  discharge := fun a ha G => cubic_linearization_discharge a ha G

proof body

Term-mode proof.

 315  identity := fun a ha G ε => field_curvature_identity_cubic a ha G ε
 316  kappa_value := jcost_to_regge_factor_eq
 317  kappa_pos := jcost_to_regge_factor_pos
 318
 319end
 320
 321end CubicDeficitDischarge
 322end SimplicialLedger
 323end Foundation
 324end IndisputableMonolith

depends on (15)

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
identity in IndisputableMonolith.Foundation.ObserverForcing decl_use
SimplicialLedger in IndisputableMonolith.Foundation.SimplicialLedger decl_use
jcost_to_regge_factor_eq in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
jcost_to_regge_factor_pos in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
CubicFieldCurvatureCert in IndisputableMonolith.Foundation.SimplicialLedger.CubicDeficitDischarge decl_use
cubic_linearization_discharge in IndisputableMonolith.Foundation.SimplicialLedger.CubicDeficitDischarge decl_use
field_curvature_identity_cubic in IndisputableMonolith.Foundation.SimplicialLedger.CubicDeficitDischarge decl_use
G in IndisputableMonolith.Gravity.JCostInflaton decl_use
kappa_pos in IndisputableMonolith.Gravity.ZeroParameterGravity decl_use
kappa_pos in IndisputableMonolith.Materials.ThermalConductivityRegimesFromPhiLadder decl_use
kappa_pos in IndisputableMonolith.NumberTheory.AnnularCost decl_use
identity in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use