`massFromSpatialLedger`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

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

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

  52/-! ## Mass from Ledger -/
  53
  54/-- Mass is ledger density (the key identification). -/
  55def massFromSpatialLedger (L : SpatialLedger) : ℝ := L.density
  56
  57/-- Mass is non-negative. -/
  58theorem mass_nonneg (L : SpatialLedger) : 0 ≤ massFromSpatialLedger L := L.density_nonneg
  59
  60/-- Vacuum has zero mass. -/
  61theorem vacuum_has_zero_mass : massFromSpatialLedger vacuumLedger = 0 := rfl
  62
  63/-! ## Local Strain -/
  64
  65/-- Local strain: the "tightness" of constraints at a point. -/
  66structure LocalStrain where
  67  /-- Strain value. -/
  68  J : ℝ
  69  /-- Strain is non-negative. -/
  70  J_nonneg : 0 ≤ J
  71
  72/-- Strain from ledger density. -/
  73def strainFromLedger (L : SpatialLedger) : LocalStrain := {
  74  J := L.density,  -- Strain is proportional to mass/density
  75  J_nonneg := L.density_nonneg
  76}
  77
  78/-- Vacuum has zero strain. -/
  79theorem vacuum_has_zero_strain : (strainFromLedger vacuumLedger).J = 0 := rfl
  80
  81/-! ## Curvature -/
  82
  83/-- Curvature is a monotonic function of strain.
  84
  85In full GR, this would be a tensor. Here we use a simplified scalar model.

papers checked against this theorem

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