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

physical_light_not_first

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)

 143theorem physical_light_not_first :
 144    ¬∀ s : Stage, s ≠ PhysicalLight → Before PhysicalLight s := by

proof body

Term-mode proof.

 145  intro h
 146  have hbad := h Stage.distinction (by decide)
 147  norm_num [Before, PhysicalLight, rank] at hbad
 148
 149/-! ## Observer: two senses -/
 150
 151/-- Primitive observer-like structure: a recognizer/interface. This is forced
 152as soon as recognition, not merely bare abstract distinction, is in play. -/

depends on (15)

Lean names referenced from this declaration's body.