two_fifth_in_jain_sequence
plain-language theorem explainer
The theorem confirms that the filling factor 2/5 arises in the Jain sequence for composite fermions with p=2 and m=1 under the plus branch. Researchers modeling fractional quantum Hall states via the Recognition Science ledger would reference this when listing allowed fractions. The proof proceeds by unfolding the jain_fraction definition and applying arithmetic normalization.
Claim. $2/5$ satisfies the Jain sequence formula for filling factor $p/(2mp+1)$ with $p=2$, $m=1$.
background
The module derives the quantum Hall effect from the RS topological ledger, where the integer QHE follows from Chern numbers tied to the eight-tick phase structure and the fractional case from composite fermions constrained by the 8-tick balance. The jain_fraction definition encodes the allowed filling factors as $p/(2mp+1)$ or $p/(2mp-1)$ with odd denominators enforced by Fermi statistics. Upstream, the Charge abbrev sets the native units while the jain_fraction def supplies the sequence formula directly applied here.
proof idea
The proof is a one-line wrapper that unfolds the jain_fraction definition and reduces the resulting rational equality via norm_num.
why it matters
This instance anchors the Jain sequence within the RS framework for the FQHE, supporting the claim that fractions like 2/5 emerge from the 8-tick balance constraint on composite fermions. It fills the specific case for the 2/5 state listed among the module's key results on jain_sequence. No downstream uses appear yet, leaving open integration with quasi-particle charge calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.