jain_denominator_odd_plus
plain-language theorem explainer
The denominator 2mp + 1 of Jain fractions ν = p/(2mp + 1) is always odd for positive integers p and m. Researchers modeling fractional quantum Hall states via composite fermions cite this parity result to enforce the odd-denominator rule. The proof reduces the expression via ring simplification and applies omega to establish the modulo-2 identity.
Claim. For positive integers $p$ and $m$, the denominator $2mp + 1$ of the Jain filling factor $ν = p/(2mp + 1)$ satisfies $(2mp + 1) ≡ 1 mod 2$.
background
In the Recognition Science treatment of the quantum Hall effect, the fractional quantum Hall effect arises from composite fermions constrained by the 8-tick balance. The module states that allowed FQHE fractions are ν = p/(2mp ± 1) and that the odd-denominator condition follows from fermion antisymmetry in the topological ledger structure. Upstream results on J-cost structures and ledger factorization supply the algebraic setting in which this parity fact is applied.
proof idea
The proof begins by rewriting 2 * m * p as 2 * (m * p) using ring. It then applies omega to verify that (2 * (m * p) + 1) % 2 = 1. Finally, linarith combines this with a ring_nf equality to conclude the result for the original expression.
why it matters
This result supports the key theorem fqhe_odd_denominator establishing that FQHE requires an odd denominator. It fills the pauli_from_antisymmetry step in the module, linking to the 8-tick octave and fermion exchange symmetry in the Recognition framework. The parent theorem uses it directly to negate even parity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.