theorem proved term proof

`continuum_bridge_cert`

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

formal statement (Lean)

 313theorem continuum_bridge_cert : ContinuumBridgeCert where
 314  chain := jcost_to_efe_chain

proof body

Term-mode proof.

 315  flat_vacuum := fun G => flat_is_vacuum G
 316  kappa_derived := jcost_to_regge_factor_eq
 317  kappa_pos := jcost_to_regge_factor_pos
 318  flat_cost_zero := flat_zero_cost
 319  deficit_correspondence := fun _ => rfl
 320
 321end
 322
 323end ContinuumBridge
 324end SimplicialLedger
 325end Foundation
 326end IndisputableMonolith

depends on (14)

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
SimplicialLedger in IndisputableMonolith.Foundation.SimplicialLedger decl_use
ContinuumBridgeCert in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
flat_is_vacuum in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
flat_zero_cost in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
jcost_to_efe_chain in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge 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
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