galactic_constraint
The galactic constraint number is defined as twice the phi-ladder rung for galactic memory timescale minus the rung for characteristic galactic radius, yielding approximately 158.5. Researchers deriving galactic acceleration scales from Recognition Science parameters would cite this when linking tau-star to the a0-r0 relation. The definition is a direct arithmetic combination of two fixed real constants supplied by sibling declarations.
claimLet $N_τ$ be the φ-ladder rung for galactic memory timescale and $N_r$ the rung for characteristic galactic radius. The galactic constraint number is $2N_τ - N_r$.
background
The GravityParameters module derives phenomenological galactic gravity parameters from φ. Each parameter is classified as derived from φ, possessing an RS basis, or purely phenomenological. The rung $N_τ$ satisfies τ★ = τ₀ · φ^{N_τ} with N_τ ≈ 142.4; the rung $N_r$ satisfies r₀ = ℓ₀ · φ^{N_r} with N_r ≈ 126.3 and is constrained by the τ★ relation N_r = 2·N_τ - 158.5.
proof idea
The declaration is a direct definition performing the arithmetic 2 * N_tau_galactic - N_r_galactic on the two pre-defined real constants. No lemmas or tactics are invoked.
why it matters in Recognition Science
This supplies the numerical link between galactic radius and memory timescale rungs that sets the acceleration scale exponent. It appears in the module table of seven parameters and supports the linked a0, r0 via τ★ = √(2π r₀ / a₀). It touches the open question of whether the approximate value 158.5 admits a deeper Fibonacci or self-similar derivation.
scope and limits
- Does not derive the individual rung values from first principles.
- Does not compute the resulting acceleration scale.
- Does not prove consistency with observed galactic rotation curves.
- Does not connect to the eight-tick octave or spatial dimensions.
formal statement (Lean)
196def galactic_constraint : ℝ := 2 * N_tau_galactic - N_r_galactic
proof body
Definition body.
197
198/-- The φ-ladder rung for the galactic memory timescale (integer approximation). -/