PhantomCoupledGWAntennaSensitivityCert
plain-language theorem explainer
The PhantomCoupledGWAntennaSensitivityCert structure packages the carrier frequency band constraint, equality of sensitivity at the carrier to the floor value, positivity for all positive frequencies, and strict decrease of sensitivity with increasing frequency. Gravitational wave instrumentation researchers would cite this certificate when confirming the inverse scaling law for phantom-cavity antennas in the LISA band. The structure is assembled directly from the carrier definition, the sensitivity function, and the anti-monotonicity lemma.
Claim. Let $c = 5phi$ denote the carrier frequency in Hz and let $s(f)$ denote sensitivity at frequency $f$. The certificate asserts $8.05 < c < 8.10$, $s(c) = h_0$, $s(f) > 0$ for every $f > 0$, and $s(f_2) < s(f_1)$ whenever $0 < f_1 < f_2$, where $s(f) = h_0 c / f$ for $f > 0$.
background
The module models a phantom-cavity-coupled gravitational wave antenna with minimum detectable strain $h_{min}(f) = h_0 c / f$ for positive frequencies, where $c = 5 phi$ is the BIT carrier. The carrier definition yields the interval (8.05, 8.10) via the golden-ratio bounds $phi > 1.61$ and $phi < 1.62$. The sensitivity function returns zero for non-positive arguments and the scaled reciprocal $h_0 c / f$ otherwise, with floor $h_0 = 1$.
proof idea
The structure is a record whose fields are supplied by direct reference. The carrier band field comes from the carrier band theorem. The equality at carrier follows by unfolding the sensitivity definition. Positivity and strict anti-monotonicity are taken from the corresponding lemmas, with the latter proved by case analysis on the piecewise definition and reduction to the inequality of positive reciprocals.
why it matters
This certificate supports the phantomCoupledGWAntennaSensitivityCert definition that serves as the master statement for the engineering derivation of phantom-cavity GW antenna sensitivity on track J6 of Plan v5. It verifies the required positivity and inverse scaling above the carrier at $5 phi$ Hz. The result aligns with Recognition Science constants and supplies the falsifier of a deployed antenna failing to exhibit the predicted $1/f$ behavior.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.