laughlin_exchange_phase
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the filling factor 1/q from the forcing chain.
- Does not compute the quasiparticle charge e/q.
- Does not establish the existence of the Laughlin wavefunction.
- Does not address higher Landau level mixing.
formal statement (Lean)
160noncomputable def laughlin_exchange_phase (q : ℕ) : ℝ :=
proof body
Definition body.
161 Real.pi / q
162
163/-- Electron exchange phase = π (fermion). -/