theorem proved term proof

`omega_BIT_pos`

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

formal statement (Lean)

  56theorem omega_BIT_pos : 0 < omega_BIT := by

Term-mode proof.

  57  unfold omega_BIT
  58  have h_phi := Constants.phi_pos
  59  linarith
  60
  61/-- The BIT carrier frequency is in the band `(7.5, 8.1)`. -/

Lean names referenced from this declaration's body.

Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
carrier in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use
carrier in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
band in IndisputableMonolith.Foundation.PreLogicalCost decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
omega_BIT in IndisputableMonolith.QuantumComputing.DecoherenceFromBIT decl_use