sensitivity_pos
plain-language theorem explainer
The theorem proves that antenna sensitivity remains strictly positive for every positive frequency in the phantom-cavity GW model. Engineers verifying sub-Hz strain floors for RS_PAT_030 devices would cite it to confirm the reference scaling. The proof is a short term-mode reduction that unfolds the piecewise definition and applies division positivity using the carrier fact.
Claim. For every real number $f > 0$, the sensitivity satisfies $0 < h_0 · c / f$, where $c = 5φ$ Hz is the carrier frequency and $h_0 = 1$ is the reference floor.
background
The module treats phantom-cavity-coupled GW antenna sensitivity (RS_PAT_030). Carrier frequency is defined as $5φ$ Hz, identical to the cortical neuromodulation device carrier. Sensitivity is defined piecewise: it returns zero for $f ≤ 0$ and $h_0 ·$ carrier / $f$ otherwise, with $h_0$ set to the unit reference 1. Carrier positivity is imported from the neuromodulation device and restated locally, both proved by unfolding the definition and applying multiplication positivity with the known positivity of $φ$. The module doc states the target scaling $h_min(f) = h_0 · (5φ Hz / f)$ for sub-Hz strain sensitivity.
proof idea
The proof unfolds sensitivity and h_0, rewrites the if-condition via not_le.mpr on the hypothesis 0 < f, then applies div_pos. The numerator side is discharged by simp followed by the carrier_pos fact; the denominator side is discharged directly by the hypothesis.
why it matters
The result populates the sensitivity_pos field of PhantomCoupledGWAntennaSensitivityCert, which is assembled into the module certificate. It is referenced by unsat_has_positive_gap and UNSATGapCondition in the SpectralGap module to extract a positive min_sensitivity value. The derivation fills the engineering track step that sets the BIT carrier at 5φ Hz as the reference for the inverse-frequency scaling above carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.