two_fifth_in_jain_sequence
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 in Recognition Science
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.
scope and limits
- Does not establish energy minimization for the 2/5 state.
- Does not derive the Laughlin quasi-particle charge at this filling.
- Does not address Hall conductance quantization from first principles.
formal statement (Lean)
130theorem two_fifth_in_jain_sequence :
131 jain_fraction 2 1 true = 2/5 := by
proof body
Term-mode proof.
132 unfold jain_fraction
133 norm_num
134
135/-! ## Laughlin Quasi-particle Charge -/
136
137/-- At filling ν = 1/q, quasi-particles carry fractional charge e/q. -/