null_holds_if_C_lag_small
plain-language theorem explainer
The theorem shows that if C_lag times ((T_dyn/τ0)^α minus one) is less than tolerance, then the absolute deviation of the ILG-predicted weight from unity falls below tolerance. Experimentalists and modelers testing rotating lab devices under Information-Limited Gravity would cite it to bound expected corrections when the coupling is small. The proof is a tactic sequence that unfolds the prediction and null definitions, proves non-negativity of the excess term via power inequalities, and reduces the absolute value directly to the input bound by环
Claim. Let $T_{dyn} > τ_0 > 0$, $α > 0$, $C_{lag} ≥ 0$, and tolerance $> 0$. If $C_{lag} ((T_{dyn}/τ_0)^α - 1) < $ tolerance, then the lab-scale weight prediction $w = 1 + C_{lag} ((T_{dyn}/τ_0)^α - 1)$ satisfies $|w - 1| < $ tolerance.
background
The Flight.GravityBridge module links the ILG weight kernel to flight and propulsion models. It formalizes lab-scale predictions for rotating devices and asks whether deviations from Newtonian weight appear when the dynamical timescale greatly exceeds the recognition tick. mkLabPrediction builds a LabScalePrediction record whose weight is defined as 1 + C_lag * (Real.rpow (T_dyn / τ0) α - 1). nullHypothesis is the proposition that the absolute deviation of this weight from 1 lies below a supplied tolerance. The module states the kernel explicitly as w_t(T_dyn, τ₀) = 1 + C_lag * ((T_dyn/τ₀)^α - 1) with τ₀ ≈ 7.3 fs and α ≈ 0.191, noting that T_rot ≫ τ₀ at laboratory scales yields w ≈ 1. The theorem depends on these two definitions together with arithmetic facts such as lt_trans for establishing positivity of the time ratio.
proof idea
The tactic proof first unfolds nullHypothesis and mkLabPrediction, then simplifies. It obtains positivity of the ratio T_dyn/τ0 via div_pos and lt_trans, shows the power term is at least one by one_le_rpow after one_le_div, and records non-negativity of the difference and product. A ring step rewrites the expression inside the absolute value to the product term; abs_of_nonneg then converts the target inequality into the supplied bound, which is discharged by exact.
why it matters
This theorem supplies the quantitative condition under which the null hypothesis holds for the ILG weight kernel at lab scales, directly supporting the module's claim that w ≈ 1 when C_lag is small. It thereby formalizes one of the key questions addressed by the Flight-Gravity Bridge: whether any deviation from Newtonian weight is detectable for rotating devices. In the Recognition Science framework the result connects to the eight-tick resonance structure imported from Gravity.EightTickResonance and to the overall forcing chain that fixes three spatial dimensions. The module records the associated falsifier: a nonzero measured thrust at lab scales would indicate either that ILG is incorrect or that a non-gravitational effect is present; the present bound gives the precise threshold for that test.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.