mkLabPrediction
plain-language theorem explainer
mkLabPrediction constructs a LabScalePrediction record by inserting dynamical time T_dyn, recognition tick τ0, ILG exponent α, and lag constant C_lag into the weight formula. Experimental groups testing rotating devices for non-Newtonian weight shifts would call this constructor to obtain a concrete w_predicted value for null-hypothesis checks. The definition is a direct structure literal whose weight equality is discharged by reflexivity.
Claim. Given real numbers $T_{dyn}$, $τ_0$, $α$, and $C_{lag}$, the lab-scale prediction is the record whose fields are $T_{dyn}$, $τ_0$, $α$, $C_{lag}$, predicted weight $1 + C_{lag}((T_{dyn}/τ_0)^α - 1)$, and the reflexivity proof that the weight equals that expression.
background
The Flight.GravityBridge module connects the ILG weight kernel from Gravity.ILG to rotating-device models. Its central formula is $w_t(T_{dyn}, τ_0) = 1 + C_{lag}((T_{dyn}/τ_0)^α - 1)$, with $τ_0$ the fundamental tick (Constants.tick), $α ≈ 0.191$, and $C_{lag}$ small to match solar-system tests. LabScalePrediction packages these inputs with the computed weight and its defining equation. Upstream results supply the tick as the RS time quantum and the eight-tick phase function.
proof idea
This is a direct record constructor. It assigns the four real parameters to the corresponding fields, evaluates w_predicted with Real.rpow, and closes the equality h_w by rfl.
why it matters
The definition supplies the concrete instances required by the downstream theorems null_holds_if_C_lag_small and rsLabPrediction. It operationalizes the module claim that w ≈ 1 at lab scales when C_lag is small, while exposing a large deviation under the RS-native choice C_lag = φ^{-5}. It thereby links the eight-tick schedule to testable ILG predictions at typical laboratory periods.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.