structure
definition
Trace
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Flight.Falsifiers on GitHub at line 26.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
model -
consistent -
tick -
or -
tick -
DriveSchedule -
Vec3 -
Schedule -
of -
one -
is -
of -
one -
as -
is -
of -
for -
is -
pressure -
of -
is -
one -
one -
Schedule -
vacuum
used by
formal source
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 ∧