nullHypothesis
plain-language theorem explainer
The null hypothesis asserts that the ILG-predicted weight for a lab-scale rotating device satisfies |w_predicted - 1| less than a supplied tolerance. Experimental physicists testing for deviations in lab gravity or propulsion setups would cite this predicate to frame null results. The declaration is introduced as a direct definition of that predicate on the LabScalePrediction structure.
Claim. Given a lab-scale prediction record $P$ with predicted weight $w$ obeying $w = 1 + C_{lag} ((T_{dyn}/τ_0)^α - 1)$ and tolerance $ε$, the null hypothesis is the proposition $|w - 1| < ε$.
background
The Flight-Gravity Bridge module connects the ILG weight kernel from Gravity.ILG to the Flight model. The kernel takes the form $w_t(T_{dyn}, τ_0) = 1 + C_{lag} ((T_{dyn}/τ_0)^α - 1)$, with $τ_0$ the recognition tick and $α ≈ 0.191$. LabScalePrediction is the structure that packages the dynamical time $T_{dyn}$, tick $τ_0$, exponent $α$, coupling $C_{lag}$, and the resulting $w_{predicted}$ that satisfies the kernel equation. Upstream, $C_{lag}$ is defined as $φ^{-5}$ in the EightTickResonance module.
proof idea
This is a definition that directly sets nullHypothesis P tolerance to the inequality |P.w_predicted - 1| < tolerance.
why it matters
This hypothesis_interface supplies the predicate used by the theorem null_holds_if_C_lag_small, which shows that C_lag below tolerance divided by the ratio term forces the null to hold. It encodes the RS prediction of undetectable deviation from w=1 at lab scales, consistent with the eight-tick octave and the requirement that C_lag stay small for solar-system agreement. It leaves open the precise numerical bound on C_lag needed in practice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.