fqhe_odd_denominator
plain-language theorem explainer
The result shows that Jain-sequence filling factors for the fractional quantum Hall effect must carry odd denominators. Physicists enumerating allowed composite-fermion fractions would cite it when restricting the topological ledger to fermion-compatible states. The argument reduces the claim directly to the prior congruence that the denominator equals 1 modulo 2 and then applies an arithmetic decision procedure.
Claim. For positive integers $p$ and $m$, the denominator $2mp+1$ of the Jain filling factor satisfies $(2mp+1) mod 2 ≠ 0$.
background
The module derives both integer and fractional quantum Hall effects from the Recognition Science topological ledger, with the integer case tied to Chern numbers of occupied Landau levels under eight-tick phase topology. The fractional case follows from composite fermions whose effective filling factors obey the eight-tick balance, yielding the Jain sequence of fractions $p/(2mp±1)$. The immediate upstream result states that the denominator of a Jain fraction for $ν = p/(2mp+1)$ is congruent to 1 modulo 2.
proof idea
The proof invokes the upstream theorem that the Jain denominator is congruent to 1 modulo 2 and then applies the omega tactic to obtain the negation of even parity.
why it matters
This declaration supplies the explicit odd-denominator constraint required by the module's pauli_from_antisymmetry claim, confirming that fermion exchange symmetry restricts the allowed topological sectors. It sits inside the eight-tick octave structure that forces three spatial dimensions and the composite-fermion construction. No downstream uses are recorded yet, leaving its integration with the full Jain-sequence enumeration open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.