LabScalePrediction
plain-language theorem explainer
LabScalePrediction packages the dynamical period, recognition tick, ILG exponent, lag coupling and resulting weight into a single record satisfying the explicit ILG formula. Experimental groups comparing rotating-device weight measurements to modified-gravity predictions would cite the structure when stating their observable. The declaration is a pure structure definition that directly encodes the five fields plus the equality constraint on w_predicted.
Claim. A record of real numbers $(T_ {dyn}, τ_0, α, C_{lag}, w_{predicted})$ obeying $w_{predicted}=1+C_{lag}((T_{dyn}/τ_0)^α-1)$, where $T_{dyn}$ is the device rotation period, $τ_0$ the fundamental recognition tick, $α$ the ILG exponent and $C_{lag}$ the lag coupling constant.
background
The Flight-Gravity Bridge module links the ILG weight kernel from Gravity.ILG to flight and propulsion models. The kernel is written $w_t(T_{dyn},τ_0)=1+C_{lag}((T_{dyn}/τ_0)^α-1)$ with $α≈0.191$ and $τ_0$ the RS time quantum. Upstream, Constants.tick supplies the definition $τ_0:=1$ in RS-native units while Gravity.EightTickResonance.C_lag supplies the concrete value $C_{lag}=φ^{-5}≈0.09$.
proof idea
This is a structure definition that directly encodes the five fields and the equality hypothesis h_w; no lemmas or tactics are applied.
why it matters
The structure supplies the data type consumed by mkLabPrediction, nullHypothesis and rsLabPrediction. It encodes the lab-scale claim in the module documentation that $w≈1$ unless $C_{lag}$ is large enough to produce a measurable deviation, thereby connecting the eight-tick resonance coupling to a concrete falsifiable test. The open question left open is whether the RS-native $C_{lag}$ must be suppressed at laboratory scales to recover the Newtonian limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.