3D acoustic localization

What does an owl hear?

Asymmetric ears + 30 µs ITD resolution = 2° angular precision in pure dark. The trick is anatomy, not timing.

What does an owl hear?

40 simulated localization trials, target at +20° azimuth / -15° elevation

Human — RMS 36.7°
Owl — RMS 1.60°

Snap your fingers. Watch the owl pinpoint, the human wander.

owl error
—
human error
—
onsets
0
tap above to enable the mic

The math behind it

Each function carries a @verify contract that compiles to a Lean theorem about its bounds. The same source compiles to C, Verilog, HLSL, and 28 more targets. View the experiment on GitHub →

interaural_time.emlchain 1
module interaural_time;

const SPEED_OF_SOUND_M_S: Real = 343.0
const EAR_SEPARATION_M:   Real = 0.06

@verify(lean, theorem = "itd_bounded_by_max_path")
fn interaural_time(angle_rad: Real) -> Real
    ensures (result <=  EAR_SEPARATION_M / SPEED_OF_SOUND_M_S)
    ensures (result >= -EAR_SEPARATION_M / SPEED_OF_SOUND_M_S)
{
    clamp(EAR_SEPARATION_M * sin(angle_rad) / SPEED_OF_SOUND_M_S,
          -EAR_SEPARATION_M / SPEED_OF_SOUND_M_S,
           EAR_SEPARATION_M / SPEED_OF_SOUND_M_S)
}
vertical_offset.emlchain 1
module vertical_offset;

const SPEED_OF_SOUND_M_S:    Real = 343.0
const VERTICAL_EAR_OFFSET_M: Real = 0.007

@verify(lean, theorem = "vertical_itd_bounded")
fn vertical_offset(elevation_rad: Real) -> Real
    ensures (result <=  VERTICAL_EAR_OFFSET_M / SPEED_OF_SOUND_M_S)
    ensures (result >= -VERTICAL_EAR_OFFSET_M / SPEED_OF_SOUND_M_S)
{
    clamp(VERTICAL_EAR_OFFSET_M * sin(elevation_rad) / SPEED_OF_SOUND_M_S,
          -VERTICAL_EAR_OFFSET_M / SPEED_OF_SOUND_M_S,
           VERTICAL_EAR_OFFSET_M / SPEED_OF_SOUND_M_S)
}
azimuth_estimate.emlchain 1
module azimuth_estimate;

const SPEED_OF_SOUND_M_S: Real = 343.0
const EAR_SEPARATION_M:   Real = 0.06
const HALF_PI:            Real = 1.5707963267948966

@verify(lean, theorem = "azimuth_in_valid_range")
fn azimuth_from_itd(delta_t_s: Real) -> Real
    ensures (result >= -HALF_PI)
    ensures (result <=  HALF_PI)
{
    clamp(asin(clamp(delta_t_s * SPEED_OF_SOUND_M_S / EAR_SEPARATION_M,
                     -1.0, 1.0)),
          -HALF_PI, HALF_PI)
}
elevation_estimate.emlchain 1
module elevation_estimate;

const SPEED_OF_SOUND_M_S:    Real = 343.0
const VERTICAL_EAR_OFFSET_M: Real = 0.007
const HALF_PI:               Real = 1.5707963267948966

@verify(lean, theorem = "elevation_in_valid_range")
fn elevation_from_vertical_itd(dt_v: Real) -> Real
    ensures (result >= -HALF_PI)
    ensures (result <=  HALF_PI)
{
    clamp(asin(clamp(dt_v * SPEED_OF_SOUND_M_S / VERTICAL_EAR_OFFSET_M,
                     -1.0, 1.0)),
          -HALF_PI, HALF_PI)
}

Same EML pipeline. Different sense.

Eight more cross-species sensor models live alongside this one — bat sonar, owl 3D hearing, pit-viper infrared, dog olfaction, pigeon magnetoreception, shark electric sense, mantis shrimp 16-channel hyperspectral, spider web vibration.

See all nine senses →