`ContinuumBridgeCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge
domain: Foundation
line: 304 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge on GitHub at line 304.

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

 301/-- The Continuum Bridge Certificate: J-cost stationarity on the
 302    simplicial ledger produces the Einstein field equations
 303    in the continuum limit, with coupling κ = 8φ⁵. -/
 304structure ContinuumBridgeCert where
 305  chain : JCostToEFE
 306  flat_vacuum : ∀ {n : ℕ} (G : WeightedLedgerGraph n),
 307    ∀ i, discrete_laplacian G (fun _ => (0 : ℝ)) i = 0
 308  kappa_derived : jcost_to_regge_factor = 8 * phi ^ 5
 309  kappa_pos : 0 < jcost_to_regge_factor
 310  flat_cost_zero : Jcost 1 = 0
 311  deficit_correspondence : ∀ δε : ℝ, J_log_quadratic δε = δε ^ 2 / 2
 312
 313theorem continuum_bridge_cert : ContinuumBridgeCert where
 314  chain := jcost_to_efe_chain
 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

papers checked against this theorem

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