Documentation surfaces: organize by audience, not chronology

[cameronfreer]

Tracking the documentation restructuring. Recorded now so it isn't lost; it is a separate track from the R4 mathematics and should not block the two-sided transport work.

Stable purpose per surface

Surface	Purpose
README	Developer-facing overview, major result families, build
Homepage	Short research pitch and navigation
Architecture page	Conceptual dependency layers and entry points
Blueprint	Complete theorem narrative and dependencies
API docs / module headers	Exhaustive technical detail
Issues / milestones	Live frontier and implementation status
Verification page	CI policy only

The organizing principle: by audience and mathematical layer, not chronology, PR sequence, or exhaustive declaration lists.

Planned work

• README — four theorem families, a 5–7 layer library map, verification policy, build/citation/license. At most one or two entry-point declarations per family; the blueprint and API docs carry the complete list. Drop the duplicated bibliography in favour of the blueprint bibliography.
• Homepage — two-sentence hero, four program cards, three or four highlights in prose rather than Lean identifiers, "Explore" links, and one evergreen development pointer. Delete the status strip and the "Current frontier" section, which is stale relative to the coherent-basis, factor, coupling, and rank-latent work already merged.
• Graphon.lean — the largest single opportunity. Measured: 245 lines carrying 113 module inventory bullets, duplicating module headers, issue numbers, historical decisions, and implementation gotchas. The imports already are the exhaustive inventory. The root docstring should carry what import Graphon exposes, a thematic map of ~8 clusters, and pointers to blueprint and API docs.
• docs/verification.md — policy only: what CI builds, placeholder rejection, exact audit scope, documentation/site checks. Dated proof history moves to issues or an explicit archive.
• Archive — docs/ currently holds five scoping/roadmap/planning documents (afkk-cut-guessing, overlay-scoping, post-r3-mainline-completion-plan, rokhlin-scoping, sampling-asymptotics-roadmap, sqmoment-cycle-krylov). Verified: nothing in .github/ or blueprint/ references them, so moving them under an archive directory is low risk.
• ARCHITECTURE.md — organized on the stable flow: measure infrastructure → graphon analysis and sampling → exchangeable graph laws → generic relational exchangeability → functional representation machinery → graph/digraph specializations.

Two caveats on the drift check

A structural check rejecting volatile status prose from landing pages is a good idea, but two refinements:

1. It must distinguish issue links from issue numbers in prose. docs: refresh README framing for the relational converse #166 deliberately adds links to R4: dissociated functional AHK for relational structures (AHK umbrella #103) #107 and ForMathlib: upstream candidates tracker #160 to the README, precisely so that live status lives in the tracker rather than being restated and going stale. A blanket ban on issue references would forbid the fix rather than the problem. The rule should target dates, audit counts, job counts, and quantified status claims — plus issue numbers used as history — while permitting links used as pointers.
2. "Zero sorry/admit" is not actually volatile, since CI enforces it; it cannot drift the way "21 sorries" could. The proposed phrasing — "CI rejects proof placeholders and audits designated headline declarations for their axiom dependencies" — is still better, because it survives a change in policy as well as in counts. Worth adopting for that reason rather than for staleness.

Note on Graphon.lean deletions

Some inventory entries carry cross-module reasoning (for instance why the rank layer is a Bool-cube rather than a dependent product, which spans RelRankSuccessor and everything downstream). Checked: that reasoning is already duplicated into the owning module's header, so deleting the Graphon.lean copy loses nothing. Any entry that turns out not to be duplicated should be moved into the owning module header rather than dropped.

Suggested as 3–4 small PRs rather than one sweep: Graphon.lean first (largest and most self-contained), then README/homepage, then verification + archive, then ARCHITECTURE.md and the drift check.

[cameronfreer]

Acceptance criteria and scope limits

Refining the plan. The framing that drives the rest: this is a mature formalization with an active extension, not a developing project whose README reports every milestone. The front-page contract is a review checklist, not a template to be applied rigidly.

Division of authority

Surface	Owns
README	Identity, stable capabilities, entry point, trust policy
Homepage	Reader-facing mathematical narrative
Blueprint	Complete results and proof dependencies
Module headers / API docs	Technical detail
Issues	Live status
ARCHITECTURE.md	Stable design

Acceptance criteria

1. Graphon.lean contains no PR history, issue-driven sequencing, or cross-module proof essays; anything unique moves to the owning module header.
2. README and homepage contain no hand-maintained progress metrics or milestone inventories.
3. The homepage's mutable "Current frontier" is replaced by a tracker link.
4. docs/verification.md states policy; dated narratives move under an archive.
5. ARCHITECTURE.md explains stable mathematical layers, not files or PRs.
6. The deployed site exposes its source commit.
7. Drift checks guard those structural rules while continuing to permit issue links used as pointers.

Explicitly not adopted

A general documentation review suggested a larger file split. Rejecting most of it, with reasons, so it does not get re-proposed:

• No STATUS.md — would duplicate R4: dissociated functional AHK for relational structures (AHK umbrella #103) #107 and drift.
• No RESULTS.md — the blueprint already serves that role.
• No ROADMAP.md — issues and milestones are the live roadmap.
• No CHANGELOG.md until there are meaningful tagged releases.
• No generated JSON carrying sorryCount or audit counts. I proposed this above; withdrawing it. CI is already the source of truth, no consumer needs the artifact, and it would restate project status in a second place — the exact failure this issue exists to remove.
• No duplicated Lean/Mathlib version strings — lean-toolchain and lake-manifest.json already own them.

The source-commit marker is different in kind and is retained (criterion 6). It reports the identity of the deployed artifact, not project status. That is what distinguishes "source updated but not built" from "built but not deployed" from "deployed but not indexed" — an ambiguity that has already cost one manual investigation, when an external report of stale sorry text on the homepage turned out to be crawler lag rather than a deployment failure (home_page/index.md contains no such text).

Note on the homepage

External praise for the current homepage is snapshot-accurate but not maintenance-accurate: its hand-written "Current frontier" has already fallen behind the merged R4 work. That is the argument for criterion 3 — not that the section is badly written, but that any hand-maintained frontier section will drift by construction.

Net effect: fewer sources of truth, without manufacturing a documentation bureaucracy.