End-to-end
Every other gate here checks a source: the Lean compiles, the ledger chains, the prose cites live keys. This checks the artefact a reader opens, and this page is its output — so it cannot describe a check that did not run.
Last run: 9 of 9 passed.
| check | result | measured |
|---|---|---|
| the formulas page is built | ✓ | built |
| it references the data file rather than embedding it | ✓ | under the 200 KB limit and references formulas.jsonld: true |
| the data file parses as JSON-LD | ✓ | parses |
| it declares the schema.org context | ✓ | ["https://schema.org",{"wing":"https://schema.org/genre","source":"https://schem |
| it is an ItemList | ✓ | ItemList |
| numberOfItems matches what the list holds | ✓ | declared 26197, holds 26197 |
| the page and the data agree on the count | ✓ | page says 26197, data holds 26197 |
| every linked theorem page is built | ✓ | 1455 links, 0 dead |
| every item carries the three facets the widget filters by | ✓ | 26197 of 26197 complete |
What this cannot tell you
It reads built files, not a browser. It cannot tell you the filter responds to a keystroke, or that the layout holds at phone width — only that the page references its data, that the data parses as schema.org, that the counts agree, and that every address the page offers a reader resolves to a page that exists.
Browser behaviour was confirmed by hand on 2026-09-25 — the filter narrowing 1,192 to 24 on "reflection", and showing "nothing matches that filter" rather than an empty page on a term with no hits — and is recorded here as confirmed by hand, not as covered by this check.