chi8_zero
plain-language theorem explainer
The Recognition Theta module introduces the 8-tick real character χ₈ to complete the cost theta function with the eight-tick structure from the forcing chain. This theorem records the base case χ₈(0) = 0, which is required for the character to be well-defined on the naturals and for the Recognition Theta sum to begin correctly. The proof is a one-line unfolding of the definition of χ₈ followed by reflexivity.
Claim. $χ_8(0) = 0$, where $χ_8$ is the real character modulo 8 that vanishes on even residues and takes values $+1$ or $-1$ on odd residues according to the residue class.
background
The module constructs the Recognition Theta function Θ̃_RS(t) as a 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 inherit a modular identity under t ↦ 1/t. The character χ₈ is defined by cases on n % 8: it equals 0 for even residues, +1 for residues 1 and 3, and -1 for residues 5 and 7. The upstream definition in Primes.Modular supplies the integer-valued version of the same character, while the local definition in RecognitionTheta lifts it to reals for use in the theta sum.
proof idea
The proof is a one-line wrapper that unfolds the definition of χ₈ and applies reflexivity to the resulting match expression on 0 % 8.
why it matters
This base case anchors the 8-tick character used throughout the Recognition Theta construction, which targets the modular identity stated as hypothesis RecognitionThetaModularIdentity. It supports evaluation of the constant term in the theta sum and is a prerequisite for later results such as recognitionTheta_at_one. The declaration sits inside the elementary arithmetic layer that precedes the phi-ladder Poisson summation required for the full modular property.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.