N_r_galactic
plain-language theorem explainer
N_r_galactic assigns the numerical exponent 126.3 to the phi-ladder for the characteristic galactic radius r0. Galaxy modelers in Recognition Science cite this constant to enforce the tau-star relation that fixes the acceleration scale exponent. The definition is a direct numerical assignment satisfying N_r = 2 N_tau_galactic - 158.5.
Claim. The exponent $N_r$ on the phi-ladder for the characteristic galactic radius satisfies $r_0 = ell_0 phi^{N_r}$ with $N_r = 126.3$, subject to the constraint $N_r = 2 N_tau - 158.5$.
background
The GravityParameters module derives galactic gravity parameters from the Recognition Science phi framework. Parameters are classified as derived from phi, having RS basis, or phenomenological, with a0_phi_ladder_formula listed as a proven theorem. The phi-ladder is supplied by the upstream scale definition scale(k) := phi^k from LargeScaleStructureFromRS. N_r_galactic sets the radius rung, paired with N_tau_galactic at 142.4 for the memory timescale tau-star = tau0 phi to that power.
proof idea
One-line definition that directly assigns the constant 126.3 to the galactic radius exponent on the phi-ladder.
why it matters
This definition supplies the radius exponent to galactic_constraint, which computes 2 N_tau_galactic - N_r_galactic to set the acceleration scale. It implements the tau-star relation from the doc-comment and connects to the proven a0_phi_ladder_formula theorem. The value touches the phi-ladder structure for mass formulas and the eight-tick octave, leaving the precise 158.5 offset as an open calibration point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.