n_derived
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive an explicit functional form for n(r) from the phi-ladder or J-cost.
- Does not implement the hypothesized resonance enhancement below the ScaleGate threshold.
- Does not quantify the LSB boost required to match observed rotation curves.
- Does not connect n to defectDist or Berry creation.
formal statement (Lean)
103def n_derived : ℝ := 1
proof body
Definition body.
104
105/-! ## 5. Theoretical Bounds -/
106
107/-- Theorem: HSB Suppression recovers Newtonian limit.
108 As baryon acceleration goes to infinity, the ILG modification vanishes. -/