IndisputableMonolith.Physics.QuantumHallEffect

declarations in this module (22)

• structure ChernNumber L35
• theorem hall_conductance_quantized L40
• theorem chern_number_integer_from_8tick L51
• def iqhe_filling L60
• theorem iqhe_conductance_integer L63
• abbrev von_klitzing_constant L68
• theorem RK_positive L71
• def landau_energy L78
• theorem landau_spacing L82
• theorem zero_point_energy L89
• def jain_fraction L99
• theorem jain_denominator_odd_plus L103
• theorem jain_denominator_odd_minus L110
• theorem fqhe_odd_denominator L118
• theorem one_third_in_jain_sequence L124
• theorem two_fifth_in_jain_sequence L130
• def laughlin_quasi_charge L138
• theorem laughlin_charge_one_third L141
• theorem quasi_charge_decreasing L146
• def laughlin_exchange_phase L160
• theorem electron_exchange_phase L164
• theorem one_third_exchange_phase L169