`FlightReport`

definition

show as: view math explainer →

module: IndisputableMonolith.Flight.Report
domain: Flight
line: 25 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Flight.Report on GitHub at line 25.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.