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

paper2_N_galaxies

show as:
view Lean formalization →

This definition supplies the integer 127 as the galaxy count in the SPARC Q=1 sample used for Paper II falsification tests. Researchers working on ILG rotation curve predictions would reference it when computing median chi-squared statistics across the sample. The declaration is a direct constant assignment with no computation.

claimThe number of galaxies in the SPARC Q=1 sample for the Paper II analysis is 127.

background

The module formalizes a chi-squared falsifier for the ILG model against SPARC galaxy rotation curves. It locks RS parameters to phi-derived values: alpha_t = (1 - 1/phi)/2 ≈ 0.191, C_lag = phi^{-5} ≈ 0.090, Upsilon_star = phi ≈ 1.618. The protocol computes ILG predictions with zero free parameters per galaxy, then checks if the median chi2/dof exceeds a threshold (generous 5.0 or tight 3.0) to falsify the model.

proof idea

The declaration is a direct constant definition that assigns the natural number 127.

why it matters in Recognition Science

This supplies the fixed sample size required for the SPARC falsification protocol in the ILG model tests. It anchors the median statistic computation across the galaxy set using phi-locked parameters. The module connects to the broader Recognition Science framework through the eight-tick octave and J-cost selection, as referenced in the upstream StrongCP comparison of RS discrete selection versus axion continuous relaxation.

scope and limits

formal statement (Lean)

 116def paper2_N_galaxies : ℕ := 127

proof body

Definition body.

 117
 118/-- MOND simple-nu comparison: median 2.47, mean 4.65. -/

depends on (1)

Lean names referenced from this declaration's body.