n_derived
plain-language theorem explainer
The declaration fixes the derived radial profile factor at unity inside the ILG model for galaxy rotation curves. Workers on HSB overprediction and LSB underprediction would cite it when isolating the morphology suppression ξ from any radial correction. The definition is a direct constant assignment chosen to let the companion saturation function handle the leading systematic bias.
Claim. The derived radial exponent is defined by the constant value $n=1$.
background
The DerivedFactors module constructs the two correction functions required by the ILG kernel: the morphology factor ξ(g) that suppresses the modification at high baryon acceleration and the radial profile n(r) that is expected to rise at large radii where acceleration falls. The module starts from the SevenBeatViolation result that only an 8-beat cycle satisfies neutrality and completeness in three spatial dimensions; leakage into 7-beat modes at high density supplies the saturation scale a_sat that drives ξ toward zero.
proof idea
This is a direct definition that assigns the real number 1. No lemmas or tactics are invoked; the constant is chosen explicitly so that the suppression behavior resides entirely in the companion xi_derived definition.
why it matters
The definition supplies the default radial exponent that the xi_derived saturation function (1/(1 + g_baryon/a_sat)) multiplies against the ILG kernel. It therefore closes the minimal pair of derived factors needed to confront rotation-curve data. Within the Recognition framework it touches the T7 eight-tick octave and the ScaleGate saturation hypothesis, while leaving open the explicit resonance term tied to the λ_rec threshold that would replace the present placeholder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.