hsb_suppression_limit
plain-language theorem explainer
The theorem establishes that the derived suppression factor for high surface brightness galaxies tends to zero as baryon acceleration tends to infinity. Researchers modeling galactic rotation curves with ILG modifications would cite it to recover Newtonian behavior in baryon-dominated systems. The proof unfolds the explicit rational form of the factor, verifies positivity of the saturation scale via linarith, and applies standard filter limit lemmas for the reciprocal of a diverging linear term.
Claim. Let $a_0 > 0$. Define the saturation scale by $a_*(a_0) := 8 a_0$. Let the suppression factor be given by $xi(g; a_0) := 1 / (1 + g / a_*(a_0))$. Then $lim_{g to +infty} xi(g; a_0) = 0$.
background
The module derives morphology and radial factors from seven-beat violation and scale-gate saturation. The eight-beat cycle is the minimal valid period for three spatial dimensions; at high energy density the eight-beat lock leaks into seven-beat modes, suppressing the ILG kernel. The saturation acceleration is defined as a_saturation a0 := lock_stiffness * a0 with lock_stiffness := 1 / seven_beat_gap, yielding the numerical factor 8. The suppression factor xi_derived is then the rational function 1 / (1 + g / a_saturation a0). Upstream definitions state that eight times the characteristic acceleration is required to break coherence and that the factor multiplies the ILG kernel amplitude.
proof idea
The tactic proof unfolds xi_derived to expose the rational expression. It proves positivity of a_saturation by unfolding the chain lock_stiffness, seven_beat_gap and applying linarith. It rewrites the term as the reciprocal of a linear function, then chains Filter.Tendsto.inv_tendsto_atTop, tendsto_atTop_add_const_left and atTop_mul_const (using the positive inverse of the saturation scale) to obtain the required limit at infinity.
why it matters
The result supplies the high-acceleration closure of the suppression mechanism needed to correct HSB overprediction in the ILG convolution plan. It rests on the eight-tick octave structure from the forcing chain and the seven-beat leakage hypothesis. The theorem pairs with the companion LSB unsuppressed limit in the same module; no further downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.