rs_lab_prediction_value
plain-language theorem explainer
The definition asserts that the RS-predicted lab weight w satisfies 25 < w < 35. Experimental groups testing ILG deviations in rotating devices would cite this interval as the concrete forecast under standard constants. It is obtained by direct substitution of the w_predicted field from rsLabPrediction into the bounding predicate.
Claim. Let $w$ be the weight predicted by the ILG kernel $w_t = 1 + C_{lag} ((T_{dyn}/τ_0)^α - 1)$ at typical laboratory period $T_{dyn}$ and recognition constants. Then $25 < w < 35$.
background
The Flight.GravityBridge module links the ILG weight kernel from Gravity.ILG to the Flight propulsion model. The kernel is $w_t(T_{dyn}, τ_0) = 1 + C_{lag} ((T_{dyn}/τ_0)^α - 1)$ with $τ_0 ≈ 7.3$ fs, $α ≈ 0.191$, and $C_{lag} = φ^{-5}$. rsLabPrediction constructs the concrete instance using typicalLabPeriod_seconds, tau0_seconds, ilg_alpha and C_lag_RS, yielding $w ≈ 29$ as shown in its doc-comment: 'w - 1 = φ^{-5} * ((0.06 / 7.3e-15)^0.191 - 1) ≈ 28'. The upstream A definitions supply the active-edge count per tick used in the underlying mass and actualization steps.
proof idea
This is a direct definition of the proposition as the conjunction of two strict inequalities on the w_predicted field of rsLabPrediction. No additional lemmas are applied; the body simply evaluates the numeric interval after the structure is built by mkLabPrediction.
why it matters
The definition encodes the central falsifiable claim of the Flight-Gravity Bridge: a large deviation from Newtonian w=1 when the ILG kernel is applied at lab scales. It formalizes the prediction computed in rsLabPrediction and sits at the intersection of the eight-tick octave and the ILG weight kernel. The result leaves open the three interpretation options listed in the module doc-comment: direct test, suppression of C_lag, or mismatch between T_dyn and T_rot.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.