hsb_suppression_limit
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the stiffness constant 8 from first principles.
- Does not treat the low-acceleration regime or LSB galaxies.
- Does not incorporate observational bounds on the saturation scale.
- Does not establish uniqueness of the rational suppression form.
formal statement (Lean)
109theorem hsb_suppression_limit (a0 : ℝ) (ha0 : a0 > 0) :
110 Filter.Tendsto (fun g => xi_derived g a0) Filter.atTop (nhds 0) := by
proof body
Tactic-mode proof.
111 unfold xi_derived
112 have h_sat_pos : a_saturation a0 > 0 := by
113 unfold a_saturation lock_stiffness seven_beat_gap
114 linarith
115 -- Rewrite 1/(1+x) as (1+x)⁻¹ to match inv_tendsto_atTop
116 rw [show (fun g => 1 / (1 + g / a_saturation a0)) = (fun g => (1 + g / a_saturation a0)⁻¹) by ext; simp]
117 apply Filter.Tendsto.inv_tendsto_atTop
118 apply Filter.tendsto_atTop_add_const_left
119 apply Filter.Tendsto.atTop_mul_const (inv_pos.mpr h_sat_pos) Filter.tendsto_id
120
121/-- Theorem: LSB Limit is Unsuppressed.
122 As baryon acceleration goes to zero, the suppression factor goes to 1. -/