laughlin_exchange_phase
plain-language theorem explainer
Laughlin quasiparticles at filling factor 1/q carry an anyonic exchange phase of π/q. Physicists modeling fractional quantum Hall states cite this when deriving statistics from the topological ledger. The definition is a direct assignment of π divided by the integer denominator q.
Claim. The exchange phase for Laughlin quasiparticles with denominator $q$ is given by $θ(q) = π/q$.
background
The module treats the quantum Hall effect as a topological invariant arising from the RS ledger structure. Upstream, the EightTick phase supplies the discrete real values kπ/4 for k = 0 to 7, while the Wedge phase constructs the unimodular complex number e^{i w}. These feed the anyonic statistics for both integer and fractional fillings as described in the module documentation on the RS Quantum Hall Effect.
proof idea
One-line definition that returns Real.pi / q, inheriting the real phase value directly from the 8-tick construction.
why it matters
This definition supplies the exchange phase used by the downstream theorems electron_exchange_phase (q=1 yields fermions) and one_third_exchange_phase (q=3 yields π/3 anyons). It realizes the anyonic statistics required by the 8-tick balance for composite fermions in the FQHE, as stated in the module's key results and the paper RS_Quantum_Hall_Effect.tex.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.