`IndisputableMonolith.Gravity`

IndisputableMonolith/Gravity.lean · 29 lines · 0 declarations

Explainer status: pending

   1import IndisputableMonolith.Gravity.ILG
   2import IndisputableMonolith.Gravity.Rotation
   3import IndisputableMonolith.Gravity.ParameterizationBridge
   4import IndisputableMonolith.Gravity.DerivedFactors
   5
   6/-!
   7# IndisputableMonolith.Gravity
   8
   9Gravity module facade - re-exports core gravity formalizations:
  10- `Rotation`: Newtonian rotation curve identities (v² = GM/r, flat curves)
  11- `ILG`: Information-Limited Gravity time-kernel and weight functions
  12- `DerivedFactors`: HSB suppression derived from SevenBeatViolation saturation
  13- `ParameterizationBridge`: Links α to T_dyn/T_0 ratios
  14
  15See also `IndisputableMonolith.Relativity.ILG` for the full relativistic ILG formalization
  16(currently sealed pending Mathlib updates).
  17-/
  18
  19namespace IndisputableMonolith
  20namespace Gravity
  21
  22-- Re-export key definitions
  23open ILG (w_t w_t_ref w_t_rescale w_t_nonneg Params ParamProps BridgeData)
  24open Rotation (RotSys vrot vrot_sq vrot_flat_of_linear_Menc)
  25open DerivedFactors (xi_derived a_saturation)
  26
  27end Gravity
  28end IndisputableMonolith
  29

source mirrored from github.com/jonwashburn/shape-of-logic