theorem proved term proof

`carrier_band`

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

formal statement (Lean)

  37theorem carrier_band : (8.05 : ℝ) < carrier ∧ carrier < 8.10 := by

proof body

Term-mode proof.

  38  unfold carrier
  39  have h1 := phi_gt_onePointSixOne
  40  have h2 := phi_lt_onePointSixTwo
  41  refine ⟨by linarith, by linarith⟩
  42
  43/-- Optimal pulse spacing in seconds (= 1 / carrier). -/

used by (11)

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

asteroidTrajectoryShapingCert in IndisputableMonolith.Engineering.AsteroidTrajectoryShaping decl_use
AsteroidTrajectoryShapingCert in IndisputableMonolith.Engineering.AsteroidTrajectoryShaping decl_use
corticalNeuromodulationDeviceCert in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use
CorticalNeuromodulationDeviceCert in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use
neuromod_one_statement in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use
carrier_band in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use
gw_antenna_one_statement in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use
phantomCoupledGWAntennaSensitivityCert in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use
PhantomCoupledGWAntennaSensitivityCert in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use
emSpectrumCert in IndisputableMonolith.Physics.ElectromagneticSpectrumFromPhiLadder decl_use
EMSpectrumCert in IndisputableMonolith.Physics.ElectromagneticSpectrumFromPhiLadder decl_use

depends on (5)

Lean names referenced from this declaration's body.

phi_gt_onePointSixOne in IndisputableMonolith.Constants decl_use
phi_lt_onePointSixTwo in IndisputableMonolith.Constants decl_use
carrier in IndisputableMonolith.Engineering.CorticalNeuromodulationDevice decl_use
carrier in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use
carrier_band in IndisputableMonolith.Engineering.PhantomCoupledGWAntennaSensitivity decl_use