LabScalePrediction
plain-language theorem explainer
LabScalePrediction bundles the five real parameters of the ILG weight kernel together with the explicit equality that defines the predicted weight for a rotating lab device. Experimental groups comparing RS-derived gravity modifications to torsion-balance or Cavendish data would cite the structure when stating their expected deviation. The declaration is introduced as a plain structure definition whose only content is the five fields plus the single equality constraint on w_predicted.
Claim. A structure consists of real numbers $T_ {dyn}$, $τ_0$, $α$, $C_{lag}$, $w_{predicted}$ satisfying $w_{predicted}=1+C_{lag}((T_{dyn}/τ_0)^α-1)$.
background
The Flight.GravityBridge module links the ILG weight kernel from Gravity.ILG to the flight schedule. The kernel is written $w_t(T_{dyn},τ_0)=1+C_{lag}((T_{dyn}/τ_0)^α-1)$, where $τ_0$ is the recognition tick (fundamental time quantum), $α≈0.191$ is the ILG exponent, and $C_{lag}$ is the lag coupling. MODULE_DOC states that at lab scales $T_{dyn}≫τ_0$ by 10-15 orders of magnitude, so the structure formalizes the question whether any deviation from Newtonian weight appears.
proof idea
This is a structure definition that directly records the five fields and the equality constraint h_w; no lemmas or tactics are invoked.
why it matters
The structure is the input type for mkLabPrediction (which builds concrete instances) and for nullHypothesis (which tests whether |w_predicted-1| lies inside a tolerance). DOWNSTREAM_RESULTS show it also feeds optionB_bound_only and rsLabPrediction. The module doc-comment presents it as the formal carrier of the testable claim that w≈1 at laboratory scales, thereby closing one link between the forcing chain (T5-T8) and experiment. It leaves open whether C_lag must be taken scale-dependent to preserve the null result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.