VacuumTestFalsifier
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove any propulsion mechanism.
- Does not control for variables other than pressure and thrust.
- Applies only to traces that match the minimal Trace schema.
- Failure does not disprove the model without additional experimental controls.
Lean usage
Falsifiers.VacuumTestFalsifier 1e-4 0.003 traceformal statement (Lean)
42def VacuumTestFalsifier (p_max : ℝ) (Tmin : ℝ) (tr : Trace) : Prop :=
proof body
Definition body.
43 (∃ t, tr.ambientPressure t ≤ p_max ∧ (tr.thrust t).2.2 ≥ Tmin)
44
45/-- Banding falsifier:
46
47There exist times `t1 < t2 < t3` with similar ambient pressure but discrete
48thrust states (off/on/off). This encodes the “banded operating regimes” claim.
49-/