pith. sign in
module module high

IndisputableMonolith.Gravity.DerivedFactors

show as:
view Lean formalization →

DerivedFactors computes galactic gravity quantities from the seven-beat mode gap in Recognition Science. It sets the relative gap at 1/8 between the valid 8-beat cycle (7 modes) and invalid 7-beat cycle (6 degrees of freedom), then builds stiffness and suppression limits from that ratio. Galaxy modelers cite these factors when linking Recognition Science to rotation-curve phenomenology. The module contains only definitions.

claimThe relative mode gap is $(7-6)/8 = 1/8$. Stiffness is taken as the inverse gap or $1 - 1/8$. Derived quantities include saturation limits and suppression factors for high-surface-brightness systems.

background

Constants supplies the RS time quantum τ₀ = 1 tick. GravityParameters states that each galactic parameter is either derived from φ, has an RS basis, or remains phenomenological. The present module supplies the derived subset by converting the eight-tick octave violation into numerical factors. The DOC_COMMENT records the explicit counting: eight-beat supplies seven active modes plus DC while seven-beat supplies six degrees of freedom under neutrality, producing the 1/8 gap.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the DerivedFactors re-exported by the Gravity facade. It closes the step that converts the seven-beat violation into HSB suppression and lock stiffness, feeding the parameterization bridge that links α to T_dyn/T_0 ratios. The GravityParameters doc-comment identifies these quantities as the mathematically proven subset of galactic parameters.

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)