Magnetoreception — quantum biology

How does a pigeon find its way home?

Two scalars from one molecule: field intensity (the map) and inclination (the compass). Cryptochrome radical-pair coherence in the retina decodes both.

human view (uniform gray) · pigeon view (intensity + inclination)

Pigeon — geomagnetic intensity heatmap (latitude axis vertical)

Field intensity

45.9 µT

Inclination

61°

Region

mid-latitude — moderate dip

Latitude: 42°

South poleEquator (B = 30 µT)North pole (B = 60 µT)

Tap anywhere on Earth. See the pigeon’s compass.

location
40.0°N · -80.0°E
|B|
44.9 µT
inclination
59.2°
declination
-4.8°

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 →

geomagnetic_field.emlchain 1

module geomagnetic_field;

const B_EQUATORIAL_T: Real = 3.0e-5

@verify(lean, theorem = "geomagnetic_field_strictly_positive")
fn geomagnetic_field(latitude_rad: Real) -> Real
    ensures (result >= B_EQUATORIAL_T)
{
    max(B_EQUATORIAL_T,
        B_EQUATORIAL_T * sqrt(1.0 + 3.0 * sin(latitude_rad)
                                       * sin(latitude_rad)))
}

inclination.emlchain 1

module inclination;

const HALF_PI: Real = 1.5707963267948966

@verify(lean, theorem = "inclination_in_quarter_circle")
fn inclination(latitude_rad: Real) -> Real
    ensures (result >= -HALF_PI)
    ensures (result <=  HALF_PI)
{
    clamp(atan(2.0 * tan(latitude_rad)), -HALF_PI, HALF_PI)
}

cryptochrome.emlchain 1

module cryptochrome;

const ONE_THIRD: Real = 0.3333333333333333

@verify(lean, theorem = "cryptochrome_yield_in_unit_interval")
fn cryptochrome_yield(B: Real, angle: Real, coupling: Real) -> Real
    requires (B >= 0.0)
    requires (coupling >= 0.0)
    ensures  (result >= 0.0)
    ensures  (result <= 1.0)
{
    clamp(ONE_THIRD + (2.0 / 15.0) * coupling
            * (3.0 * cos(angle) * cos(angle) - 1.0),
          0.0, 1.0)
}

compass_bearing.emlchain 1

module compass_bearing;

const PI: Real = 3.14159265358979

@verify(lean, theorem = "compass_bearing_in_full_circle")
fn compass_bearing(north: Real, east: Real) -> Real
    ensures (result >= -PI and result <= PI)
{
    clamp(atan2(east, north), -PI, 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 →