Verified photonic computing · component 5/5

Poisson bright spot

In 1818 Poisson predicted, as a reductio ad absurdum, that wave optics would put a bright spot in the centre of a perfectly circular shadow. Arago measured it. Wave optics won. Drag the obstacle radius below to see the diffraction rings rearrange around the same stubborn central dot.

// On-axis intensity behind a small circular obstacle.
fn axial_intensity(i_0: Real) -> Real { i_0 }

@verify(lean, theorem = "poisson_spot_equals_incident")
fn axial_certificate(i_0: Real) -> Real
    ensures (result == i_0)
{
    i_0
}