Verified photonic computing · component 1/5
Mach-Zehnder interferometer
Two arms. One photon. The relative phase Δφ between them drives the output between full transmission (logical 1) and total extinction (logical 0). Drag the slider to step through every angle from 0 to 2π and watch the cos² transfer function trace itself out.
0 — full throughπ — full drop2π — full through
The math
fn through(i_in: Real, delta_phi: Real) -> Real {
i_in * (cos(delta_phi * 0.5) * cos(delta_phi * 0.5))
}
fn drop(i_in: Real, delta_phi: Real) -> Real {
i_in * (sin(delta_phi * 0.5) * sin(delta_phi * 0.5))
}
@verify(lean, theorem = "mzi_energy_conserved")
fn energy_witness(theta: Real) -> Real
ensures (result == 1.0)
{
sin(theta) * sin(theta) + cos(theta) * cos(theta)
}✓ energy conservation closed via direct application of MachLib.pythagorean.View source on GitHub →