chi8_seven
plain-language theorem explainer
The theorem states that the 8-tick character evaluates to -1 at argument 7. Workers on the Recognition Theta sum or its modular properties would cite this value when expanding explicit terms or checking sign patterns in the series. The proof is a one-line wrapper that unfolds the character definition and confirms the equality by reflexivity.
Claim. $χ_8(7) = -1$, where $χ_8$ is the simplest non-trivial real character modulo 8.
background
The Recognition Theta module constructs a candidate completion Θ̃_RS(t) of the cost theta series by adjoining the 8-tick character χ₈ and the phi-ladder weights. χ₈ is introduced as the non-trivial real Dirichlet character modulo 8, chosen to match the eight-tick octave period. The module also defines phiRung as the completely additive rung function with r(p) = ⌊log_φ p⌋ and recognitionTheta as the corresponding tsum; all listed theorems carry zero sorrys.
proof idea
The proof is a one-line wrapper that unfolds the definition of χ₈ and applies reflexivity.
why it matters
This supplies an explicit arithmetic value required for term-by-term sign control inside the Recognition Theta sum. It supports the structural properties listed in the module (phiRung_mul, recognitionThetaTerm_pos) that precede the modular-identity hypothesis (Sub-conjecture A.2). The result sits inside the T7 eight-tick octave and T6 phi-ladder steps of the forcing chain; no downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.