phiRung_zero
The phi-rung index r(n) satisfies r(0) = 0 by convention on the zero factorization. Researchers building the Recognition Theta series cite this base case to anchor the completely additive rung function before extending it over positive integers. The proof is a direct term reduction that unfolds the definition and simplifies against the zero factorization fact.
claimLet $r(n)$ denote the phi-rung index, the completely additive arithmetic function satisfying $r(p) = ⌊log_φ p⌋$ for each prime $p$. Then $r(0) = 0$.
background
The module defines the Recognition Theta function as the candidate completion of the cost theta function Θ_J(t) = Σ e^{-t c(n)} that incorporates the 8-tick character (T7) and the phi-ladder weight (T6) to support a modular identity under t ↦ 1/t. The phi-rung index r(n) is introduced as the completely additive function with r(p) = ⌊log_φ p⌋ for primes; the present theorem supplies its conventional value at zero, where the factorization is the zero finsupp. Upstream results supply related rung definitions in mass and scaling contexts, including the phi-ladder scaling phi^n and sector-specific rung maps, but the number-theoretic r(n) is local to this arithmetic development.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of phiRung and then applies simp with the fact that the factorization of zero is the zero finsupp.
why it matters in Recognition Science
This base case anchors the phi-rung index inside the Recognition Theta construction, which targets the modular identity under argument inversion (Sub-conjecture A.2 of Paper I). It feeds the phiRung_zero lemma in the RSNativeUnits module and supports the overall framework that derives spatial dimension D=3 and the eight-tick octave (T7) from the single functional equation. The result closes the zero case before the additivity theorems (phiRung_mul) and term-sign results can be applied to the series.
scope and limits
- Does not compute r(n) for any positive integer.
- Does not prove complete additivity of r.
- Does not address convergence or the modular identity of the Recognition Theta series.
formal statement (Lean)
79@[simp] theorem phiRung_zero : phiRung 0 = 0 := by
proof body
Term-mode proof.
80 unfold phiRung
81 simp [Nat.factorization_zero]
82
83/-- The phi-rung at a prime: `phiRung p = phiRungPrime p`. -/