def
definition
gravity_ledger_consistent
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.RRF.Foundation.Gravity on GitHub at line 154.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
151 vacuum_is_flat : (curvatureFromStrain (strainFromLedger vacuumLedger) 1).R = 0
152
153/-- The gravity-ledger correspondence is consistent. -/
154def gravity_ledger_consistent : GravityLedgerCorrespondence := {
155 mass_is_density := fun _ => rfl,
156 curvature_is_strain := fun _ _ _ => rfl,
157 vacuum_is_flat := by simp [curvatureFromStrain, strainFromLedger, vacuumLedger]
158}
159
160/-- Gravity as ledger curvature is a valid interpretation. -/
161theorem gravity_interpretation_valid : Nonempty GravityLedgerCorrespondence :=
162 ⟨gravity_ledger_consistent⟩
163
164end RRF.Foundation.Gravity
165end IndisputableMonolith