laughlin_charge_one_third
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.
claimAt 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 in Recognition Science
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.
scope and limits
- Does not derive the value of q from ledger dynamics.
- Does not address stability of the Laughlin state.
- Does not compute Hall conductance at fractional fillings.
formal statement (Lean)
141theorem laughlin_charge_one_third :
142 laughlin_quasi_charge 3 = 1/3 := by
proof body
Term-mode proof.
143 simp [laughlin_quasi_charge]
144
145/-- Quasi-particle charge is smaller for larger q. -/