a_saturation
The definition sets the saturation acceleration a_sat to eight times the base scale a0, where the prefactor encodes the stiffness of the eight-beat lock. Galaxy rotation-curve modelers cite it when building the suppression factor that restores the Newtonian limit at high baryon accelerations. It is a direct one-line abbreviation that multiplies the precomputed lock stiffness by the input a0.
claimDefine the saturation acceleration by $a_0$ as $a_0 = 8 a_0$, where $a_0$ is the characteristic acceleration scale and the factor 8 is the stiffness of the eight-beat lock against seven-beat leakage.
background
The DerivedFactors module constructs morphology corrections for the ILG kernel to fix overprediction in high-surface-brightness galaxies. It rests on the SevenBeatViolation result that an eight-beat cycle is the minimal valid period for three spatial dimensions, with the seven-beat gap supplying the leakage scale. The lock stiffness is defined upstream as the reciprocal of that gap, yielding the constant value 8.
proof idea
The declaration is a one-line abbreviation that multiplies the lock_stiffness constant by the input parameter a0.
why it matters in Recognition Science
This definition supplies the critical scale that enters the derived suppression factor ξ(g) = 1 / (1 + g / a_sat). It is invoked by the theorems establishing the high-acceleration Newtonian limit and the low-acceleration unsuppressed limit. Within the Recognition framework it realizes the eight-tick octave by quantifying the stiffness against seven-beat leakage, thereby closing the morphology correction needed for consistency with observed galaxy rotation curves.
scope and limits
- Does not derive the numerical value of the seven-beat gap from the forcing chain.
- Does not prove that the saturation form 1/(1+x) is the unique choice compatible with the Recognition Composition Law.
- Does not address radial dependence or higher-order corrections to the suppression.
formal statement (Lean)
65def a_saturation (a0 : ℝ) : ℝ := lock_stiffness * a0
proof body
Definition body.
66
67/-! ## 3. Derived Suppression Factor ξ -/
68
69/-- The HSB suppression factor ξ(g).
70 This factor multiplies the ILG kernel amplitude.
71
72 Behavior:
73 - Low g (<< a_sat): ξ ≈ 1 (Full ILG effect)
74 - High g (>> a_sat): ξ -> 0 (Newtonian recovery)
75
76 Functional form: Standard saturation `1 / (1 + x)`.
77 Argument x: `g / a_sat`.
78
79 Formula: ξ(g) = 1 / (1 + g / (8*a0))
80
81 This provides the necessary suppression for HSB galaxies (where g is high)
82 while maintaining the ILG boost for LSB galaxies (where g is low). -/