pith. machine review for the scientific record. sign in
def definition def or abbrev high

generous_threshold

show as:
view Lean formalization →

Generous threshold sets the falsification cutoff at 5.0 for median chi-squared per degree of freedom when testing the ILG rotation curve model on the SPARC galaxy sample with all parameters locked to phi. Researchers checking zero-free-parameter predictions would cite this value to decide whether the model survives or is ruled out. The definition is a direct real-number assignment chosen above the RS-expected median near 2.75 to allow for observational systematics.

claimThe generous falsification threshold is the real number $5.0$, such that the ILG model is falsified whenever the median chi-squared per degree of freedom across the SPARC sample exceeds this value.

background

The SPARC falsifier module defines a concrete test for the ILG model of galaxy rotation curves. All parameters are locked to values derived from the golden ratio phi: alpha approximately 0.191, lag constant approximately 0.090, and stellar mass-to-light ratio equal to phi. The protocol computes chi-squared per degree of freedom for each galaxy using zero per-galaxy free parameters, then takes the median over the sample; the outcome is compared against the threshold.

proof idea

The declaration is a direct definition that assigns the constant value 5.0.

why it matters in Recognition Science

This constant supplies the bound used inside the definitions of ILG falsified and ILG passes, which together establish decidability of the falsification criterion. It implements the generous allowance in the SPARC protocol, connecting the gravity section to Recognition Science predictions obtained from the phi-ladder and eight-tick structure. The choice keeps the broader framework testable while the specific RS forecast of median near 2.75 can still be checked via the companion tight threshold.

scope and limits

formal statement (Lean)

  45def generous_threshold : ℝ := 5.0

proof body

Definition body.

  46
  47/-- The tight threshold matching the RS prediction (median ~ 2.75).
  48    If median chi2/dof > 3.0, the specific RS prediction is refuted
  49    (though ILG as a framework might survive with different parameters). -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.