pith. machine review for the scientific record. sign in
def

a_saturation

definition
show as:
view math explainer →
module
IndisputableMonolith.Gravity.DerivedFactors
domain
Gravity
line
65 · github
papers citing
none yet

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

A cached Ask Recognition explainer exists for this declaration.

open explainer

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`.