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

lock_stiffness

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Gravity.DerivedFactors on GitHub at line 53.

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

  50
  51/-- The stiffness of the 8-beat lock against 7-beat leakage.
  52    Stiffness = 1 / Gap = 8. -/
  53def lock_stiffness : ℝ := 1 / seven_beat_gap
  54
  55/-! ## 2. Saturation Acceleration Scale -/
  56
  57/-- The acceleration scale where "saturation" (leakage) begins.
  58    Hypothesis: The critical acceleration `a_sat` is the characteristic scale `a0`
  59    boosted by the stiffness of the 8-beat lock.
  60
  61    a_sat = stiffness * a0 = 8 * a0.
  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 : ℝ) : ℝ :=