Verified photonic computing

How does light compute?

Light computes at 300,000 km/s. Matrix multiplication at the speed of a photon. Until now nobody has formally proven the photonic chip computes correctly. EML changes that. One source for the optics, the electronics, the controller — and the proof.

Mach-Zehnder

Drag the arm-phase difference. Watch the output snap from full transmission (logical 1) to total extinction (logical 0). The basic photonic logic gate.

I_out = I_in · cos²(Δφ/2)

✓ proven · energy conservation via Pythagorean

Ring resonator

Drag the wavelength. Watch transmission spike at resonance and dip into a Lorentzian off it. Photonic bandpass — the working element of every microring weight bank.

T(δ) = 1 / (1 + F · sin²(δ/2))

✓ proven · unity on resonance, FSR positive

4×4 MZI mesh

Six MZIs in the Reck triangle implement any 4×4 unitary. Watch a vector of light propagate through and become a matrix-multiplied output.

M = U₁ · D · U₂ — six independent (θ, φ) pairs

✓ proven · channel passthrough at identity-mesh

Photonic attention

One transformer attention head, hybrid: Q/K/V projections and the output projection on the photonic side, softmax + GELU on the electronic side. Watch the boundary.

Q,K,V = X · W   (photonic)   ·   A = softmax(QKᵀ/√d)  (electronic)

✓ proven · projection identity + softmax_uniform = 1/n

Poisson bright spot

Fresnel diffraction's most counter-intuitive moment: a bright dot in the centre of a circular shadow. The math was right when intuition said it was absurd.

I_axis(z) = I₀  (when the obstacle's Fresnel zone matches)

✓ proven · shadow centre = incident intensity

“The light does the math. EML proves it’s right.”

115 closed Lean proofs across the photonic computing stack — components (P1), neural network mesh (P2), manufacturing tolerance + closed-loop calibration (P3), and photonic-electronic co-design (P4). All build green against MachLib (Lean 4.14, no Mathlib). See the full carrier map →