theorem proved term proof

`electron_exchange_phase`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 164theorem electron_exchange_phase : laughlin_exchange_phase 1 = Real.pi := by

Term-mode proof.

 165  unfold laughlin_exchange_phase
 166  simp
 167
 168/-- ν = 1/3 quasi-particle exchange phase = π/3. -/

Lean names referenced from this declaration's body.

phase in IndisputableMonolith.Foundation.EightTick decl_use
phase in IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge decl_use
laughlin_exchange_phase in IndisputableMonolith.Physics.QuantumHallEffect decl_use