a_saturation
plain-language theorem explainer
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.
Claim. Define 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.