nonzero_modes_mod_8
plain-language theorem explainer
The declaration states that the set of integers from 1 to 7 has cardinality 7, or equivalently 8 minus 1. Researchers working on the Q3 unification of Ramanujan mock theta orders and partition congruences cite this fact to identify 7 as the count of non-DC modes in the 8-tick window. The proof is a one-line wrapper that invokes the decide tactic on the finite cardinality equality.
Claim. The cardinality of the set of integers from 1 to 7 equals 7, or equivalently $8-1$.
background
The module establishes that 24 equals the directed flux count of Q3, which factors as 8 times 3. This 8 arises from the eight-tick octave in the forcing chain, where non-DC modes are the non-zero frequency components in the discrete Fourier transform over that period. The doc-comment identifies the 7 non-DC modes as covering all non-zero frequencies mod 8, directly linking the count to the appearance of 7 among mock theta orders (odd primes p with gcd(p,8)=1 and p<8). Upstream, SpectralEmergence.of shows Q3 forces 24 chiral fermion flavors (=3×8) and |Aut(Q3)|=48 total fermionic degrees of freedom, supplying the combinatorial seed for the arithmetic fact.
proof idea
The proof is a one-line wrapper that applies the decide tactic to verify the cardinality of the closed interval from 1 to 7 equals 7.
why it matters
This supplies the arithmetic fact that exactly 7 non-DC modes exist modulo 8, which the module documentation uses to explain why 7 appears in both mock theta orders and congruence primes via the Q3 structure. It fills the explicit claim that 7 equals the number of non-DC DFT modes in the 8-tick window. In the Recognition framework it connects to the eight-tick octave (T7) and the relation 24=8×3 that separates 3 (mock-only) from 11 (congruence-only) while placing 7 in the overlap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.