nullHypothesis
nullHypothesis encodes the predicate that a lab-scale ILG prediction satisfies |w_predicted - 1| < tolerance. Experimental groups running rotating-device tests at periods 10^12-10^15 times the recognition tick would cite it to state the expected null result. It is realized as a direct definition on the w_predicted field of LabScalePrediction.
claimLet $P$ be a structure containing dynamical time $T_$, recognition tick $τ_0$, exponent $α$, lag $C_$, and predicted weight $w = 1 + C_ ((T_/τ_0)^α - 1)$. The null hypothesis holds when $|w - 1| < ε$ for tolerance $ε$.
background
The Flight.GravityBridge module links the ILG weight kernel $w_t(T_ , τ_0) = 1 + C_ ((T_/τ_0)^α - 1)$ to rotating-device models. Here $τ_0$ is the recognition tick, $α ≈ 0.191$, and $C_$ is the lag coupling. LabScalePrediction packages the four inputs together with the computed $w_predicted$ that satisfies the kernel equation by construction.
proof idea
One-line definition that directly compares the absolute deviation of the stored w_predicted field from 1 against the supplied tolerance. No lemmas or tactics are invoked; the body is the predicate itself.
why it matters in Recognition Science
It supplies the hypothesis interface discharged by the downstream theorem null_holds_if_C_lag_small, which proves the predicate holds once $C_ < ε / ((T_/τ_0)^α - 1)$. This supports the RS claim of negligible lab-scale deviation, consistent with the eight-tick octave and the small value $C_ = φ^{-5}$ from EightTickResonance. It leaves open the empirical determination of $C_$ from precision weight measurements.
scope and limits
- Does not assign a numerical value to $C_$.
- Does not prove the null holds for any specific device.
- Does not incorporate measurement uncertainty beyond the tolerance parameter.
- Does not apply outside the lab-scale regime where $T_ >> τ_0$.
falsifier
A measured weight deviation |w - 1| ≥ tolerance on a device with known T_, τ_0, α would falsify the hypothesis for that tolerance.
Lean usage
nullHypothesis (mkLabPrediction T_dyn τ0 α C_lag) toleranceformal statement (Lean)
123def nullHypothesis (P : LabScalePrediction) (tolerance : ℝ) : Prop :=
proof body
Definition body.
124 |P.w_predicted - 1| < tolerance
125
126/-- If C_lag < tolerance / (ratio^α - 1), the null hypothesis holds. -/