galactic_constraint
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.