jain_fraction
plain-language theorem explainer
The jain_fraction definition encodes the filling factors of the Jain sequence for fractional quantum Hall states as ν = p/(2mp ± 1). Condensed-matter theorists modeling composite fermions would cite it when listing fractions allowed by the 8-tick ledger balance and Fermi antisymmetry. It is realized as a direct conditional that selects the sign in the denominator according to the Boolean flag.
Claim. The Jain filling factor is defined by $ν(p,m,s) = p/(2mp + s)$ where $p,m$ are positive integers and $s = ±1$ is chosen by the Boolean flag.
background
In the Recognition Science account of the quantum Hall effect the integer case yields quantized Hall conductance from Chern numbers fixed by 8-tick phase topology, while fractional states arise when composite fermions are constrained by the same ledger. The module states that FQHE fractions obey ν = p/q with the denominator forced odd by fermion exchange statistics. Upstream structures on PhiForcingDerived supply the J-cost that enforces the 8-tick balance, and SpectralEmergence supplies the gauge content whose face-pair counting yields the odd-denominator rule.
proof idea
The definition is a one-line conditional expression that branches on the Boolean parameter to insert either +1 or -1 in the denominator.
why it matters
This definition supplies the explicit fractions used by the downstream theorems one_third_in_jain_sequence and two_fifth_in_jain_sequence. It realizes the jain_sequence entry listed in the module doc-comment and the RS_Quantum_Hall_Effect paper, connecting the eight-tick octave directly to the odd-denominator constraint required by antisymmetry. It leaves open the derivation of the full hierarchy from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.