How does a dolphin see with sound underwater?

module click_chirp;

// Dolphin clicks are short broadband pulses centred ~50-130 kHz
// (Tursiops). We model the FM downsweep with start/end and a
// few-hundred-microsecond duration.
const F_START_HZ: Real = 130000.0
const F_END_HZ:   Real =  40000.0
const DURATION_S: Real =      0.0004

@verify(lean, theorem = "dolphin_click_frequency_in_band")
fn click_frequency(t_s: Real) -> Real
    requires (t_s >= 0.0 and t_s <= DURATION_S)
    ensures  (result >= F_END_HZ and result <= F_START_HZ)
{
    clamp(F_START_HZ + (F_END_HZ - F_START_HZ) * (t_s / DURATION_S),
          F_END_HZ, F_START_HZ)
}

module underwater_range;

// Speed of sound in seawater (25 °C, 35 ppt salinity, surface
// pressure). 1500 m/s is the standard textbook value; varies
// by ~25 m/s with depth/temperature/salinity but irrelevant at
// the precision a marine mammal uses.
const SPEED_OF_SOUND_WATER_M_S: Real = 1500.0

@verify(lean, theorem = "underwater_delay_to_distance_nonneg")
fn delay_to_distance(delay_s: Real) -> Real
    requires (delay_s >= 0.0)
    ensures  (result >= 0.0)
{
    SPEED_OF_SOUND_WATER_M_S * delay_s / 2.0
}

// Depth of water at which the click round-trip equals one
// inter-click-interval. A dolphin clicks faster as the target
// gets closer; this is the upper-distance bound for a given ICI.
@verify(lean, theorem = "max_range_for_ici_nonneg")
fn max_range_for_ici(ici_s: Real) -> Real
    requires (ici_s > 0.0)
    ensures  (result > 0.0)
{
    SPEED_OF_SOUND_WATER_M_S * ici_s / 2.0
}

module doppler_water;

// Round-trip Doppler for a target moving along the line-of-sight
// with closing speed v_rel (positive = toward the dolphin).
// Same form as the bat's Doppler kernel; only the wave speed
// constant changes.
const SPEED_OF_SOUND_WATER_M_S: Real = 1500.0

@verify(lean, theorem = "doppler_round_trip_positive_for_closing")
fn doppler_factor(v_rel_mps: Real) -> Real
    requires (-SPEED_OF_SOUND_WATER_M_S < v_rel_mps and
              v_rel_mps < SPEED_OF_SOUND_WATER_M_S)
    ensures  (result > 0.0)
{
    (SPEED_OF_SOUND_WATER_M_S + v_rel_mps) /
    (SPEED_OF_SOUND_WATER_M_S - v_rel_mps)
}

module matched_filter;

// Matched filter: the optimal linear detector for a known
// transmit waveform in white Gaussian noise. The peak of the
// cross-correlation locates the echo's arrival time, which
// underwater_range turns into a distance.
//
// We don't expand the explicit cross-correlation here — that's
// a vector op out-of-grammar for a sketch. The gain identity is
// the contract: matched-filter output is bounded by the energy
// product of the two signals.
const ENERGY_TX:  Real = 1.0
const ENERGY_ECHO: Real = 1.0

@verify(lean, theorem = "matched_filter_gain_at_most_unity")
fn normalised_correlation_peak(corr_peak: Real) -> Real
    requires (0.0 <= corr_peak and corr_peak <= 1.0)
    ensures  (0.0 <= result and result <= 1.0)
{
    corr_peak
}

module compare_air_vs_water;

// Side-by-side: same delay, different medium → different range.
// At a 5 ms round-trip delay, a bat sees a target ~0.86 m away
// (343 * 0.005 / 2). A dolphin sees one 3.75 m away
// (1500 * 0.005 / 2). Same algebra, ~4.4× longer reach for
// the same time budget.
const C_AIR_M_S:   Real =  343.0
const C_WATER_M_S: Real = 1500.0

@verify(lean, theorem = "water_reach_exceeds_air_for_equal_delay")
fn water_to_air_ratio() -> Real
    ensures (result > 1.0)
{
    C_WATER_M_S / C_AIR_M_S
}