[Deicyde]

The maintainer's ruling of 2026-11-12 splits the cut — which sentences are statements, and
where their edges are — from locate, whether Lean has them, and publishes the first alone.
This is the reader half of that design (section 3; decisions 1, 2 and 4 at their
recommendations). The store half is PRs 1–3.

An article built from a sealed statement set carries passages with outcome: "unchecked"
and no status, a fifth summary status not_checked in by_status and in the index shards,
checked: false, and a tagging universe — the libraries a community tag may name, which
nothing has searched.

The invariant under all of it: not_checked is never folded into not_formalized. They
are opposite claims — "no library has been searched" against "every library was searched and
nothing was found". The article page, /articles, the summary box on a Wikipedia article's
page and the dashboard's totals each count it apart, and the community overlay keeps it too:
a tag moves an unchecked statement's status as it moves any other passage's, but removing
every tag leaves it not_checked.

What a reader meets:

• a neutral highlight, not the absence of one: a translucent grey wash, a dashed grey
  underline and a horizontal-hatch swatch of its own, with a circle mark and the words "Not
  checked yet" in the markup, so the status is never colour alone. The builder's mark carries
  the passage's own outcome (data-status="unchecked"); the pages count the summary status
  (data-status="not_checked"); both paint the same, in light and in dark.
• the card: "Not checked yet — no library has been searched for this statement", with the Tag
  form under it and no Confirm/Report — those are a verdict on a sealed location, and there
  is none. It stays even after a community tag moves the status.
• the counts line "3 statements · none checked yet"; while nothing on a page is checked its
  passages are statements, in the counts line, the heading, the panel, the fab and the filter
  note (both scripts read a data-noun the server writes only on such a page).
• the legend gains the swatch and "What the colours mean" its row, both offered only where
  something is unchecked, so a page of checked passages gains no fifth column of zeros.
• /articles lists the article with "0 of 3 checked" and an empty status bar: the bar is how
  the checked passages came out, and a statement nothing searched for takes no share of it.
  The dashboard says both figures, and its importance table gains the column when the build
  has one.
• the About fold says which run cut it and that no locate run has run, and the libraries
  section says no library was searched and that these are the ones a tag may name. The
  universe page says the same for a build that searched nothing. The "Preliminary" notice is
  unchanged, and Lean still leads with provenance behind the fold.
• a statement-only article offers its view model and not records it has none of;
  /api/articles/records/:pageid answers 404 for an article whose view names none, which is
  not a damaged store.

POST /api/articles/tag needed no change to work there: it already checks the library
against the article's own universe and derives pair_key from that library's repo, so a
tag written in phase 1 is the same row as the pipeline's location in phase 2.

The home page's "passages checked" now excludes them, as it already excluded the passages
with no status.

The two halves, joined. wiki/test/articles-store-mixed.test.ts and
e2e/articles.spec.ts, "the built mixed store", serve
scripts/articles/fixtures/store-mixed — the store the Python builder writes from the
record-set fixture, the pipeline's sealed cut and that cut's marked revision, and whose bytes
scripts/articles/test_build_store.py rebuilds from those inputs byte for byte. Every other
fixture here is written by hand from the design, which proves the Worker reads the shape the
design names but not that the builder writes it; these read the builder's own output, so
neither half can drift. The store tree is committed on this branch and on the builder's,
identically: the Worker test has to read it where the builder does not exist, and the builder
test has to reproduce it where these tests do not run.

That store found one bug in code older than phase 1: a highlight's accessible name was built
from the store's quote, which the record format caps at twelve words, while the mark covers
the whole passage — so the name left out text the button shows (WCAG 2.5.3, Label in Name;
axe label-content-name-mismatch). The hand-written fixtures never caught it, because their
marks are exactly their quotes. The name is now the text every mark of the passage shows
(innerText, not textContent: the stored revision keeps each formula's TeX annotation,
which MathML never draws and a screen reader must not read out), with the store's quote kept
for a passage the revision leaves unmarked, and the e2e pins the rule.

Two more from the same review, both about a page of a store with nothing unchecked: the
relation legend is dropped only from a page of statements, never from a located article whose
every passage is an absence (it has no card either, and its page is the page it always was);
and the universe page's title, heading and breadcrumb follow its paragraph, so a build that
searched nothing no longer heads a page "The libraries searched" under a link that says a tag
may name them.

Release-affecting, so it ships only in a new release built at the new commit, with a
fresh P1B and Jack's approval (CLAUDE.md, "Deploy notes"). Cache keys and asset versions:
page:home:v14, articles.css?v=14, articles.js?v=9, articles-reader.css?v=7,
articles-reader.js?v=6, and the four changed entries of the public source attestation. No
new route, no change to RESERVED, the CSP, the noindex or the read budgets; the sealed view
model is untouched and still cacheable, and every page of a store without statements is
byte-identical.

Nothing is published by this PR. The store it reads is a fixture. The live store gains an
unchecked statement only when a statement set is built and uploaded, which is a separate
operator action after this ships — and the Worker should ship first, so that an upload is
never read by a Worker that does not know the status.

Tests: a statement-only store and a mixed one, written by hand from the design, in
test/helpers/articles.ts; the article page, the reader, the list, the dashboard, the box,
the universe page, the index shard's new column, the tag route (add, refuse an unknown
library, remove) and the located pages byte for byte unchanged in test/articles.test.ts;
the tag route on a statement-only article in the authz matrix; the builder's own store end to
end in test/articles-store-mixed.test.ts; and axe in light and dark, the keyboard, the
neutral highlight, the accessible name and the filter in e2e/articles.spec.ts.