IndisputableMonolith.Flight

   1import IndisputableMonolith.Flight.Geometry
   2import IndisputableMonolith.Flight.Medium
   3import IndisputableMonolith.Flight.Pressure
   4import IndisputableMonolith.Flight.Schedule
   5import IndisputableMonolith.Flight.Thrust
   6import IndisputableMonolith.Flight.Falsifiers
   7import IndisputableMonolith.Flight.Report
   8import IndisputableMonolith.Flight.GravityBridge
   9
  10/-!
  11# IndisputableMonolith.Flight
  12
  13Spiral-Field Propulsion formalization scaffold (φ-Vortex Drive).
  14
  15This module is a convenience facade that re-exports the Flight submodules.
  16The intent is to:
  17- keep mathematical lemmas provable in Lean,
  18- isolate physical hypotheses as explicit assumptions,
  19- provide executable falsifiers for lab traces.
  20
  21All geometry is derived from RS constants (φ-tetrahedral angle, φ-spiral paths).
  22
  23Note: `IndisputableMonolith.Flight.Stability` exists but is not re-exported here yet,
  24since it pulls in heavier verification subtrees that are being modernized.
  25-/
  26