SPARCBestFit
plain-language theorem explainer
Packages the empirical SPARC best-fit triple (α, A, r₀) with uncertainties and χ²/dof as a typed record. Anyone comparing Recognition Science a priori ILG predictions to galaxy-rotation data cites this container. It is a plain structure definition with no proof obligations.
Claim. A data record holding the observed SPARC fit parameters: fractional exponent $\alpha_{\mathrm{obs}}$ with uncertainty $\sigma_\alpha$, amplitude $A_{\mathrm{obs}}$ with $\sigma_A$, scale radius $r_{0,\mathrm{obs}}$ (kpc) with $\sigma_{r_0}$, and the fit quality $\chi^2/\mathrm{dof}$. These are free-parameter outcomes from fitting 147 galaxies, not derived quantities.
background
The module addresses a gap in the discrete informational framework paper: SPARC fits treat $(A,\alpha,r_0)$ as free parameters, then note that best fits sit near golden-ratio candidates. That agreement is post-hoc. Recognition Science claims $\alpha$ and the amplitude are forced a priori from self-similarity of the memory kernel once the Recognition Composition Law fixes $J(x)=\frac12(x+x^{-1})-1$ and $\varphi$ is the unique self-similar scale.
This structure does not encode that derivation. It only holds the empirical side of the comparison: observed central values and uncertainties from paper §III.A / Eq. 29. Downstream, the concrete instance records $\alpha=0.19\pm0.02$, $A=0.38\pm0.04$, $r_0=12\pm3$ kpc. The a priori side lives in sibling objects that force $\alpha=(1-1/\varphi)/2$ and $C=\varphi^{-2}$.
proof idea
No proof. The declaration is a structure (record type) listing seven real fields. Field names and the doc-comment fix the scientific meaning; Lean imposes no equations among them. Instantiation happens in the sibling definition that fills the SPARC Eq. 29 numbers.
why it matters
Without a typed empirical target, the a priori prediction certificate cannot separate prediction from validation. This record is the observed half of that split. The sibling sparc_best_fit inhabits it with paper Eq. 29 values; comparison helpers (within-$n\sigma$ checks against $\varphi$-forced $\alpha$ and $C\approx\varphi^{-2}$) read those fields.
In the forcing chain, self-similarity after T5/T6 yields $\alpha\approx0.191$ and amplitude $\approx0.382$, which sit inside the SPARC error bars. The structure itself makes no claim about that match; it only supplies the data side so the certificate can assert that the prediction was stated before the fit numbers were consulted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.