optionB_bound_only
plain-language theorem explainer
Option B encodes that ILG weight deviations apply solely to gravitationally bound systems. For any lab device whose dynamical time lies outside the finite interval (0, 10^10), the predicted weight is fixed at unity. Researchers testing null results for rotating lab apparatus would cite the definition when stating the bound-system restriction. It is introduced as a direct universal quantification over the lab-scale prediction structure.
Claim. For every lab-scale prediction structure recording dynamical time $T_ {dyn}$, recognition tick $τ_0$, exponent $α$, lag coupling $C_{lag}$ and predicted weight $w$, if it is not the case that $0 < T_{dyn} < 10^{10}$, then $w = 1$.
background
LabScalePrediction records the dynamical time $T_{dyn}$ of a rotating device together with the recognition tick $τ_0$, the ILG exponent $α ≈ 0.191$, the lag coupling $C_{lag}$ and the resulting weight $w_{predicted}$. The module states the ILG kernel explicitly as $w_t(T_{dyn}, τ_0) = 1 + C_{lag} ((T_{dyn}/τ_0)^α - 1)$. Upstream, $C_{lag}$ is supplied by EightTickResonance as $φ^{-5}$. The local setting is the Flight-Gravity Bridge that asks whether any deviation from Newtonian weight appears for lab-scale rotation periods.
proof idea
The definition is the literal statement of the universal quantification: whenever the dynamical-time bound fails, the weight field is required to equal 1. No lemmas or tactics are invoked; the body is the direct encoding of the option-B hypothesis.
why it matters
The definition isolates Option B inside the module's RS claim structure, restricting ILG modifications to bound systems and thereby predicting a null result ($w=1$) for typical lab rotation. It supplies one of the three explicit falsifiers listed in the module doc-comment and links to the eight-tick resonance through the supplied value of $C_{lag}$. No downstream theorems yet consume it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.