pith. machine review for the scientific record. sign in
def definition def or abbrev high

N_galactic

show as:
view Lean formalization →

N_galactic assigns the integer 142 as the discrete rung on the φ-ladder for the galactic memory timescale ratio. Researchers modeling galactic dynamics from Recognition Science first principles cite this constant when discretizing log_φ(τ★/τ₀) for rotation-curve calculations. The definition is a direct numerical assignment with no computation or proof steps.

claimLet $N$ denote the integer approximation to the base-φ logarithm of the galactic-to-reference timescale ratio, with $N = 142$.

background

The Gravity Parameters module classifies each galactic gravity parameter by its connection to φ: derived, RS-basis, or phenomenological. The φ-ladder supplies discrete rungs via powers of φ for masses and timescales, with the exact ratio defined upstream as log_φ(τ★/τ₀) in the GalacticTimescale module. The module_doc states that a₀ and r₀ are linked by τ★ = √(2π r₀ / a₀), and the integer rung closes the discretization step for downstream bounds.

proof idea

Direct constant definition. No lemmas or tactics are applied; the body is the literal integer 142.

why it matters in Recognition Science

The definition supplies the fixed rung consumed by galactic_status, the N_galactic_approx theorem (140 < N < 145), and A_amplitude_bounds. It instantiates the φ-ladder rung for galactic timescales, linking the T5 J-uniqueness and T7 eight-tick octave to observable parameters while satisfying the module's derived-parameter column.

scope and limits

formal statement (Lean)

 199def N_galactic : ℝ := 142

proof body

Definition body.

 200
 201/-- The timescale constraint linking a₀ and r₀.
 202    Given τ★ and r₀, the acceleration scale is forced. -/

used by (4)

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

depends on (7)

Lean names referenced from this declaration's body.