one_third_in_jain_sequence
plain-language theorem explainer
The declaration verifies that the filling factor 1/3 arises as the Jain fraction with parameters p=1, m=1 and the plus sign. Researchers modeling fractional quantum Hall states via composite fermions would reference this when confirming allowed denominators from the 8-tick ledger. The proof reduces directly to the definition of jain_fraction followed by numerical simplification.
Claim. The Jain filling factor satisfies the formula for composite-fermion states: for positive integers p and m, the filling factor is p/(2mp + 1) when the plus branch is selected. Substituting p = 1 and m = 1 yields exactly 1/3.
background
The module derives the quantum Hall effect from the RS topological ledger, where the integer quantum Hall effect follows from Chern numbers tied to 8-tick phase topology and the fractional case arises from composite fermions constrained by the same balance. The key definition is jain_fraction (p m : ℕ) (plus : Bool) : ℚ, which returns p/(2mp + 1) on the plus branch and p/(2mp - 1) on the minus branch; the denominator is required to be odd to enforce Fermi statistics. Upstream results supply the ledger structure and the 8-tick neutrality condition that together force the allowed fractions.
proof idea
The proof is a one-line wrapper that unfolds the jain_fraction definition and applies numerical normalization to the resulting rational arithmetic.
why it matters
This anchors the Laughlin 1/3 state inside the RS-derived Jain sequence, confirming that the observed FQHE plateau fits the composite-fermion construction required by the 8-tick octave. It supports the module claim that FQHE fractions emerge directly from the same ledger that produces quantized Hall conductance and integer Chern numbers. The result closes one concrete instance of the general jain_sequence statement without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.