phiRung_one
plain-language theorem explainer
phiRung_one establishes that the phi-rung index evaluates to zero at unity, corresponding to the empty product in the prime factorization. Researchers constructing the Recognition Theta function cite this as the base case when verifying the structural properties of the rung index on positive integers. The term-mode proof reduces by unfolding the definition and simplifying against the standard fact that the factorization of one is the zero finsupp.
Claim. The phi-rung index satisfies $r(1)=0$, where $r(n)$ is the completely additive function on positive integers with $r(p)=⌊log_φ p⌋$ for each prime $p$.
background
The Recognition Theta module defines the phi-rung index phiRung n, written r(n), as a completely additive arithmetic function on the positive integers. For a prime p the value is the floor of the logarithm base phi, and the function extends by additivity over the prime factorization; the Recognition Theta sum then weights each term by this rung together with the chi8 character mod 8. This construction sits inside the larger Recognition framework that derives physics from the single functional equation, with the eight-tick octave (T7) and the self-similar phi fixed point (T6) supplying the modular and scaling structure. The present theorem supplies the base case required before the complete-additivity statement and before the modular-identity hypothesis can be stated.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of phiRung and invokes simp on the Mathlib fact that the factorization of one is the zero finsupp, which immediately yields the empty sum equal to zero.
why it matters
The result is invoked inside recognition_theta_certificate, the theorem that packages the elementary arithmetic facts (complete additivity of phiRung, the value at one, and the bound on chi8) before the Recognition Theta modular identity is stated as a hypothesis. It therefore closes the base case for the phi-ladder rung function that appears in the Recognition Theta construction and in the downstream mass-ladder formulas. Within the framework it supports the phi-forcing step (T6) and the eight-tick periodicity (T7) by guaranteeing that the rung index is well-defined at the multiplicative identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.