SignFlipFalsifier
plain-language theorem explainer
SignFlipFalsifier encodes a predicate asserting that a recorded thrust trace contains segments with vertical components of opposite sign, each exceeding a supplied magnitude threshold. Groups running schedule-flip experiments in the Flight subtheory would cite it to test the expected reversal under handedness change. The definition is a direct existential unpack over the thrust field of the Trace structure.
Claim. Let $T_{\min} \in \mathbb{R}$ be a magnitude threshold and let $\mathrm{tr}$ be a trace carrying a thrust map. The predicate holds precisely when there exist times $t_+$ and $t_-$ such that the vertical component of thrust at $t_+$ is at least $T_{\min}$ while the vertical component at $t_-$ is at most $-T_{\min}$.
background
The Flight.Falsifiers module supplies executable predicates over experimental traces that encode the data-level consequences of the physical hypotheses. Trace is the minimal schema: it records ambient pressure as a function of tick, a DriveSchedule, and a thrust vector (or acceleration proxy) at each tick. The module states that these predicates begin simple and become stricter as the model tightens.
An upstream analogue appears in Gravity.Candidates.Li: its SignFlipFalsifier asserts that the induced gravitomagnetic field reverses exactly when the source field $B_0$ is reversed. The present definition supplies the corresponding interface for the propulsion trace.
proof idea
The declaration is a direct definition whose body is the existential statement over the two times and the two inequalities on the vertical thrust component. No lemmas are invoked; the predicate is the interface itself.
why it matters
It is referenced by FlightReport (the display-level status summary for the subtheory) and by the parallel SignFlipFalsifier in Gravity.Candidates.Li. The definition supplies the concrete falsifier for sign reversal under schedule flip, consistent with the eight-tick phase structure and the requirement that vector quantities reverse under handedness change. It leaves open the addition of power or temperature fields that would later encode the pulsing-restoration claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.