Web vibration — passive analog signal processor

What does a spider feel?

The web does most of the classification mechanically — bandpass filtering at 150 Hz with 100 Hz bandwidth. By the time the signal reaches the spider's legs, prey has already been sorted from wind.

prey (top, narrowband 200 Hz, score +1.00) · wind (bottom, broadband <30 Hz, score -0.18)

Web — tap anywhere on the silk to drop a fly

Time-domain vibration on a single radial thread

FFT (color) + web bandpass (dashed) — energy distribution

PREY

score = +1.00

spider strikes

A vibration arrives at the spider’s leg. Pick the source. The web’s mechanical bandpass (dashed line above) keeps prey frequencies and rolls off wind—the spider only strikes when enough energy lands inside the band.

Tap to simulate a vibration source hitting the web.

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 →

string_vibration.emlchain 1

module string_vibration;

@verify(lean, theorem = "string_vibration_amplitude_bounded")
fn string_displacement(A: Real, x: Real, L: Real, n: Real,
                       f: Real, t: Real) -> Real
    requires (A >= 0.0)
    ensures  (result <=  A and result >= -A)
{
    clamp(A * sin(n * 3.14159265358979 * x / L)
            * cos(2.0 * 3.14159265358979 * f * t),
          -A, A)
}

frequency_filter.emlchain 0

module frequency_filter;

const F_0_HZ:    Real = 150.0
const BANDWIDTH: Real = 100.0

@verify(lean, theorem = "frequency_gain_in_unit_interval")
fn frequency_gain(f: Real) -> Real
    requires (f > 0.0)
    ensures  (result >= 0.0 and result <= 1.0)
{
    clamp(1.0 / sqrt(1.0 +
                     ((f * f - F_0_HZ * F_0_HZ) / (f * BANDWIDTH))
                     *
                     ((f * f - F_0_HZ * F_0_HZ) / (f * BANDWIDTH))),
          0.0, 1.0)
}

direction_detect.emlchain 1

module direction_detect;

const HALF_PI: Real = 1.5707963267948966

@verify(lean, theorem = "direction_angle_in_quarter_circle")
fn direction_from_delay(dt: Real, v_wave: Real, d: Real) -> Real
    requires (v_wave > 0.0 and d > 0.0)
    ensures  (result >= -HALF_PI and result <= HALF_PI)
{
    clamp(asin(clamp(dt * v_wave / d, -1.0, 1.0)),
          -HALF_PI, HALF_PI)
}

prey_vs_wind.emlchain 0

module prey_vs_wind;

@verify(lean, theorem = "prey_vs_wind_score_bounded")
fn classify(E_above: Real, E_below: Real) -> Real
    requires (E_above >= 0.0 and E_below >= 0.0)
    ensures  (result >= -1.0 and result <= 1.0)
{
    clamp((E_above - E_below) / max(E_above + E_below, 1.0e-12),
          -1.0, 1.0)
}

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 →