Verified photonic computing · component 3/5

4×4 MZI mesh

The Reck decomposition writes any 4×4 unitary as a product of 6 MZI rotations arranged in a triangle. Drag the manufacturing tolerance to see how small per-MZI phase errors compound through the mesh — the calibration loop's job is to drive that error back to zero.

Manufacturing tolerance = 0.00 — scales the per-MZI phase error band

0 — perfect fab0.5 — calibration target1.0 — out of spec

The math

// 4x4 Reck triangle: 6 MZIs implement any 4x4 unitary.
const MZI_COUNT: Real = 6.0   // N*(N-1)/2 for N=4

@verify(lean, theorem = "mzi_mesh_4x4_six_rotations")
fn mzi_count_certificate() -> Real
    ensures (result == 6.0)
{
    4.0 * (4.0 - 1.0) * 0.5
}

@verify(lean, theorem = "mzi_mesh_4x4_channel_1_identity_passthrough")
fn channel_1_identity_certificate(a1: Real) -> Real
    ensures (result == a1)
{
    a1 * cos(0.0) * cos(0.0) * cos(0.0)
        * cos(0.0) * cos(0.0) * cos(0.0)
}

✓ MZI count = 6 + channel-1 identity passthrough closed against MachLibView source on GitHub →

← All photonic demos