sensitivity_at_carrier
plain-language theorem explainer
The theorem establishes that the phantom-coupled GW antenna sensitivity equals the reference floor h_0 exactly at the carrier frequency 5 phi Hz. Engineers citing the RS_PAT_030 track for sub-Hz strain detectors would use this baseline equality. The term-mode proof unfolds the piecewise definition, rewrites the conditional via carrier positivity, and finishes with field simplification.
Claim. Let carrier = 5 phi Hz with carrier > 0 and h_0 = 1. Define sensitivity(f) = h_0 * carrier / f for f > 0 (and 0 otherwise). Then sensitivity(carrier) = h_0.
background
The PhantomCoupledGWAntennaSensitivity module defines carrier as 5 * phi, matching the cortical neuromodulation device carrier at 5 phi Hz. The reference floor h_0 is the constant 1. Sensitivity at frequency f is the piecewise function that returns 0 for f <= 0 and otherwise h_0 * carrier / f, implementing the linear scaling h_min(f) = h_0 * carrier / f above the BIT carrier as stated in the module doc for RS_PAT_030.
proof idea
The term proof unfolds sensitivity and h_0, then rewrites the if-condition using not_le.mpr applied to carrier_pos. It introduces carrier ≠ 0 from ne_of_gt carrier_pos and invokes field_simp to reduce the division carrier / carrier to 1.
why it matters
This equality is invoked directly in gw_antenna_one_statement to bundle the carrier band, sensitivity_at_carrier, positivity, and strict anti-monotonicity into the PhantomCoupledGWAntennaSensitivityCert structure. It completes the engineering derivation step for the phantom-cavity GW antenna, confirming the floor value at the phi-based carrier inside the eight-tick octave. The module doc notes the falsifier would be a deployed antenna whose sensitivity ceiling fails to follow the 1/f scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.