LabScalePrediction
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not derive numerical values for α or C_lag.
- Does not evaluate the weight deviation for any specific device.
- Does not impose gravitational-binding conditions on T_dyn.
- Does not incorporate higher-order relativistic or quantum corrections.
formal statement (Lean)
80structure LabScalePrediction where
81 T_dyn : ℝ -- Rotation period
82 τ0 : ℝ -- Recognition tick
83 α : ℝ -- ILG exponent
84 C_lag : ℝ -- Coupling constant
85 w_predicted : ℝ -- Predicted weight
86 h_w : w_predicted = 1 + C_lag * (Real.rpow (T_dyn / τ0) α - 1)
87
88/-- Construct a lab-scale prediction for a given device. -/