pith. machine review for the scientific record. sign in
theorem other other

in

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  57theorem in `Constants.lean`) with the bridge identity.
  58-/
  59
  60namespace IndisputableMonolith
  61namespace Foundation
  62namespace SimplicialLedger
  63namespace ContinuumTheorem
  64
  65open Constants Cost ContinuumBridge EdgeLengthFromPsi CubicDeficitDischarge
  66
  67noncomputable section
  68
  69/-! ## §1. The field-curvature identity with κ = κ_Einstein -/
  70
  71/-- **THE FIELD-CURVATURE IDENTITY (Einstein-coupling form).**
  72
  73    For any weighted ledger graph `G`, any conformal spacing `a > 0`,
  74    and any log-potential field `ε`:
  75
  76    `laplacian_action G ε = (1 / κ_Einstein) · regge_sum ...`
  77
  78    where κ_Einstein is the Einstein gravitational coupling `8πG/c⁴ = 8 φ⁵`
  79    in RS-native units. This is the paper's Theorem 5.1 combined with
  80    Theorem 6.1: the bridge normalization equals the physical Einstein
  81    coupling. -/

depends on (17)

Lean names referenced from this declaration's body.