recognition_theta_certificate
plain-language theorem explainer
The theorem packages six elementary arithmetic facts on the phi-rung index, the mod-8 character chi8, and the individual terms of the Recognition Theta sum. Number theorists building the modular completion of the cost theta function cite it as the verified base layer before Poisson summation. The proof is a direct term-mode tuple that assembles the six component lemmas without further reasoning.
Claim. Let $r(n)$ be the phi-rung index on positive integers and let $chi_8(n)$ be the real character modulo 8. Then $r(mn)=r(m)+r(n)$ for all positive integers $m,n$, $r(1)=0$, $|chi_8(n)|leq 1$ for every natural number $n$, $chi_8(n+8)=chi_8(n)$ for every $n$, the Recognition Theta term at argument 1 equals 1 for any real $t$, and the term vanishes whenever the index is even.
background
The Recognition Theta function is defined as the candidate completion of the cost theta sum that folds in the eight-tick character from T7 and the phi-ladder weighting from T6. Its individual summands are given by the term function recognitionThetaTerm t n. The phi-rung index r(n) is the completely additive function on positive integers whose value on a prime p is floor(log_phi p). The character chi8 is the simplest nontrivial real character modulo 8. These objects are introduced in the module whose doc-comment states that the modular identity under t to 1/t remains a hypothesis structure pending phi-ladder Poisson summation.
proof idea
The proof is a one-line term-mode wrapper. It constructs the required conjunction by supplying the six lemmas already established in the same module: phiRung_mul for complete additivity, phiRung_one for the base case at 1, chi8_abs_le_one for the bound, chi8_periodic for the period-8 property, recognitionThetaTerm_one for the constant term, and recognitionThetaTerm_even for the vanishing on even indices.
why it matters
This certificate supplies the verified arithmetic foundation for the Recognition Theta construction inside the NumberTheory module. It directly supports the hypothesis structures RecognitionThetaConvergence and RecognitionThetaModularIdentity that appear later in the same file. The result encodes the T7 eight-tick periodicity and the T6 phi-ladder additivity that the framework primer lists as forced steps toward D=3. Because the modular identity itself is still stated as a hypothesis, the certificate closes the elementary layer while leaving the analytic continuation open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.