What does a cat see?

Biological vision modeled in EML. Mathematically verified.

Four-panel comparison of human and cat vision in daylight and 5% illumination

human (daylight) · cat (photopic) · human (5% light) · cat (5% light, tapetum scotopic)

Human — full daylight

Cat — full daylight

Light level: 100% · full daylight

1% near-dark30% scotopic kicks in100% daylight

Upload your photo

The math behind the cat's eye

Four equations in EML — Monogate's mathematical equation language. Each function carries a @verifycontract that compiles to a Lean theorem about its bounds. The same source compiles to C, Verilog, HLSL, and 28 more targets. View the Lean proof →

rod_sensitivity.emlchain 1

module rod_sensitivity;

const ROD_PEAK_NM:  Real = 498.0
const ROD_SIGMA_NM: Real =  50.0

@verify(lean, theorem = "rod_sensitivity_bounded_unit")
fn rod_sensitivity(wavelength_nm: Real) -> Real
    where chain_order <= 1
    ensures (result >= 0.0)
    ensures (result <= 1.0)
{
    exp(-((wavelength_nm - ROD_PEAK_NM) * (wavelength_nm - ROD_PEAK_NM))
         / (2.0 * ROD_SIGMA_NM * ROD_SIGMA_NM))
}

cone_s.emlchain 1

module cone_s;

const CONE_S_PEAK_NM:  Real = 450.0
const CONE_S_SIGMA_NM: Real =  30.0

@verify(lean, theorem = "cone_s_sensitivity_bounded_unit")
fn cone_s_sensitivity(wavelength_nm: Real) -> Real
    where chain_order <= 1
    ensures (result >= 0.0)
    ensures (result <= 1.0)
{
    exp(-((wavelength_nm - CONE_S_PEAK_NM) * (wavelength_nm - CONE_S_PEAK_NM))
         / (2.0 * CONE_S_SIGMA_NM * CONE_S_SIGMA_NM))
}

cone_l.emlchain 1

module cone_l;

const CONE_L_PEAK_NM:  Real = 554.0
const CONE_L_SIGMA_NM: Real =  50.0

@verify(lean, theorem = "cone_l_sensitivity_bounded_unit")
fn cone_l_sensitivity(wavelength_nm: Real) -> Real
    where chain_order <= 1
    ensures (result >= 0.0)
    ensures (result <= 1.0)
{
    exp(-((wavelength_nm - CONE_L_PEAK_NM) * (wavelength_nm - CONE_L_PEAK_NM))
         / (2.0 * CONE_L_SIGMA_NM * CONE_L_SIGMA_NM))
}

tapetum.emlchain 1

module tapetum;

const TAPETUM_PEAK_NM:   Real = 500.0
const TAPETUM_SIGMA_NM:  Real =  70.0
const TAPETUM_BASE_GAIN: Real =   1.0
const TAPETUM_MAX_GAIN:  Real = 130.0

@verify(lean, theorem = "tapetum_amplify_monotone_bounded")
fn tapetum_amplify(input_intensity: Real, wavelength_nm: Real) -> Real
    where chain_order <= 1
    requires (input_intensity >= 0.0)
    ensures  (result >= input_intensity)
    ensures  (result <= input_intensity * 130.0)
{
    input_intensity * tapetum_gain(wavelength_nm)
}

This biological model is mathematically verified.

The EML→Lean pipeline emits a theorem statement for each @verify annotation; one obligation (rod_sensitivity ≥ 0) is discharged against MachLib foundations and passes lake build. The remaining bounds follow the same pattern.

See the experiment on GitHub →