phiRung_mul
plain-language theorem explainer
The phi-rung index r satisfies complete additivity r(m n) = r(m) + r(n) for all positive integers m and n. Researchers constructing the Recognition Theta series cite this to confirm that the rung map is a completely additive arithmetic function compatible with prime factorization. The proof unfolds the definition of phiRung, rewrites via the multiplicativity of Nat.factorization, and splits the resulting Finsupp sum with sum_add_index' before discharging the side conditions by ring arithmetic.
Claim. For all positive integers $m$ and $n$, the phi-rung index satisfies $r(m n) = r(m) + r(n)$, where $r(k)$ is the sum of the scaled exponents appearing in the prime factorization of $k$.
background
The Recognition Theta module builds the candidate modular completion Θ̃_RS(t) of the cost theta function by adjoining the 8-tick character and the phi-ladder weights. The phi-rung function, written phiRung n or r(n), is the integer-valued index obtained by summing the rung contributions of each prime power in the factorization of n; it is completely additive by design. The local setting is the elementary arithmetic layer that must be in place before the modular identity (Sub-conjecture A.2) can be stated as a hypothesis.
proof idea
The proof is a short tactic sequence: unfold phiRung exposes the Finsupp sum over the factorization support; rw [Nat.factorization_mul hm hn, Finsupp.sum_add_index'] splits the sum into two independent sums; the two side conditions are each discharged by push_cast followed by ring.
why it matters
This result supplies the complete additivity of the phi-rung index that is collected inside recognition_theta_certificate and that is invoked by the subsequent phiRung_prime_pow theorem. It realizes the phi-ladder arithmetic (T6) at the level of positive integers, thereby preparing the structural facts required for the Recognition Theta function and its conjectured modular identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.