pith. machine review for the scientific record. sign in
def definition def or abbrev high

sensitivity

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  48def sensitivity (f : ℝ) : ℝ :=

proof body

Definition body.

  49  if f ≤ 0 then 0 else h_0 * carrier / f
  50

used by (17)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.