`massiveLedger`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

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

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

  42}
  43
  44/-- A non-vacuum ledger with mass. -/
  45def massiveLedger (d : ℝ) (hd : 0 < d) : SpatialLedger := {
  46  density := d,
  47  density_nonneg := le_of_lt hd,
  48  charge := 0,
  49  balanced := rfl
  50}
  51
  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

papers checked against this theorem

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