chi8_three
plain-language theorem explainer
The theorem establishes that the eight-tick character evaluates to +1 at the integer 3. Researchers building the Recognition Theta series would cite this sign when assembling the n=3 term in the sum over the phi-ladder. The proof reduces directly to the definition of chi8 by unfolding and reflexivity.
Claim. $χ_8(3) = 1$, where $χ_8$ is the real character mod 8 that returns +1 on residues 1 and 3, -1 on 5 and 7, and 0 on evens.
background
The Recognition Theta module constructs a candidate completion of the cost theta function that incorporates the 8-tick character (T7) and phi-ladder weights (T6) to support a modular identity under t ↦ 1/t. The character χ₈ is defined by cases on n mod 8: it vanishes on even residues, returns +1 for n ≡ 1 or 3 (mod 8), and -1 for n ≡ 5 or 7 (mod 8). This matches the upstream definition in Primes.Modular.chi8, which supplies the same values over the integers.
proof idea
The proof is a one-line wrapper that unfolds the definition of chi8 and applies reflexivity.
why it matters
This supplies the explicit sign for the n=3 term inside the Recognition Theta sum, consistent with the eight-tick octave (T7) of the forcing chain. It forms part of the elementary arithmetic properties needed before the modular identity (Sub-conjecture A.2) can be stated as a hypothesis. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.