def
definition
lock_stiffness
show as:
view math explainer →
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
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 : ℝ) : ℝ :=