chi8_abs_le_one
plain-language theorem explainer
The 8-tick character satisfies |chi8(n)| ≤ 1 for every natural number n. Researchers assembling the structural certificate for the Recognition Theta function cite this bound together with the complete additivity of the phi-rung index. The argument unfolds the definition of chi8 and exhausts the eight residue classes modulo 8 by interval case analysis.
Claim. $|χ_8(n)| ≤ 1$ for all $n ∈ ℕ$, where $χ_8$ is the 8-tick character.
background
The Recognition Theta module builds a candidate completion of the cost theta series by adjoining the 8-tick character (T7) and the phi-ladder weights (T6). The 8-tick character is the simplest non-trivial real character modulo 8; the fundamental time quantum is the tick τ₀ = 1 in RS-native units, with one octave equal to eight ticks. The module proves all listed arithmetic facts with zero sorry and states the modular identity as the hypothesis RecognitionThetaModularIdentity (Sub-conjecture A.2).
proof idea
Unfold chi8. Record that n % 8 < 8 by the standard modulus lemma. Apply interval_cases to split on the eight possible residues. Each branch reduces by simp to the required inequality.
why it matters
The bound supplies the third conjunct of recognition_theta_certificate, the theorem that packages the arithmetic facts required for the Recognition Theta construction. It supplies the elementary control on the 8-tick character (T7) needed before the modular identity can be stated. The full modular inversion property remains a hypothesis structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.