Progress

The Statistics page measures volume: lines of Lean per roadmap, pull requests merged, reviews written. This page measures something else, how far each roadmap has got against its own specification, and it describes coverage of the roadmaps that exist, not how much of mathematics has been formalized.

Three kinds of evidence go into the board, and they are kept apart:

• Layers are the headings of the human-written roadmap README.md: layers, lanes, parts or stages. They do not move when code lands. Nothing here turns them into a percentage, because layers differ in size and a partial layer is not known to be half done. “Layers reported done” is a count of headings. A roadmap whose README names its milestones some other way has no layer inventory here, which says nothing about its work.
• Layer states are read from the roadmap's generated STATUS.md, the report that TauCetiProgress writes after each window of merged pull requests. “Reported done” means that report, describing the library at the commit named in its header, says the layer's milestones are proved. It is a model's account of the work, not security-validated, and not a certificate that every sentence of the layer's specification is met. Where a report says nothing about a layer, the layer is unassessed; so is every layer of a roadmap with no report yet. When a README is edited after its report but still names the same layers, the report's states stay on the board, marked “README changed” and counted as due an update, until the next report assesses the README as it now stands; a README that adds, removes or renumbers a layer leaves its layers unassessed until then. A sub-roadmap's README change also marks its umbrella's row, whose totals count the sub-roadmap's states, and when the two share a report, that one report is counted as due.
• Activity is mechanical: pull requests merged under the roadmap's roadmap/<Area> label, the same attribution the Statistics page uses, counted up to the stated cutoff. A pull request with no roadmap label, or more than one, is counted in the global figures but assigned to no roadmap.

The formal declarations behind all of this are checked by Lean in the usual way; the board adds no checking of its own. A roadmap marked declared complete is one the maintainers have archived as complete against its README. That is a human judgment, shown beside the report's layer assessment rather than replacing it, and the two can disagree.

A report always lags the library, because it describes the last published documentation build, so its age alone is not a signal. The board marks a roadmap as due an update once ten or more pull requests have merged since its report, the threshold TauCetiProgress itself uses to open a new window; that is a heuristic, not a guarantee that nothing relevant changed below it. The umbrella roadmap for representation theory is reported as one unit, so its sub-roadmaps share its report and its label.

The topic grouping is a hand assignment kept beside the generator. So, for now, are the layer states: TauCetiProgress does not yet write them in a machine-readable form, so the generator reads a companion file transcribed from each report's prose, bound to the exact report and the exact README it was read against. When either changes, the transcription is retired and the layers go back to unassessed until it is read again. The intended replacement is a tauceti-coverage:v1 marker beside the report's header, naming the roadmap, the library commit, the README it assessed (a hash), and one line per layer with its state and a one-line note of what remains, validated by the same script that validates the rest of a generated report. That is what this page will accept, offered as a proposal rather than an agreed format; the generator prefers such a marker whenever one is present and fits, and leaves a marker that does not name its README unassessed rather than applying it to whatever README is current. Open pull requests carrying a roadmap's label are counted beside its merged ones, as work in flight that no report describes yet, and where someone has published a map or write-up of a single roadmap, its row links to it.