N_tau_conjecture_eq_142
plain-language theorem explainer
The equality fixes the conjectured galactic timescale rung at exactly 142 via the definition N_τ = F_12 - 2. Modelers of galactic rotation curves and dark-matter alternatives in Recognition Science cite this value when calibrating the phi-ladder for a0 and r0. The proof is a one-line native decision that evaluates the arithmetic expression directly.
Claim. $N_τ = 142$, where $N_τ := F_{12} - 2$ and $F_{12}$ is the twelfth Fibonacci number.
background
The GravityParameters module derives seven galactic gravity parameters from φ, classifying each as derived, RS-basis, or phenomenological. N_τ appears as the conjectured galactic timescale rung with the explicit definition N_τ = F_12 - 2. The module links this rung to the observable pair a0, r0 through the relation τ★ = √(2π r0 / a0) and records the axiom a0_phi_ladder_formula as already proved.
proof idea
The proof is a one-line term that applies native_decide to the definition N_tau_conjecture := F_12 - 2.
why it matters
This declaration supplies the concrete integer required for the galactic timescale rung inside the seven-parameter table. It supports the linked a0-r0 calibration and sits downstream of the phi-ladder and eight-tick octave steps in the Recognition framework. No downstream theorems yet reference the equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.