seven_beat_gap
plain-language theorem explainer
The declaration defines the relative mode gap between the valid 8-beat cycle and the invalid 7-beat cycle as the real number 1/8. Galaxy dynamics modelers using the ILG framework cite this gap to set the scale for suppression of modifications at high surface brightness. The value follows from a direct count of degrees of freedom: seven active modes in the 8-beat cycle versus six in the 7-beat cycle under neutrality, normalized by the cycle length.
Claim. The relative mode gap between the valid 8-beat cycle and the invalid 7-beat cycle is $1/8$.
background
The DerivedFactors module derives the morphology factor ξ and radial density profile n(r) to correct the ILG kernel's overprediction of rotation velocities in high surface brightness galaxies. It introduces the seven-beat leakage saturation hypothesis, where the 8-beat cycle (minimal valid period for three spatial dimensions) stiffens against leakage into 7-beat modes at high accelerations.
proof idea
The definition is a direct one-line assignment of the real number 1/8, obtained by dividing the mode difference (7 active minus 6 degrees of freedom) by the cycle length 8.
why it matters
This gap definition provides the numerical input for lock_stiffness, which in turn enters the expressions for xi_derived used in the theorems hsb_suppression_limit and lsb_unsuppressed_limit. It implements the saturation scale in the Seven-Beat Leakage Saturation hypothesis of the module, linking to the T7 eight-tick octave and D=3 from the forcing chain. It leaves open the question of whether high-density leakage into non-power-of-two modes occurs in real gravitational systems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.