SignFlipFalsifier
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not encode the explicit handedness-flip schedule or its generation mechanism.
- Does not require the positive and negative segments to be consecutive or sustained.
- Does not incorporate power, temperature, or segment labels to test restoration.
- Does not specify how the trace is produced from the underlying physical model.
formal statement (Lean)
66def SignFlipFalsifier (Tmin : ℝ) (tr : Trace) : Prop :=
proof body
Definition body.
67 ∃ tpos tneg,
68 (tr.thrust tpos).2.2 ≥ Tmin ∧
69 (tr.thrust tneg).2.2 ≤ -Tmin
70
71/-- Phase-lock falsifier (display-level):
72
73There exist two times `t1 < t2` under sustained pulsing such that the thrust
74proxy decays significantly.
75
76This encodes the *failure mode* claim (“continuous forcing degrades performance”).
77It does **not** yet encode the “pulsing restores it” part; that will require
78either richer trace fields (power/temperature) or explicit segment labels.
79-/