alpha_locked
Recognition Science locks the ILG alpha parameter to the explicit algebraic value (1 minus phi inverse) divided by two. Galaxy dynamics researchers cite the definition when building zero-parameter models under the global-only policy for SPARC rotation curves. The definition is a direct one-line abbreviation of the expression derived from the phi fixed point.
claim$alpha_locked := (1 - phi^{-1})/2$
background
The ILG module supplies catalog-level constants for the Indisputable Local Gravity weight function. Phi denotes the golden ratio fixed point forced by the Recognition Science chain (T5 J-uniqueness and T6 self-similar fixed point). Upstream results in CouplingLockIn establish the same expression as the initial condition for RG flow at the lock-in scale ell0, while SPARCFalsifier records it as the locked alpha parameter approximately 0.191.
proof idea
This is a one-line definition that directly encodes the algebraic expression (1 - 1/phi)/2. No lemmas or tactics are invoked beyond substitution of the phi constant.
why it matters in Recognition Science
The definition supplies the alpha component of the parameters_from_phi theorem, which asserts that alpha_locked, upsilon_locked and clag_locked are all fixed by phi with zero free parameters. It enters the GlobalOnlyPolicy structure and the SPARCFalsifierCert used to certify that ILG passes falsification tests on galaxy data. The value closes the lock-in condition tied to the T5-T6 steps of the forcing chain and lies inside the framework's predicted alpha band.
scope and limits
- Does not assert numerical agreement with the measured fine-structure constant.
- Does not derive the expression from first principles inside this module.
- Does not specify the physical interpretation of the alpha parameter in the ILG weight function.
- Does not include error bounds or approximation statements.
formal statement (Lean)
7@[simp] noncomputable def alpha_locked : ℝ := (1 - 1 / phi) / 2
proof body
Definition body.
8