IndisputableMonolith.Flight.Report

   1import Mathlib
   2import IndisputableMonolith.Flight.Geometry
   3import IndisputableMonolith.Flight.Schedule
   4import IndisputableMonolith.Flight.Falsifiers
   5
   6/-!
   7# Flight Report
   8
   9Small, human-readable report helpers for the Flight subtheory.
  10
  11The goal is to mirror other “report” style modules in the repo: expose
  12lightweight indicators of what is proved vs. assumed, and what falsifiers
  13exist.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace Flight
  18
  19/-- A tiny, display-level status summary for the Flight subtheory.
  20
  21This is intentionally a pure string (not JSON) so it can be printed from Lean.
  22
  23All terminology is RS-native (no third-party branding).
  24-/
  25def FlightReport : String :=
  26  String.intercalate "\n" [
  27    "FlightReport (IndisputableMonolith.Flight) — Spiral-Field Propulsion",
  28    "",
  29    "[M] Theorems proved (φ-geometry + 8-gate):",
  30    "- Flight.Geometry.SpiralLemmas.logSpiral_ne_zero",
  31    "- Flight.Geometry.SpiralLemmas.stepRatio_logSpiral_closed_form",
  32    "- Flight.Geometry.SpiralLemmas.stepRatio_invariant_under_r0",
  33    "- Flight.Geometry.SpiralLemmas.perTurn_ratio",
  34    "- Flight.Geometry.SpiralLemmas.kappa_discreteness",
  35    "- Flight.Schedule.eightGateNeutral_shift_invariance (under Schedule.Periodic8)",
  36    "",
  37    "Key RS definitions:",
  38    "- Flight.Geometry.phiTetrahedralAngle (arccos(-1/3) ≈ 109.47°)",
  39    "- Flight.Geometry.RotorPitch (φ-spiral pitch family)",
  40    "- Flight.Schedule.DriveSchedule (8-tick window discipline)",
  41    "",
  42    "Falsifiers implemented:",
  43    "- Flight.Falsifiers.VacuumTestFalsifier",
  44    "- Flight.Falsifiers.BandingFalsifier",
  45    "- Flight.Falsifiers.SignFlipFalsifier",
  46    "- Flight.Falsifiers.PhaseLockFalsifier",
  47    "",
  48    "Notes:",
  49    "- Medium model is currently a local proxy (decoupled from LNAL VM) for build stability.",
  50    "- Stability/NS bridge is planned as an optional module, not re-exported by Flight.lean yet."
  51  ]
  52
  53end Flight
  54end IndisputableMonolith
  55