VacuumTestFalsifier
plain-language theorem explainer
VacuumTestFalsifier defines a predicate that holds when a trace records nonzero vertical thrust at some time tick where ambient pressure has fallen below a supplied threshold. Experimental groups testing vacuum-persistence claims in spiral-field propulsion would invoke it on chamber data. The definition expands directly to an existential quantifier over the trace's pressure and thrust fields.
Claim. The predicate holds if there exists a time $t$ such that the ambient-pressure function of the trace at $t$ is at most $p_0$ and the third component of the thrust vector at $t$ is at least $T_0$.
background
The Trace structure supplies three fields: ambient pressure as a function of discrete time ticks, a commanded drive schedule, and a measured thrust vector. This definition sits inside the Flight Falsifiers module, whose purpose is to encode executable data requirements that must hold if the underlying physical hypotheses are correct. It references the momentum cutoff $p_0$ from the QFT UVCutoff module and pressure expressions from the ILG PressureForm module to anchor the numerical thresholds.
proof idea
The definition is a direct expansion to an existential quantifier that inspects the ambientPressure and thrust fields of the supplied trace at a single time tick.
why it matters
The predicate is the core object called by VacuumPersistence in the Podkletnov candidate module and appears inside the FlightReport summary string. It supplies the one-way consistency test required by the Flight subtheory to distinguish non-aerodynamic effects from residual gas dynamics, consistent with the Recognition Science emphasis on generating falsifiable predictions from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.