recognitionThetaTruncated_two
plain-language theorem explainer
The theorem establishes that the Recognition Theta function truncated after the n=0 and n=1 terms equals 1 for any real parameter t. Researchers verifying base cases of the phi-ladder weighted theta series before invoking modular identities would cite this result. The proof is a direct term-mode reduction that unfolds the finite sum and applies the explicit evaluation of the n=1 term together with the vanishing n=0 contribution.
Claim. For every real number $t$, the truncated Recognition Theta function at level 2 satisfies $1$.
background
The Recognition Theta function is the candidate completion of the cost theta series that incorporates the 8-tick character and phi-ladder weights so as to inherit a modular identity under $t$ to $1/t$. The truncated version sums only the first few terms of the series. The module defines phiRung as the completely additive rung index with $r(p) = floor(log_phi p)$ for primes, chi8 as the character mod 8, and recognitionThetaTerm as the general summand. Upstream results include the complete additivity phiRung_mul and the evaluation recognitionTheta_at_one that fixes the constant term.
proof idea
The proof unfolds the definition of the truncated sum and simplifies the finite range sum using the successor lemma together with the explicit value of the n=1 term, which is 1, while the n=0 term contributes zero.
why it matters
This base-case verification anchors the truncated series before the modular identity hypothesis (Sub-conjecture A.2) is invoked, confirming the constant term required by the eight-tick octave (T7) and phi-ladder fixed point (T6). It supports the overall Recognition Theta program whose full Poisson summation step remains conditional. No downstream uses are recorded, leaving open its role in discharging the analytic sub-conjectures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.