generous_threshold
plain-language theorem explainer
The generous_threshold definition supplies the constant 5.0 as the cutoff value for median chi-squared per degree of freedom when testing the ILG rotation-curve model on the SPARC galaxy sample. Observers comparing zero-free-parameter RS predictions against real rotation curves would cite this number to decide whether the model survives or is falsified. The declaration is a direct constant assignment.
Claim. The generous falsification threshold equals $5.0$, so that the ILG model is falsified if the median chi-squared per degree of freedom across the SPARC sample exceeds this value.
background
The module formalizes a falsification test for the ILG rotation-curve model. All RS parameters (alpha_t = (1 - 1/phi)/2, C_lag = phi^(-5), Upsilon_star = phi) are locked with zero per-galaxy free parameters. For each of the ~175 SPARC galaxies one computes chi2/dof of the predicted curve, then takes the median; the model is falsified if this median exceeds the threshold. The module documentation states that the underlying theory predicts a median near 2.75, so the generous threshold of 5.0 provides buffer for systematic errors while the tight threshold of 3.0 tests the specific prediction.
proof idea
One-line definition that directly assigns the real constant 5.0.
why it matters
The constant is the anchor for the sibling definitions ILG_falsified and ILG_passes, which together enable the decidability theorem falsification_decidable. It implements the generous arm of the SPARC falsification protocol described in the module documentation, where the RS parameter lock from phi is used to generate the zero-free-parameter predictions. The choice of 5.0 rather than the predicted 2.75 explicitly allows for unmodeled systematics while still providing a concrete falsification criterion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.