VacuumPersistence
plain-language theorem explainer
VacuumPersistence defines the predicate asserting that a given experimental trace exhibits nonzero thrust at ambient pressures below 1e-4, thereby excluding ion-wind or thermal artifacts in Podkletnov-style tests. Researchers formalizing gravity-shielding claims within Recognition Science would cite it when applying Flight falsifiers to rotating-superconductor data. The definition is a direct one-line wrapper around the VacuumTestFalsifier predicate instantiated at the stated thresholds.
Claim. Let $tr$ be a trace consisting of an ambient-pressure function, a drive schedule, and a thrust vector. Then VacuumPersistence$(tr)$ holds precisely when there exists a time $t$ such that the pressure at $t$ is at most $10^{-4}$ and the vertical thrust component at $t$ is at least $0.003$.
background
The Podkletnov module formalizes the 1992/1997 claim of weight reduction above a rotating YBCO disk as either an ILG metric modification or a spiral-field thrust, subject to Flight falsifiers. The Trace structure records ambient pressure as a function of time, the commanded schedule, and the measured thrust vector. VacuumTestFalsifier returns true exactly when thrust remains above a minimum while pressure falls below a chosen maximum, serving as a one-way consistency check against aerodynamic explanations.
proof idea
This is a one-line wrapper that applies the VacuumTestFalsifier definition with parameters p_max = 1e-4 and Tmin = 0.003 directly to the supplied trace.
why it matters
The definition supplies the vacuum-persistence falsifier required by the Podkletnov hypothesis, ensuring any claimed thrust cannot be dismissed as residual air effects. It feeds the broader set of Flight falsifiers used to test RS interpretations of the anomaly against classical alternatives. Within the Recognition Science framework it supports the distinction between genuine metric or phase-gradient forces and artifacts, consistent with the requirement that all physics derive from the J-cost functional and the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.