rsLabPrediction
plain-language theorem explainer
rsLabPrediction assembles the concrete lab-scale weight deviation from the ILG kernel using RS-derived constants. Experimentalists testing rotating devices for non-Newtonian effects would cite this value. The definition is a direct application of the mkLabPrediction constructor to the typical lab period, recognition tick, ILG exponent, and phi-derived coupling constant.
Claim. The lab-scale prediction is the structure with dynamical time $T_0 = 0.06$, recognition tick $τ_0 = 7.3×10^{-15}$, exponent $α = (1-φ^{-1})/2$, coupling $C_λ = φ^{-5}$, and predicted weight $w = 1 + C_λ ((T_0/τ_0)^α - 1)$.
background
LabScalePrediction is the structure holding dynamical time $T_dyn$, recognition tick $τ_0$, ILG exponent $α$, coupling $C_lag$, and the weight $w_predicted$ obeying $w_predicted = 1 + C_lag ((T_dyn/τ_0)^α - 1)$. The module links the ILG weight kernel to the Flight model and asks whether rotating lab devices deviate from Newtonian weight $w=1$. Upstream results supply $C_lag_RS = φ^{-5}$, $ilg_alpha = (1 - φ^{-1})/2$, $tau0_seconds ≈ 7.3 fs$, and $typicalLabPeriod_seconds = 0.06 s$.
proof idea
This is a one-line wrapper that applies mkLabPrediction to typicalLabPeriod_seconds, tau0_seconds, ilg_alpha, and C_lag_RS.
why it matters
It supplies the numerical prediction that feeds optionA_testable and rs_lab_prediction_value. With $C_lag = φ^{-5}$ the deviation reaches order 28, offering a falsifiable test or evidence that the coupling is suppressed at lab scales or that $T_dyn ≠ T_rot$ for non-bound systems. It realizes the module's claim structure for the ILG kernel at laboratory scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.