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.