laughlin_charge_one_third
plain-language theorem explainer
The declaration proves that the quasi-particle charge at filling factor ν = 1/3 equals 1/3 of the elementary charge. Researchers modeling fractional quantum Hall states within the Recognition Science ledger would cite this when linking the 8-tick balance to Laughlin quasiparticles. The proof is a one-line term-mode simplification that unfolds the definition of the quasi-charge function.
Claim. At filling factor $ν = 1/3$, the quasi-particle charge equals $1/3$ (in units where the elementary charge $e = 1$).
background
The Quantum Hall Effect module derives both integer and fractional Hall conductances from the Recognition Science topological ledger. The 8-tick balance constrains composite fermions, producing Jain sequences and Laughlin states at filling factors ν = 1/q. The function laughlin_quasi_charge(q) assigns fractional charge 1/q to quasiparticles at ν = 1/q, consistent with the composite-fermion picture described in the module documentation.
proof idea
The proof is a one-line term-mode simplification that unfolds the definition laughlin_quasi_charge q := 1/q at q = 3.
why it matters
This result fills the Laughlin charge slot in the FQHE sequence, directly supporting the module claim that quasi-particle charge equals e/q at ν = 1/q. It connects to the paper RS_Quantum_Hall_Effect.tex and the forcing chain T7 eight-tick octave. The result is fully proved with no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.