one_third_exchange_phase
plain-language theorem explainer
The declaration establishes that the exchange phase for Laughlin quasi-particles at filling factor 1/3 equals π/3. Condensed matter physicists modeling anyonic statistics in the fractional quantum Hall regime would cite this when extracting braiding phases from the RS topological ledger. The proof is a direct specialization of the general phase definition followed by arithmetic normalization.
Claim. For Laughlin quasi-particles at filling factor ν = 1/3 the exchange phase satisfies θ = π/3.
background
The module derives the quantum Hall effect from the Recognition Science topological ledger structure, where integer Hall conductance arises as a Chern number invariant of occupied Landau levels and fractional states follow from composite fermions constrained by 8-tick balance. The upstream definition states that Laughlin quasi-particles at filling ν = 1/q carry anyonic exchange phase θ = π/q, recovering fermions for q = 1 and anyons for q = 3. This places the result inside the module's treatment of quantized Hall conductance, Jain sequences, and odd-denominator requirements from fermion exchange.
proof idea
The proof is a one-line wrapper that unfolds the definition of the general Laughlin exchange phase and applies numerical normalization to confirm the equality for q = 3.
why it matters
This result specializes the anyonic statistics to the primary Laughlin state at ν = 1/3, supporting the module's claims on fractional quantum Hall fractions and the requirement of odd denominators from fermion exchange. It connects directly to the RS eight-tick octave and topological ledger structure in the paper RS_Quantum_Hall_Effect.tex. No open questions are addressed here, but the instance closes a concrete case within the FQHE sequence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.