lsb_unsuppressed_limit
plain-language theorem explainer
The theorem shows that the derived suppression factor for low-surface-brightness systems tends to 1 as the acceleration parameter g approaches zero, for any positive characteristic scale a0. Galaxy dynamicists using the Recognition Science ILG kernel would cite the result to recover Newtonian limits at low accelerations. The proof is a term-mode argument that rewrites the target value via field simplification on the saturation definitions and invokes continuity of division and addition under the neighborhood filter.
Claim. Let $a_0 > 0$. Then $lim_{g→0} ξ(g,a_0)=1$, where $ξ(g,a_0)$ is the suppression factor $1/(1+g/a_{sat})$ with saturation scale $a_{sat}=8a_0$ obtained from the eight-to-seven beat gap.
background
The module derives morphology and radial factors to correct ILG kernel overprediction in high-surface-brightness galaxies. It posits that the eight-beat lock saturates via leakage into seven-beat modes at high acceleration, suppressing the ILG modification. The seven-beat gap is defined as the relative mode difference 1/8; lock stiffness is its reciprocal 8; saturation acceleration is then stiffness times the input scale a0. The suppression factor xi_derived is constructed directly from these quantities as the quotient that multiplies the ILG amplitude. Upstream constants supply the dimensionless bridge K as phi to the power 1/2, though the present limit uses only the saturation scale.
proof idea
Unfold xi_derived, then rewrite the target neighborhood point 1 as the quotient 1/(1+0/a_saturation a0) by field_simp on a_saturation, lock_stiffness and seven_beat_gap together with linarith. Apply Filter.Tendsto.div, splitting into constant numerator and an added denominator whose own limit is obtained by another Tendsto.div of the identity map by a constant; the nonzero-denominator side conditions are discharged by linarith on the positive stiffness and a0.
why it matters
The result supplies the low-acceleration anchor for the suppression factor required by the HSB overprediction diagnosis in the ILG convolution plan. It rests on the seven-beat violation and ScaleGate saturation hypotheses stated in the module. No downstream theorems are recorded yet, but the limit is a prerequisite for any consistent radial morphology derivation that must recover Newtonian gravity in LSB regimes. It touches the open question of whether the numerical stiffness 8 is the unique choice compatible with the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.