def
definition
a_saturation
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Gravity.DerivedFactors on GitHub at line 65.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
62
63 Physical intuition: You need 8x the characteristic acceleration to "break"
64 the 8-beat coherence and suppress the ILG effect. -/
65def a_saturation (a0 : ℝ) : ℝ := lock_stiffness * a0
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). -/
83def xi_derived (g_baryon : ℝ) (a0 : ℝ) : ℝ :=
84 1 / (1 + g_baryon / (a_saturation a0))
85
86/-! ## 4. Radial Profile n(r) -/
87
88/-- The radial profile `n(r)` was calibrated to increase at large radii.
89 From a derived perspective, this is likely the inverse of the suppression.
90
91 As r increases, acceleration g drops.
92 So ξ(g) increases towards 1.
93
94 If `n(r)` is meant to provide *extra* boost at very low density (LSB underprediction),
95 it might be a "Resonance" term that kicks in when `g < a0`.