Playground

Research-derived audio + visual demos: Bessel FM synth (the math behind FM synthesis), math-as-melody chord stacks, Pfaffian phase portraits. Self-contained exhibits from the latest exploration sessions.

Flagship

Bessel FM Synth

Slide the modulation index — the bar chart IS the Bessel function. The math behind every '80s pop song.

Flagship

Math as Melody

Every AST has a chord. Click an expression — chain orders sum into pitch stacks. Ai(x)·Γ(x) rings as a maj9.

Pfaffian Phase Portrait

Four chain-3 towers, one cubic-phase outlier. Slide x — Airy explodes while Bessel and friends stay tame.

Additive Synth

Every saw / square / triangle is a sinc-truncated Fourier series. The T_Si tower in the path of every D/A converter.

Lean Dependency Graph

See the structure of 562 declarations across monogate-lean. Click any node to walk the proof dependency tree. Sorries highlighted in red — open frontiers visible at a glance.