LabScalePrediction
plain-language theorem explainer
The structure packages the parameters and algebraic relation for the information-limited gravity weight of a rotating lab device. Experimentalists testing for non-Newtonian weight shifts at laboratory scales would cite the packaged formula to state a concrete prediction. The declaration is a structure definition that directly records the ILG kernel without lemmas or computation.
Claim. A tuple consisting of dynamical period $T$, recognition tick $τ_0$, exponent $α$, coupling $C$, and weight $w$ satisfying $w = 1 + C((T/τ_0)^α - 1)$.
background
The Flight.GravityBridge module links the ILG weight kernel to the propulsion model. The kernel takes the explicit form $w_t(T, τ_0) = 1 + C((T/τ_0)^α - 1)$, where $τ_0$ is the fundamental recognition tick (Constants.tick), $α ≈ 0.191$ is the ILG exponent, and $C$ is the lag coupling. Upstream, EightTickResonance.C_lag supplies the RS-native value $C = φ^{-5} ≈ 0.09$, while Constants.tick defines the time quantum as 1 in RS units.
proof idea
This is a structure definition that directly encodes the five fields together with the equality constraint taken from the ILG weight kernel.
why it matters
The structure supplies the data type consumed by mkLabPrediction (to build instances), nullHypothesis (to test closeness to Newtonian weight), and rsLabPrediction (to instantiate the RS values). It formalizes the lab-scale test case inside the Flight-Gravity Bridge, directly addressing the module question of whether ILG produces measurable deviation when $T ≫ τ_0$. It leaves open whether $C$ remains scale-independent or vanishes at laboratory energies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.