PhaseLockFalsifier
plain-language theorem explainer
PhaseLockFalsifier defines a predicate on a Trace that asserts existence of two separated pulsing windows of given length where the third thrust component drops by at least the supplied amount. Propulsion experimenters would cite it when checking recorded schedules for continuous-forcing degradation. The definition expands directly into quantified conditions on schedule.pulse and thrust vectors.
Claim. Let $w$ be a positive integer, $d$ a real number, and $tr$ a trace with schedule and thrust functions. The predicate holds if there exist times $t_1 < t_2$ such that the schedule pulses throughout both intervals of length $w$ starting at $t_1$ and at $t_2$, and the difference in the third component of thrust satisfies $(tr.thrust(t_1))_3 - (tr.thrust(t_2))_3 ≥ d$.
background
The Flight.Falsifiers module supplies executable predicates over recorded traces that encode what data must show if the physical hypotheses hold. Trace is the minimal schema containing ambientPressure as a function of time, a DriveSchedule of pulse/no-pulse commands, and a sequence of thrust vectors. The module documentation states these are intentionally simple interfaces that tighten as the model matures.
proof idea
This is a direct definition that unpacks into an existential statement over time indices with constraints drawn from the schedule and thrust fields of the input Trace. No lemmas are applied.
why it matters
The definition supplies one falsifier predicate consumed by FlightReport to summarize the Flight subtheory. It implements the failure-mode claim that continuous forcing degrades performance. It parallels the Falsifiers structure from Relativity.ILG and supports experimental checks within the spiral-field propulsion setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.