Read this before you screenshot anything

How to read this site

1op interleaves three genuinely different kinds of claim under one visual language: a machine-checked theorem, a reproducible measurement, and an exploratory model that asserts nothing formal at all. Nothing on the page used to distinguish them. This does.

Every exhibit carries exactly one badge below. Every badge but Play links to its own evidence — a real ledger theorem, a real dataset or script, or an honest scope statement. A build-time check (scripts/audit-badges.ts, wired into CI) fails the deploy if a “Proved” badge doesn’t resolve to something real. Default tier for any new exhibit is Model — Proved has to be earned.

Proved

Machine-checked: a real ledger headline, zero sorryAx. Click through to the proof.

Example: The Barrier (Depth Ladder, level ∞) — No finite tree of exp and ln reaches sin(x) over the reals — machine-checked in Lean, zero sorryAx, proved three separate ways.

Measured

Empirically computed and reproducible. Not a theorem -- click through to the data or script.

Example: SuperBEST's 80.8% savings — A real, reproducible cost-table computation. Not a theorem — click through and the same table is right there.

Model

Exploratory structure. No empirical or formal claim -- click through for the exact scope.

Example: Senses (animal perception sketches) — Exploratory EML-shaped structure. Not biological proof, not hardware validation — the scope statement says so directly.

Play

Makes no claim. Art, games, and sandboxes -- nothing here to substantiate.

Example: Zen Garden — Draggable nodes and domain coloring. It isn't asserting anything, so it doesn't carry a claim to substantiate.

The full machine-checked ledger this site draws “Proved” claims from lives at monogate.org/theorems. Forge-sourced kernel proofs (the waves carrier demos, the Proved Controller) link straight to their .lean file in agent-maestro/forge.