pith. machine review for the scientific record. sign in
theorem proved term proof

fermion_phase_from_foundation

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 364theorem fermion_phase_from_foundation :
 365    Foundation.EightTick.phaseExp ⟨4, by norm_num⟩ = -1 :=

proof body

Term-mode proof.

 366  Foundation.EightTick.phase_4_is_minus_one
 367
 368open Foundation.EightTick in
 369/-- **FOUNDATION CONNECTION**: The boson phase (+1) derives from the
 370    Foundation's 8-tick structure at tick k=0.
 371
 372    This explicitly connects the spin-statistics theorem to the proven
 373    phase_0_is_one theorem in Foundation.EightTick. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.