GravityFalsifier
plain-language theorem explainer
GravityFalsifier records a measured thrust, the ILG-predicted thrust, and their absolute difference to capture a potential lab-scale deviation from the predicted null result. Experimental groups testing rotating devices would cite the structure when reporting nonzero thrust that could falsify the ILG weight kernel or indicate an unaccounted force. The definition is a direct record constructor that defaults the discrepancy field to the absolute difference of the two thrust values.
Claim. A record with fields $m, p, d$ where $m$ is measured thrust, $p$ is the thrust predicted by the ILG weight kernel, and $d = |m - p|$.
background
The module connects the ILG weight kernel $w_t(T_{dyn}, τ_0) = 1 + C_{lag} ((T_{dyn}/τ_0)^α - 1)$ from Gravity.ILG to the Flight propulsion model. Here $τ_0 ≈ 7.3$ fs is the recognition tick, $α = (1 - φ^{-1})/2 ≈ 0.191$, and $C_{lag}$ is a small coupling constant. For a rotating lab device the dynamical time is identified with the rotation period, which exceeds $τ_0$ by 10-15 orders of magnitude and forces the prediction $w ≈ 1$ (null result) at laboratory scales.
proof idea
One-line definition of a structure whose three fields are measured_thrust and predicted_thrust_from_ILG supplied by the user, with discrepancy defaulted to the absolute difference of those two real numbers.
why it matters
The structure supplies the input type for falsifierTriggered, which returns true precisely when the discrepancy exceeds a chosen threshold. It therefore implements the module's RS claim that any nonzero lab-scale thrust either falsifies the ILG kernel or signals a non-gravitational effect, closing the link from the phi-derived constants and eight-tick schedule to experimental testability. The downstream note that C_lag is derived from φ rather than free reinforces that the falsifier tests a parameter-free prediction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.