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

modes_span_distinct_bands

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)

 288theorem modes_span_distinct_bands :
 289    phi ^ 3 < phi ^ 5 ∧ phi ^ 5 < phi ^ 8 := by

proof body

Term-mode proof.

 290  constructor
 291  · linarith [phi_cubed_bounds.2, phi_fifth_bounds.1]
 292  · linarith [phi_fifth_bounds.2, phi_eighth_in_gamma_band.1]
 293
 294/-! ## Section 5: Device Specification
 295
 296The complete RS-coherent PBM device specification.
 297All parameters derive from φ with zero free parameters. -/
 298
 299/-- RS-coherent photobiomodulation device specification.
 300    Every field is derived from the golden ratio φ. -/

used by (1)

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

depends on (10)

Lean names referenced from this declaration's body.