quasi_charge_decreasing
plain-language theorem explainer
Quasi-particle charge in Laughlin states at filling 1/q decreases strictly as the denominator q grows. Condensed matter physicists modeling fractional quantum Hall hierarchies cite this ordering to rank charge values by denominator. The argument unfolds the charge definition, casts natural-number inequalities to rationals, and applies the standard positive-division lemma.
Claim. For positive integers $q_1 < q_2$, the Laughlin quasi-particle charge satisfies $1/q_2 < 1/q_1$.
background
The module treats the quantum Hall effect as a topological invariant arising from the eight-tick phase ledger. The central definition is laughlin_quasi_charge q := 1/q, which assigns charge e/q to quasi-particles at filling factor ν = 1/q. Upstream results supply the phase map kπ/4 for k in Fin 8 and the Statistics inductive type that distinguishes fermionic and bosonic exchange.
proof idea
Unfold laughlin_quasi_charge to reduce to the reciprocal inequality. Cast the three natural-number hypotheses to rationals to obtain positivity and the strict order. Apply div_lt_div_of_pos_left to the positive unit and the two rational inequalities.
why it matters
The monotonicity supplies the basic ordering of quasi-particle charges inside the Laughlin sequence at ν = 1/q. It supports the anyonic statistics θ = π/q stated in the module and the broader derivation of Chern-number quantization from eight-tick phases. No downstream uses are recorded, leaving its role in composite-fermion constructions open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.