laughlin_quasi_charge
plain-language theorem explainer
The definition supplies the fractional charge carried by quasi-particles at filling factor one over q. Researchers modeling fractional quantum Hall states cite this assignment when deriving effective charges for Laughlin plateaus. It is realized as a direct reciprocal assignment in the native units with no further reduction.
Claim. At filling factor $ν = 1/q$ the quasi-particle charge equals $1/q$ (in units with electron charge $e = 1$).
background
The module derives the quantum Hall effect from the Recognition Science topological ledger structure. Integer quantum Hall conductance is quantized as $σ_{xy} = n e^2 / h$ via Chern numbers obtained from eight-tick phase topology. Fractional fillings $ν = p/q$ arise from composite fermions constrained by the same eight-tick balance, with the listed key result that quasi-particle charge equals $e/q$ at $ν = 1/q$.
proof idea
This is a direct definition that sets the charge equal to the reciprocal of the denominator q. No lemmas or tactics are applied beyond the assignment itself.
why it matters
The definition supplies the charge value used in the specific theorem for $ν = 1/3$ and in the proof that charge decreases with larger q. It implements the Laughlin charge result listed among the module key results and in the associated paper RS_Quantum_Hall_Effect.tex. It connects the fractional quantum Hall effect to the eight-tick octave constraint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.