Pith. sign in
module module high

IndisputableMonolith.Gravity.DerivedFactors

show as:
view Lean formalization →

DerivedFactors module computes gravity parameters from the relative mode gap between valid 8-beat and invalid 7-beat cycles. Researchers modeling HSB suppression in galactic rotation curves cite these factors. The module consists of definitions that translate the gap of 1/8 into stiffness and saturation limits.

claimThe relative mode gap between the 8-beat cycle (7 active modes) and 7-beat cycle (6 degrees of freedom) equals $(7-6)/8 = 1/8$, with stiffness taken as the inverse gap.

background

This module sits inside the Gravity domain and imports the RS time quantum $ au_0 = 1$ tick from Constants together with the parameter classification from GravityParameters. GravityParameters states that each parameter is either mathematically proven from $\phi$, has an RS basis matching observations, or remains phenomenological. The central definition is the mode gap arising from the neutrality constraint on 7 slots versus 7 active modes plus DC in the valid cycle.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies HSB suppression and related limits to the Gravity facade, which re-exports them for rotation-curve and ILG formalizations. It fills the step that derives suppression from SevenBeatViolation saturation and links directly to the eight-tick octave (T7) of the forcing chain.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (7)