sensitivity_pos
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not fix a numerical value for h_0 beyond the unit reference.
- Does not incorporate quantum or thermal noise floors.
- Does not prove the strict anti-monotonicity property (handled by a sibling theorem).
- Does not address specific LISA-band mHz deployment constraints.
Lean usage
def phantomCoupledGWAntennaSensitivityCert : PhantomCoupledGWAntennaSensitivityCert where carrier_band := carrier_band sensitivity_at_carrier := sensitivity_at_carrier sensitivity_pos := @sensitivity_pos sensitivity_strict_anti := @sensitivity_strict_antiformal statement (Lean)
57theorem sensitivity_pos {f : ℝ} (h : 0 < f) : 0 < sensitivity f := by
proof body
Term-mode proof.
58 unfold sensitivity h_0
59 rw [if_neg (not_le.mpr h)]
60 apply div_pos
61 · simp; exact carrier_pos
62 · exact h
63
64/-- Sensitivity is strictly anti-monotonic in `f` (above carrier:
65sensitivity decreases; below: increases). -/