alpha_locked
alpha_locked defines the locked alpha parameter for the ILG rotation-curve model as the constant alphaLock equal to (1 - 1/phi)/2. Researchers testing the SPARC falsifier with zero free parameters cite it to enforce the global-only policy. The declaration is a direct alias to the upstream constant definition.
claim$alpha_locked := (1 - phi^{-1})/2$
background
The SPARC Chi-Squared Falsifier module tests the ILG model on ~175 galaxies using only catalog-level constants derived from phi, with zero per-galaxy free parameters. The locked RS parameters are alpha_t = (1 - 1/phi)/2, C_lag = phi^{-5}, and Upsilon_star = phi. Upstream, Constants defines alphaLock as the canonical locked fine-structure constant alpha_lock = (1 - 1/phi)/2, with the algebraic identity 2 * alphaLock clearing the denominator.
proof idea
One-line wrapper that aliases alphaLock from the Constants module.
why it matters in Recognition Science
This supplies the alpha value required by GlobalOnlyPolicy, parameters_from_phi, and SPARCFalsifierCert in the same module. It anchors the zero-free-parameter falsification test of the ILG prediction against SPARC data, consistent with phi-derived constants and the Recognition framework's locked parameters.
scope and limits
- Does not compute chi-squared values or execute the falsification decision.
- Does not incorporate galaxy-specific kinematic data.
- Does not modify the numerical value of alphaLock.
- Does not introduce new hypotheses or axioms.
Lean usage
theorem params_from_phi : alpha_locked = (1 - 1 / phi) / 2 := by unfold alpha_locked; rflformal statement (Lean)
73noncomputable def alpha_locked : ℝ := alphaLock
proof body
Definition body.
74
75/-- The mass-to-light ratio is locked to phi ≈ 1.618. -/