SignFlipFalsifier
plain-language theorem explainer
SignFlipFalsifier requires that a thrust trace under an external handedness flip contains both a vertical component above a positive minimum threshold and one below its negative counterpart. Flight experimenters testing spiral-field propulsion in vacuum chambers would cite this predicate when checking data for sign-reversal consistency. The definition is a direct existential quantification over two time indices in the trace's thrust function.
Claim. Let $T_>0$ be a minimum thrust threshold and let $tr$ be an experimental trace whose thrust function returns a three-vector at each time tick. Then the predicate holds precisely when there exist times $t_+$ and $t_-$ such that the vertical component of thrust at $t_+$ is at least $T$ and the vertical component at $t_-$ is at most $-T$.
background
The Flight.Falsifiers module defines executable predicates over recorded traces that must hold in data if the physical hypotheses are true. These predicates begin as minimal interfaces and tighten as the model is refined. Trace is the core schema: it stores ambient pressure as a function of time tick, the commanded DriveSchedule, and the measured thrust vector at each tick. The present definition is the flight-level counterpart of the sign-reversal condition appearing in Gravity.Candidates.Li, where reversal of the base field must reverse the induced gravitomagnetic component.
proof idea
The declaration is a direct definition. It asserts the existence of two time indices in the trace such that the vertical thrust component meets or exceeds the supplied positive threshold at one index and meets or falls below the negative threshold at the other.
why it matters
This supplies one of the core falsifiability checks for the Flight subtheory of spiral-field propulsion. It is referenced by FlightReport when summarizing the status of the φ-geometry and 8-gate theorems. It mirrors the sign-flip condition in the Li candidate, thereby linking the flight model to the Recognition Science framework of vector-field reversals under the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.