`LedgerDeadlock`

definition

show as: view math explainer →

module: IndisputableMonolith.RRF.Foundation.Gravity
domain: RRF
line: 123 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RRF.Foundation.Gravity on GitHub at line 123.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 120/-! ## Black Holes as Ledger Deadlocks -/
 121
 122/-- A region is a "deadlock" when strain is infinite / ledger can't close. -/
 123structure LedgerDeadlock where
 124  /-- The region. -/
 125  region : Type*
 126  /-- Strain diverges. -/
 127  strain_divergent : ∀ bound : ℝ, ∃ (S : LocalStrain), S.J > bound
 128  /-- Only valid move is to wait (time dilation). -/
 129  must_wait : True
 130
 131/-- The Schwarzschild radius concept. -/
 132noncomputable def schwarzschildRadius (M : ℝ) : ℝ := 2 * G_Newton * M / (3e8)^2
 133
 134/-- Inside Schwarzschild radius, ledger is maximally constrained. -/
 135structure InsideSchwarzschild (M r : ℝ) where
 136  /-- r is inside the Schwarzschild radius. -/
 137  inside : r < schwarzschildRadius M
 138  /-- Constraint density is extreme. -/
 139  extreme_density : True
 140
 141/-! ## Summary -/
 142
 143/-- The gravity-ledger correspondence. -/
 144structure GravityLedgerCorrespondence where
 145  /-- Mass is ledger density. -/
 146  mass_is_density : ∀ L : SpatialLedger, massFromSpatialLedger L = L.density
 147  /-- Curvature is strain. -/
 148  curvature_is_strain : ∀ S : LocalStrain, ∀ κ > 0,
 149    (curvatureFromStrain S κ).R = κ * S.J
 150  /-- Vacuum is flat. -/
 151  vacuum_is_flat : (curvatureFromStrain (strainFromLedger vacuumLedger) 1).R = 0
 152
 153/-- The gravity-ledger correspondence is consistent. -/

papers checked against this theorem

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