`IndisputableMonolith.Relativity.GRLimit`

IndisputableMonolith/Relativity/GRLimit.lean · 14 lines · 0 declarations

Explainer status: ready · generated 2026-05-13 18:30:23.705455+00:00

   1/-!
   2Temporarily deferred: GR Limit Module Aggregator
   3
   4This module is intentionally disabled to reduce scope for the current
   5milestone. All previous imports are commented out below. Re-enable
   6by uncommenting the imports when ready to work on GR-limit results.
   7-/
   8
   9-- import IndisputableMonolith.Relativity.GRLimit.Continuity
  10-- import IndisputableMonolith.Relativity.GRLimit.Observables
  11-- import IndisputableMonolith.Relativity.GRLimit.Parameters
  12
  13-- (Intentionally left empty while deferred)
  14

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