pith. machine review for the scientific record. sign in
def definition def or abbrev high

FlightReport

show as:
view Lean formalization →

FlightReport defines a plain-text status summary string for the Flight subtheory. It lists proved phi-geometry lemmas, eight-gate scheduling results, key RS definitions such as the tetrahedral angle, and four falsifiers. A researcher reviewing the Flight module would consult this string for an at-a-glance status check. The body is a direct string construction that joins a fixed list of lines with newlines.

claimThe Flight report is the string obtained by joining with newlines the list containing the header for spiral-field propulsion, the enumeration of proved theorems on log-spiral geometry and eight-gate shift invariance, the key definitions including the phi-tetrahedral angle and rotor pitch, the list of falsifiers, and the notes on the medium-model proxy.

background

The Flight module supplies lightweight report helpers that mirror other report-style modules in the repository. Its local setting is a display-level summary exposing what has been proved versus assumed in the spiral-field propulsion subtheory, using only RS-native terminology. Upstream, the tick constant supplies the fundamental time quantum of one tick, while the BandingFalsifier encodes the existence of times with similar ambient pressure but discrete thrust states and the PhaseLockFalsifier encodes thrust decay under sustained pulsing.

proof idea

The definition directly constructs the string by applying String.intercalate to a literal list of lines. No lemmas or tactics are invoked; it is a pure data definition with no computation beyond string joining.

why it matters in Recognition Science

This definition supplies the human-readable entry point for the Flight subtheory, which develops phi-geometry and eight-tick scheduling for propulsion models. It references the eight-tick octave from the forcing chain and lists falsifiers that test banded operating regimes and phase-lock failure modes. No parent theorems are fed because it is a terminal display object that closes the documentation layer for the Flight domain.

scope and limits

formal statement (Lean)

  25def FlightReport : String :=

proof body

Definition body.

  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

depends on (32)

Lean names referenced from this declaration's body.

… and 2 more