pith. machine review for the scientific record. sign in
def definition def or abbrev high

N_r_conjecture

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 314def N_r_conjecture : ℕ := N_tau_conjecture - rung_offset

proof body

Definition body.

 315

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.