pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Gravity.DerivedFactors

show as:
view Lean formalization →

DerivedFactors computes RS-native gravity parameters from the eight-tick structure, notably the seven-beat mode gap stiffness and HSB suppression limits. Galaxy modelers working on flat rotation curves or information-limited gravity cite these expressions when linking phi-ladder results to phenomenological fits. The module assembles algebraic definitions from upstream constants and GravityParameters without internal proofs.

claimThe module defines the relative mode gap between the valid 8-beat cycle (7 active modes plus DC) and invalid 7-beat cycle (6 degrees of freedom under neutrality) as $(7-6)/8 = 1/8$, with inverse gap $1 - 1/8$ serving as stiffness factor, plus derived quantities lock_stiffness, a_saturation, xi_derived, n_derived, hsb_suppression_limit, and lsb_unsuppressed_limit.

background

This module sits in the Gravity domain and imports the RS time quantum tau_0 = 1 tick from Constants together with phi-derived galactic parameters from GravityParameters. The latter classifies each parameter as mathematically derived from phi, possessing an RS basis, or purely phenomenological. The supplied DOC_COMMENT introduces the mode gap: 8-beat has 7 active modes while 7-beat has 6 degrees of freedom from the neutrality constraint on 7 slots, so relative gap equals 1/8; the inverse is proposed as stiffness via p_steepness logic.

proof idea

This is a definition module, no proofs. It assembles the sibling definitions seven_beat_gap, lock_stiffness, a_saturation, xi_derived, n_derived, hsb_suppression_limit, and lsb_unsuppressed_limit through direct algebraic expressions based on the mode gap and upstream phi-ladder quantities.

why it matters in Recognition Science

DerivedFactors supplies the HSB suppression component re-exported by the Gravity facade for use in Rotation and ILG formalizations. It fills the derived-factors slot in the Recognition Science gravity derivation, connecting the eight-tick octave (T7) and phi fixed point (T6) to saturation effects on galactic scales.

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)