theorem proved term proof

`carrier_gt_8`

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

formal statement (Lean)

  45theorem carrier_gt_8 : carrierFreq > 8 := by

Term-mode proof.

  46  unfold carrierFreq
  47  have := phi_gt_onePointSixOne
  48  linarith
  49
  50/-- Theta-band upper bound: 5φ < 5 · 1.62 = 8.1. -/

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

dftHarmonicSpectrumCert in IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum decl_use

Lean names referenced from this declaration's body.

phi_gt_onePointSixOne in IndisputableMonolith.Constants decl_use
carrierFreq in IndisputableMonolith.CrossDomain.DFTHarmonicSpectrum decl_use
band in IndisputableMonolith.Foundation.PreLogicalCost decl_use