IndisputableMonolith.Flight.Falsifiers

   1import Mathlib
   2import IndisputableMonolith.Flight.Schedule
   3import IndisputableMonolith.Flight.Thrust
   4
   5/-!
   6# Flight Falsifiers
   7
   8Executable predicates over recorded traces.
   9
  10These are intentionally simple “interfaces” at first: the goal is to
  11encode *what must be true in data* if the physical hypotheses are true.
  12
  13As the physical model tightens, these falsifiers should become stricter.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace Flight
  18namespace Falsifiers
  19
  20open IndisputableMonolith.Flight
  21
  22/-- Minimal experimental trace schema (display-level).
  23
  24This is intentionally small and can be extended.
  25-/
  26structure Trace where
  27  /-- Ambient pressure (e.g., vacuum chamber pressure) as a function of time tick. -/
  28  ambientPressure : ℕ → ℝ
  29  /-- Commanded schedule (pulse/no-pulse). -/
  30  schedule : Schedule.DriveSchedule
  31  /-- Measured thrust vector (or inferred acceleration proxy). -/
  32  thrust : ℕ → Thrust.Vec3
  33
  34/-- Vacuum persistence falsifier:
  35
  36If thrust remains nonzero while ambient pressure is lowered below a threshold,
  37then the claim is *consistent* with non-aerodynamic propulsion.
  38
  39(This is a *one-way* falsifier: failure does not disprove the model unless
  40we control for other conditions.)
  41-/
  42def VacuumTestFalsifier (p_max : ℝ) (Tmin : ℝ) (tr : Trace) : Prop :=
  43  (∃ t, tr.ambientPressure t ≤ p_max ∧ (tr.thrust t).2.2 ≥ Tmin)
  44
  45/-- Banding falsifier:
  46
  47There exist times `t1 < t2 < t3` with similar ambient pressure but discrete
  48thrust states (off/on/off). This encodes the “banded operating regimes” claim.
  49-/
  50def BandingFalsifier (εp : ℝ) (Tmin : ℝ) (tr : Trace) : Prop :=
  51  ∃ t1 t2 t3,
  52    t1 < t2 ∧ t2 < t3 ∧
  53    |tr.ambientPressure t1 - tr.ambientPressure t2| ≤ εp ∧
  54    |tr.ambientPressure t2 - tr.ambientPressure t3| ≤ εp ∧
  55    (tr.thrust t1).2.2 < Tmin ∧
  56    (tr.thrust t2).2.2 ≥ Tmin ∧
  57    (tr.thrust t3).2.2 < Tmin
  58
  59/-- Sign-flip falsifier:
  60
  61Under a schedule “handedness flip” (modeled externally), thrust should flip sign.
  62
  63At the trace level, we encode this as the existence of two segments with
  64opposite-signed vertical thrust.
  65-/
  66def SignFlipFalsifier (Tmin : ℝ) (tr : Trace) : Prop :=
  67  ∃ tpos tneg,
  68    (tr.thrust tpos).2.2 ≥ Tmin ∧
  69    (tr.thrust tneg).2.2 ≤ -Tmin
  70
  71/-- Phase-lock falsifier (display-level):
  72
  73There exist two times `t1 < t2` under sustained pulsing such that the thrust
  74proxy decays significantly.
  75
  76This encodes the *failure mode* claim (“continuous forcing degrades performance”).
  77It does **not** yet encode the “pulsing restores it” part; that will require
  78either richer trace fields (power/temperature) or explicit segment labels.
  79-/
  80def PhaseLockFalsifier (window : ℕ) (drop : ℝ) (tr : Trace) : Prop :=
  81  ∃ t1 t2,
  82    t1 < t2 ∧
  83    (∀ t, t1 ≤ t ∧ t < t1 + window → (tr.schedule t).pulse = true) ∧
  84    (∀ t, t2 ≤ t ∧ t < t2 + window → (tr.schedule t).pulse = true) ∧
  85    (tr.thrust t1).2.2 - (tr.thrust t2).2.2 ≥ drop
  86
  87end Falsifiers
  88end Flight
  89end IndisputableMonolith
  90
  91