pith. machine review for the scientific record. sign in
theorem proved term proof high

sensitivity_at_carrier

show as:
view Lean formalization →

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.

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

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.

scope and limits

Lean usage

  have h : sensitivity carrier = h_0 := sensitivity_at_carrier

formal statement (Lean)

  51theorem sensitivity_at_carrier : sensitivity carrier = h_0 := by

proof body

Term-mode proof.

  52  unfold sensitivity h_0
  53  rw [if_neg (not_le.mpr carrier_pos)]
  54  have h_ne : carrier ≠ 0 := ne_of_gt carrier_pos
  55  field_simp
  56

used by (3)

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

depends on (7)

Lean names referenced from this declaration's body.