chern_number_integer_from_8tick
plain-language theorem explainer
Recognition Science derives integer Chern numbers for Landau levels in the quantum Hall effect from the exact periodicity of its eight discrete phase factors. A condensed-matter theorist would cite this when proving that Hall conductance is quantized in integer multiples of e²/h. The argument is a one-line wrapper that invokes the algebraic identity (phaseExp k)^8 = 1 for each k in Fin 8.
Claim. For every $k = 0,1,…,7$, the complex phase factor $e^{i k π/4}$ satisfies $(e^{i k π/4})^8 = 1$.
background
The module treats the integer quantum Hall effect as a topological consequence of the RS ledger. The eight-tick structure supplies the phase factors via phase(k) = k π/4 and phaseExp(k) = exp(i · phase(k)). These phases are periodic with period 2π, so their eighth powers equal unity by the standard exponential periodicity exp(2π i n) = 1 for integer n. The upstream lemma phase_eighth_power_is_one records exactly this identity after unfolding the definitions and applying the exponential multiplication rule.
proof idea
The proof is a one-line wrapper. It introduces the index k and directly supplies the pair (1, phase_eighth_power_is_one k) to witness the existential quantifier.
why it matters
This result supplies the topological integrality needed for the quantized Hall conductance σ_xy = n e²/h inside the same module. It realizes the eight-tick octave (T7) of the forcing chain as a concrete periodicity that forces the Berry curvature integral over the Brillouin zone to be an integer multiple of 2π. The declaration therefore closes the link between the RS-native 8-tick ledger and the observed integer quantum Hall plateaus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.