ChernNumber
plain-language theorem explainer
ChernNumber encodes the integer topological invariant that sets the quantized Hall conductance in both integer and fractional quantum Hall regimes. Physicists modeling Landau level filling or composite fermion states would cite this structure when connecting RS ledger topology to observed conductance plateaus. The declaration is a direct structure definition that restricts the invariant to integer values by fiat.
Claim. A Chern number is an integer $n$ that counts the number of filled Landau levels (IQHE) or the composite-fermion Landau-level structure (FQHE) and equals the Hall conductance in units of $e^2/h$.
background
The module treats the quantum Hall effect as a direct consequence of the RS topological ledger. Hall conductance is identified with the Chern number of occupied states, with the IQHE arising from integer filling of Landau levels and the FQHE from composite fermions constrained by the 8-tick balance. The module imports EightTick and JcostCore, so the integer restriction inherits from the discrete phase topology and J-cost calibration already established upstream.
proof idea
The declaration is a structure definition that introduces a single field of type integer. No lemmas or tactics are invoked; the integer character is asserted directly in the structure and reinforced by the accompanying doc-comment on topological quantization.
why it matters
This supplies the integer Chern number required by the module's listed results, including hall_conductance_quantized and chern_number_integer_from_8tick. It links the 8-tick octave (T7) and the ledger factorization structures to the observed quantization of Hall conductance, closing the interface between spectral emergence and quantum Hall phenomenology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.