claimed_effect_range
plain-language theorem explainer
Podkletnov's reported weight reduction above a rotating YBCO disk is captured as the closed interval from 0.3 to 2.1 percent. Gravity-anomaly modelers in Recognition Science cite this bound when applying Flight falsifiers to distinguish metric-kernel shifts from air-current artifacts. The declaration is a direct predicate definition on a real parameter.
Claim. Let $w$ denote the claimed weight-loss percentage. Then $0.3 ≤ w ≤ 2.1$.
background
The Podkletnov module encodes the 1992/1997 experimental claim that a rotating YBCO superconductor disk induces 0.3%–2.1% weight reduction in overhead test masses. Recognition Science treats the anomaly either as an ILG modification of the local metric weight kernel $w(k,a)$ or as spiral-field thrust arising from a phase gradient. The definition supplies the magnitude anchor for downstream falsifiers such as vacuum persistence, which requires the effect to survive removal of air currents and ion wind.
proof idea
Direct definition: the body is the conjunction of the two inequalities that bound the input real number.
why it matters
The definition supplies the quantitative experimental claim that the Recognition Science framework must accommodate when modeling gravity anomalies. It feeds the thrust/weight-anomaly interpretation and the vacuum-persistence falsifier listed in the module. No downstream theorems yet reference it, leaving open its eventual linkage to the eight-tick octave or phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.