falsifierTriggered
plain-language theorem explainer
The predicate that a gravity falsifier is triggered holds precisely when the absolute discrepancy between measured thrust and the ILG-predicted thrust exceeds a supplied real-valued threshold. Experimental physicists testing the information-limited gravity model at laboratory scales would cite this predicate to decide whether a given measurement set falsifies the RS null prediction. The definition is a direct one-line comparison that reuses the discrepancy field already defined inside the gravity falsifier structure.
Claim. The predicate that a gravity falsifier structure is triggered by threshold $t$ holds if and only if the absolute difference between its measured thrust and its ILG-predicted thrust exceeds $t$.
background
In the Flight-Gravity Bridge module the ILG weight kernel takes the form $w_t(T_{dyn},τ_0)=1+C_{lag}((T_{dyn}/τ_0)^α-1)$, where $C_{lag}$ is fixed by $φ^{-5}$ and $α≈0.191$. A gravity falsifier structure records a measured thrust, the thrust predicted by this kernel, and their absolute difference as the discrepancy. The module addresses whether rotating lab devices exhibit any deviation from Newtonian weight at scales where the dynamical time greatly exceeds the recognition tick $τ_0≈7.3$ fs.
proof idea
The definition is a direct one-line wrapper that evaluates the inequality between the discrepancy field of the input gravity falsifier structure and the supplied threshold. No lemmas are applied; the body simply reuses the absolute-value computation already present in the structure definition.
why it matters
This definition completes the falsification interface for the RS-specific predictions in the Flight-Gravity Bridge. It operationalizes the claim that the ILG kernel, with $C_{lag}$ fixed by $φ$, yields no observable deviation at lab scales. The predicate supports any empirical program that compares rotating-device measurements against the eight-tick resonance schedule and touches the open question of whether non-gravitational effects could mimic a nonzero discrepancy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.