electron_exchange_phase
plain-language theorem explainer
Electron exchange at filling factor 1 yields phase π, confirming fermionic statistics inside the Laughlin anyon construction. Condensed-matter theorists modeling integer quantum Hall states cite this result to anchor the q=1 limit of the anyonic statistics. The proof is a one-line wrapper that unfolds the Laughlin phase definition and simplifies.
Claim. The Laughlin anyon exchange phase evaluated at denominator q=1 equals π, i.e., θ(1) = π.
background
The module derives both integer and fractional quantum Hall effects from the Recognition Science 8-tick topological ledger. The 8-tick phase supplies discrete angles kπ/4 (k=0..7) that generate the Chern numbers and filling fractions. The Laughlin exchange phase is introduced as θ(q) = π/q, recovering fermions when q=1 and anyons when q>1. Upstream, the EightTick.phase definition supplies the underlying periodic angles, while the Wedge.phase definition supplies the associated complex exponentials used in the broader topological ledger.
proof idea
The proof is a one-line wrapper: it unfolds the definition of laughlin_exchange_phase (which is π/q) at q=1 and applies simp to obtain π.
why it matters
The result fixes the fermionic endpoint of the Laughlin sequence inside the module, thereby supporting the claims on quantized Hall conductance, integer Chern numbers from 8-tick topology, and the requirement of odd denominators for Pauli antisymmetry. It directly instantiates the 8-tick octave (T7) and the spatial dimension D=3 constraints of the forcing chain when applied to electron statistics. No open scaffolding remains for this specific case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.