jain_denominator_odd_minus
plain-language theorem explainer
The theorem shows that for natural numbers p and m with 2mp > 1 the denominator 2mp-1 of the Jain filling factor ν = p/(2mp-1) is odd. Condensed-matter theorists modeling fractional quantum Hall states cite this to enforce the odd-denominator constraint required by composite-fermion statistics. The short tactic proof rewrites the product, strengthens the inequality, applies omega to the modular arithmetic, and equates the expressions via ring normalization.
Claim. For natural numbers $p, m$ satisfying $2mp > 1$, the integer $2mp - 1$ is odd: $(2mp - 1) % 2 = 1$.
background
The module derives the quantum Hall effect from the Recognition Science topological ledger. Jain fractions appear as allowed filling factors ν = p/(2mp ± 1) under the 8-tick balance constraint. The odd-denominator requirement follows from the antisymmetry of the fermionic wave function, as stated in the module's pauli_from_antisymmetry result.
proof idea
The proof first rewrites 2 * m * p as 2 * (m * p) by ring. It then uses linarith on the rewritten inequality to obtain 1 < 2*(mp). Omega solves the modular claim (2(m*p)-1) % 2 = 1 directly. Finally linarith equates the original expression to the rewritten one after ring_nf normalization.
why it matters
This result supplies the minus branch of the Jain sequence ν = p/(2mp-1) and thereby supports the module's claim that FQHE fractions require odd denominators. It closes one half of the jain_sequence construction referenced in the module documentation and the paper RS_Quantum_Hall_Effect.tex. The odd parity is ultimately traceable to the eight-tick phase topology that enforces fermionic exchange statistics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.