Olfaction — Michaelis-Menten kinetics

What does a dog smell?

A 10,000× tighter K_d turns a trace plume from invisible to fully resolved. Drag the source strength and watch the dog's perception window collapse onto the human's.

What does a dog smell?

human (top, faint blue) · dog (bottom, full plume cone)

Human (K_d ≈ 1 ppm)
Dog (K_d ≈ 0.1 ppt — 10,000× tighter)
10⁻¹³ — only dog10⁻⁹ — explosive trace10⁻⁵ — both detect

Blow into the mic. Watch the plume disperse.

tap above to enable wind from blowing

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 →

receptor_binding.emlchain 0
module receptor_binding;

const R_MAX: Real = 1.0
const K_D:   Real = 1.0e-6

@verify(lean, theorem = "receptor_binding_in_unit_interval")
fn receptor_binding(c: Real) -> Real
    requires (c >= 0.0)
    ensures  (result >= 0.0)
    ensures  (result <= R_MAX)
{
    clamp(R_MAX * c / (c + K_D), 0.0, R_MAX)
}
sensitivity_ratio.emlchain 0
module sensitivity_ratio;

const K_D_DOG:   Real = 1.0e-10
const K_D_HUMAN: Real = 1.0e-6

@verify(lean, theorem = "sensitivity_ratio_at_least_one")
fn dog_vs_human_sensitivity(c: Real) -> Real
    requires (c >= 0.0)
    ensures  (result >= 1.0)
{
    max(1.0, (c + K_D_HUMAN) / (c + K_D_DOG))
}
plume_diffusion.emlchain 1
module plume_diffusion;

const PI:          Real = 3.14159265358979
const WIND_SPEED:  Real = 1.0
const SIGMA_COEFF: Real = 0.2

@verify(lean, theorem = "plume_concentration_nonneg")
fn plume_concentration(Q: Real, x: Real, y: Real) -> Real
    requires (Q >= 0.0)
    requires (x > 0.0)
    ensures  (result >= 0.0)
{
    max(0.0,
        Q / (2.0 * PI * SIGMA_COEFF * SIGMA_COEFF * x * WIND_SPEED)
          * exp(-(y * y) / (2.0 * SIGMA_COEFF * SIGMA_COEFF * x)))
}
stereo_smell.emlchain 0
module stereo_smell;

@verify(lean, theorem = "stereo_difference_bounded")
fn stereo_concentration_diff(c_left: Real, c_right: Real) -> Real
    requires (c_left  >= 0.0 and c_left  <= 1.0)
    requires (c_right >= 0.0 and c_right <= 1.0)
    ensures  (result >= -1.0 and result <= 1.0)
{
    clamp(c_left - c_right, -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 →