def
definition
strainFromLedger
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.RRF.Foundation.Gravity on GitHub at line 73.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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. -/
97theorem gravity_is_ledger_curvature (κ : ℝ) (hκ : 0 < κ) :
98 ∀ S₁ S₂ : LocalStrain, S₁.J ≤ S₂.J →
99 (curvatureFromStrain S₁ κ).R ≤ (curvatureFromStrain S₂ κ).R := by
100 intro S₁ S₂ h
101 simp only [curvatureFromStrain]
102 exact mul_le_mul_of_nonneg_left h (le_of_lt hκ)
103