Verified photonic computing · component 2/5

Ring resonator

A microring resonator is a tiny optical loop — light circulates inside it, and at certain wavelengths the round-trip phase comes back in step with itself. Those are the resonances. Drag the round-trip phase below; watch the transmission curve trace a Lorentzian dip.

Round-trip phase δ = 0.00 radFinesse coefficient F = 60 — sets how sharp the Lorentzian dip is

The math

fn transmission(delta: Real, finesse: Real) -> Real
    requires (finesse >= 0.0)
{
    let half = sin(delta * 0.5);
    1.0 / (1.0 + finesse * (half * half))
}

@verify(lean, theorem = "ring_resonator_unity_on_resonance")
fn transmission_on_resonance(finesse: Real) -> Real
    ensures (result == 1.0)
{
    1.0 / (1.0 + finesse * (sin(0.0) * sin(0.0)))
}

✓ unity transmission on-resonance + FSR positivity, closed against MachLibView source on GitHub →

← All photonic demos