sensitivity
plain-language theorem explainer
The sensitivity definition supplies the minimum detectable strain h_min(f) for a phantom-cavity GW antenna. Engineers modeling sub-Hz detectors and proofs in JConvexityUniversality cite the 1/f scaling above the carrier. The definition is a direct conditional that returns zero below zero frequency and h_0 times carrier over f otherwise.
Claim. The minimum strain sensitivity is defined by $h_0(f) = 0$ if $f ≤ 0$ and $h_0 · (5φ / f)$ otherwise, where $5φ$ denotes the carrier frequency in Hz and $h_0 = 1$ is the reference floor at the carrier.
background
The module models a phantom-cavity-coupled GW antenna whose carrier frequency is fixed at 5φ Hz. Upstream carrier definitions state that the cortical-column carrier equals 5 · φ Hz and that h_0 sets the dimensionless sensitivity floor to unity. The local setting requires that strain sensitivity scale linearly above the carrier and inversely below it for LISA-band mHz frequencies.
proof idea
The definition is implemented as a direct conditional expression on the sign of f. No lemmas are applied; the body simply multiplies the constant h_0 by carrier and divides by f when f is positive.
why it matters
This supplies the explicit sensitivity law used by gw_antenna_one_statement to certify carrier band and strict anti-monotonicity, and by PhantomCoupledGWAntennaSensitivityCert to record the engineering properties. It feeds jcost_at_one_plus_delta and universalSensitivity_eq in JConvexityUniversality, connecting the 1/f engineering model to the quadratic leading term of the J-cost. The construction completes the J6 track by furnishing the required frequency dependence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.