N_r_conjecture
plain-language theorem explainer
N_r_conjecture defines the conjectured galactic radius rung by subtracting the 16-rung offset from the conjectured galactic timescale rung N_τ. Researchers modeling galactic rotation curves in Recognition Science cite it to connect temporal and spatial scales on the phi-ladder. It is realized as a direct arithmetic subtraction from the two upstream definitions.
Claim. The conjectured galactic radius rung satisfies $N_r = N_τ - 16$, where $N_τ$ is the conjectured galactic timescale rung given by $N_τ = F_{12} - 2$.
background
The module derives phenomenological galactic gravity parameters from the golden ratio φ. N_τ is the conjectured galactic timescale rung defined as F_12 - 2 = 142. The rung offset is defined as 16, identified as 2^4 = 4², the second non-trivial perfect square that separates timescale and radius rungs on the phi-ladder.
proof idea
The definition is a one-line wrapper that subtracts rung_offset from N_tau_conjecture.
why it matters
This definition supplies the value used by the theorem N_r_conjecture_eq_126 that establishes N_r = 126 and by the rung_relationship theorem that restates the subtraction. It completes the spatial scale entry in the gravity parameters table derived from φ, linking to the phi-ladder and the eight-tick octave structure via the power-of-two offset. It leaves open empirical validation of the F_12 conjecture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.