ResonantSpeedFalsifier
plain-language theorem explainer
This definition introduces a predicate asserting that a rotation speed in rpm aligns with a phi-resonant mode under the Recognition Science model of Podkletnov gravity shielding. Experimentalists testing anomalous weight reduction claims would cite it to check reported critical speeds such as those near 5000 rpm. The implementation is a placeholder returning the constant true proposition, awaiting replacement by an explicit phi-harmonic check derived from J-cost structures.
Claim. Let $r$ be a real number denoting rotation speed in rpm. The predicate holds if and only if $r$ equals a resonant frequency on the phi-ladder, where phi is the unique positive fixed point of the self-similar forcing $J(x) = (x + x^{-1})/2 - 1$.
background
Recognition Science organizes quantities on discrete phi-ladders, with nuclear densities scaling as phi to an integer power times Planck density (NucleosynthesisTiers.of). The J-cost $J(x) = (x + x^{-1})/2 - 1$ is strictly convex with global minimum at $x=1$, and local dynamics update at most eight neighbors per tick (PhysicsComplexityStructure.of and PhiForcingDerived.of). LedgerFactorization.of calibrates this J on the positive reals under multiplication. The module interprets Podkletnov's 1992/1997 YBCO disk claim as either an ILG metric-weight modification or a spiral-field thrust, to be tested via flight falsifiers.
proof idea
The definition is a one-line placeholder returning the constant proposition True. It is intended to be expanded into an explicit membership test against phi-harmonic frequencies constructed from the upstream J-cost and spectral emergence structures.
why it matters
The definition supplies a concrete falsification handle for the resonant-speed banding reported in Podkletnov experiments, tying directly to the phi-resonant modes of the eight-tick octave and T5 J-uniqueness in the forcing chain. It supports the module's shielding-versus-thrust distinction and material-independence test. No downstream theorems currently reference it, leaving the predicate as an open interface for experimental closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.