N_tau_galactic
plain-language theorem explainer
N_tau_galactic assigns the numerical rung 142.4 for the galactic memory timescale tau star on the phi-ladder. Galaxy modelers and gravity phenomenologists cite this value when linking the acceleration scale a0 to radius r0 via the tau-star constraint. The definition is a direct constant assignment whose comment notes proximity to F_12 minus two.
Claim. $N_{τ,galactic}=142.4$ where the galactic memory timescale satisfies $τ^★=τ_0⋅ϕ^{N_{τ,galactic}}$.
background
The GravityParameters module classifies parameters as derived from phi, possessing an RS basis, or phenomenological. N_tau_galactic supplies the exponent for tau star, the memory timescale that links a0 and r0 through the relation τ★=√(2π r0/a0). The sibling definition N_galactic sets the integer approximation to 142, while F_12 is defined as 144. Upstream rung definitions in Constants and CellularAutomata establish the ladder indexing used throughout the module.
proof idea
This is a direct definition that assigns the real number 142.4. No lemmas or tactics are applied; the declaration consists of the constant together with a comment on its relation to F_12.
why it matters
The value feeds the downstream galactic_constraint defined as 2 N_tau_galactic minus N_r_galactic. It supplies the memory-timescale exponent required by the phi-ladder treatment of galactic gravity parameters. The accompanying comment flags a possible Fibonacci structure through F_12, consistent with self-similar features in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.