def
definition
def or abbrev
a_saturation
show as:
view Lean formalization →
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). -/