`LocalStrain`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

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

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

  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.
  86-/
  87structure ScalarCurvature where
  88  /-- Scalar curvature (Ricci scalar). -/
  89  R : ℝ
  90
  91/-- Curvature from strain (the gravity mapping). -/
  92def curvatureFromStrain (S : LocalStrain) (κ : ℝ) : ScalarCurvature := {
  93  R := κ * S.J  -- Linear relationship (Einstein's equation in weak field)
  94}
  95
  96/-- The bridge theorem: curvature is monotonic in strain. -/

papers checked against this theorem

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