falsifierTriggered
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute numerical values for the discrepancy.
- Does not select or justify a particular threshold value.
- Does not incorporate non-gravitational contributions to thrust.
- Does not link to specific experimental protocols or data sets.
formal statement (Lean)
156def falsifierTriggered (f : GravityFalsifier) (threshold : ℝ) : Prop :=
proof body
Definition body.
157 f.discrepancy > threshold
158
159/-! ## RS-Specific Predictions -/
160
161/-- The RS prediction: C_lag is derived from φ, not a free parameter.
162 Specifically, C_lag = φ⁻⁵ ≈ 0.0902 in the time-kernel formula. -/