BandingFalsifier
plain-language theorem explainer
The BandingFalsifier predicate asserts the existence of three ordered times in a recorded trace where ambient pressure changes remain bounded by a small εp while the vertical thrust component crosses a minimum threshold from below to above and back below. Experimentalists validating banded operating regimes in spiral-field propulsion data would cite this predicate when scanning traces for the predicted discrete on-off-on pattern. The definition is a direct existential encoding over the trace's pressure and thrust functions with no auxiliary le
Claim. Given thresholds $ε_p > 0$ and $T_{min} > 0$, and a trace $tr$ consisting of an ambient-pressure function and a thrust function to vectors, the banding falsifier holds if there exist times $t_1 < t_2 < t_3$ such that $|tr.ambientPressure(t_1) - tr.ambientPressure(t_2)| ≤ ε_p$, $|tr.ambientPressure(t_2) - tr.ambientPressure(t_3)| ≤ ε_p$, the vertical component of $tr.thrust(t_1)$ is less than $T_{min}$, the vertical component of $tr.thrust(t_2)$ is at least $T_{min}$, and the vertical component of $tr.thrust(t_3)$ is less than $T_{min}$.
background
The Flight.Falsifiers module supplies executable predicates over recorded traces that must hold if the Recognition Science flight hypotheses are correct. The central data structure is the Trace record, which packages ambientPressure as a map from time ticks to reals, a commanded DriveSchedule, and thrust as a map to Vec3 vectors. These predicates are intentionally minimal interfaces that tighten as the underlying model is refined. Upstream structures such as LedgerFactorization and PhiForcingDerived supply the J-cost and ledger foundations that motivate the discrete thrust states appearing in the trace.
proof idea
As a definition the BandingFalsifier is realized by a direct existential quantifier over three time variables together with the listed inequalities on consecutive pressure differences and the off-on-off pattern in the vertical thrust component. No lemmas are invoked; the body is the literal encoding of the required pattern.
why it matters
This definition supplies one of the falsifiable signatures collected in the downstream FlightReport for the spiral-field propulsion subtheory. It encodes the banded operating regimes claim and sits inside the Flight module that inherits the eight-tick octave and phi-ladder from the foundational forcing chain. The predicate therefore serves as a concrete check that discrete thrust transitions occur under stable pressure conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.