phantomCoupledGWAntennaSensitivityCert
plain-language theorem explainer
Phantom-coupled GW antenna sensitivity is certified by a structure fixing the carrier in (8.05, 8.10) Hz with h_min(f) = h_0 * carrier / f for f > 0, enforcing positivity and strict decrease in frequency. Engineers modeling sub-Hz gravitational wave detectors cite this to fix the scaling law. The definition is a direct record construction from the module's carrier and sensitivity definitions.
Claim. Let carrier = 5φ. The certificate asserts 8.05 < carrier < 8.10, h_min(carrier) = h_0, ∀f > 0 (h_min(f) > 0), and ∀f₁, f₂ > 0 with f₁ < f₂ (h_min(f₂) < h_min(f₁)), where h_min(f) = h_0 · carrier / f for f > 0.
background
The module models the phantom-cavity-coupled GW antenna (RS_PAT_030) with strain sensitivity h_min(f) = h_0 · (5φ Hz / f). Carrier frequency is defined as 5φ Hz, imported from the cortical neuromodulation device. Sensitivity is defined as zero for f ≤ 0 and h_0 times carrier over f otherwise. The structure bundles the carrier band constraint, equality at the carrier, positivity for positive frequencies, and strict anti-monotonicity.
proof idea
The definition constructs the PhantomCoupledGWAntennaSensitivityCert record by direct field assignment from the module's carrier_band theorem, sensitivity_at_carrier equality, sensitivity_pos theorem, and sensitivity_strict_anti theorem.
why it matters
This packages the sensitivity properties supporting the gw_antenna_one_statement summary. It completes the engineering derivation for track J6 of Plan v5, linking the 5φ carrier to the 1/f scaling at LISA-band frequencies. In the Recognition framework it grounds observable strain response in the phi-based constants, with the module falsifier being a sub-Hz antenna whose ceiling fails to scale as 1/f.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.