PhaseLockFalsifier
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not incorporate ambient-pressure values into the predicate.
- Does not require the two pulsing windows to be disjoint beyond $t_1 < t_2$.
- Does not encode any restoration of thrust under intermittent pulsing.
- Does not specify physical units or scaling for the drop threshold.
formal statement (Lean)
80def PhaseLockFalsifier (window : ℕ) (drop : ℝ) (tr : Trace) : Prop :=
proof body
Definition body.
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