rs_lab_prediction_value
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove the numerical value of w; only states the bounding predicate.
- Does not derive the ILG kernel or the value of C_lag from the forcing chain.
- Does not specify experimental protocols or error budgets for measuring w.
- Does not address non-rotating or gravitationally bound systems.
formal statement (Lean)
181def rs_lab_prediction_value : Prop :=
proof body
Definition body.
182 25 < rsLabPrediction.w_predicted ∧ rsLabPrediction.w_predicted < 35
183
184/-! ## Interpretation Options -/
185
186/-- Option A: ILG applies at lab scales → large deviation → testable. -/