PhaseLockFalsifier
plain-language theorem explainer
PhaseLockFalsifier defines a predicate over an experimental trace that holds exactly when two distinct windows of sustained pulsing exist and the selected thrust component decays by at least the supplied drop amount between them. Flight subtheory modelers cite it when testing recorded data against the continuous-forcing degradation hypothesis. The definition is assembled directly from the Trace fields via existential quantification and three conjuncts with no lemmas applied.
Claim. Let $w$ be a positive integer, $d$ a real number, and let $tr$ be a trace with schedule and thrust fields. The predicate holds if and only if there exist times $t_1 < t_2$ such that the schedule commands pulses throughout each interval of length $w$ starting at $t_1$ and at $t_2$, and the selected component of the thrust vector at $t_1$ exceeds the value at $t_2$ by at least $d$.
background
The Flight.Falsifiers module supplies executable predicates over recorded traces that must hold if the physical hypotheses are correct. The Trace structure is the minimal schema: it records ambient pressure as a function of time, a DriveSchedule of pulse or no-pulse commands, and a thrust vector (or acceleration proxy) at each tick. This predicate is one of several siblings that encode failure modes; it draws on the general Falsifiers structure imported from the ILG relativity module, which enumerates numerical bands for PPN, lensing, and gravitational-wave tests.
proof idea
The definition is given directly by an existential quantifier over two times together with the three conjuncts for ordering, sustained pulsing in each window, and the thrust-component inequality. No upstream lemmas are invoked; the predicate is assembled from the schedule and thrust fields of the supplied Trace argument.
why it matters
This supplies the concrete failure-mode predicate for phase-lock behavior and is referenced by the FlightReport summary string. It encodes the claim that continuous forcing degrades performance while leaving the restoration effect under pulsing for future trace enrichment. In the Recognition Science framework it contributes to the falsifiability layer of the Flight geometry, which rests on the phi-ladder and eight-tick octave. An open question is extension of the trace with power or temperature fields to capture the full pulsing-restoration cycle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.