source/math_map.md is landed verbatim and never edited. Its upward corrections live here, as an overlay that scripts/mathmap.mjs applies when it parses the map. Every query, composite and report sees the overlaid map; --landed shows the original, and every entry carries its origin (map, fill, clone:
Three kinds of pointer stand in for content in the landed map:
Counted honestly (a pointer is not a type), 1,118 of the 1,954 landed entries can anchor a composite.
Clone resolution (computed). A pointer resolves by explicit id, else by name in the named domain, else by name in the ISO home domain, else to the one solid entry of that name anywhere (marked “by name”). Chains are followed. A pointer whose home does not exist is dangling.
Authored fills. d7-*.js fill every D7 stub. homes.js writes each missing home once (79 homes: SVD, PCA, the Z-transform, Johnson-Lindenstrauss, Delaunay and the rest) and attaches it to every entry that points at it. Each fill names its entry by id and by the map’s exact name, so a fill cannot land on the wrong entry, and the check refuses a fill over an entry that has content of its own.
A fill is authored: written from standard mathematics, from memory, and not reviewed against sources. The map’s own status fields (Unformalized, Unvalidated, Unreviewed) still apply. A fill with a reading names an ambiguous or nonstandard entry and says how it was read. A fill whose fields are “Unknown” records an entry that could not be identified (D7-271, D8-199); it stays unusable as an anchor rather than carrying invented content.
The D7 mapper report (source/Category_Theory_Transformation_Enumeration.pdf) gives names only in its enumeration (“formatted strictly as names”), and types for about 25 transformation classes in its prose tables (functors, adjunctions, universal constructions, completions, the Grothendieck construction, free algebras, quotients, subdirect decomposition, Knuth-Bendix, resolutions, derived functors, spectral sequences, the mapping cone, integral transforms). The fills agree with those tables; everything else is authored here.
additions.js holds entries the map lacks, written because a composite needs them (ids in a series the map never uses: D<n>-X<nn>). Unlike fills, each addition is receipted: every claim that carries weight has a verbatim window in excerpts/, and scripts/mathmap.mjs checks that each quote occurs in its file. Additions carry origin added and are counted in the domain totals; the audit’s sample never draws them.
corrections.js replaces landed fields that a check found wrong or imprecise: an audit grade, a flag, or a Mathlib link graded conflicts. Every corrected field is supported by a receipt in excerpts/ (Wikipedia windows are taken from a pinned revision with scripts/excerpt.mjs), claims that cannot be receipted are dropped and the reason says so, and the landed text stays on the entry. Correcting all five content fields of a flagged entry resolves its flag. Hypotheses an entry leaves out go in conditions.js instead.
domains.js declares domains the landed map lacks (D9, systems and effects) with the tags their entries use. generated.js holds entries landed from a graded generation round (generation/): design contracts written by a generator, checked here for consistency (known invariants and carriers, nothing both kept and broken, tags in the vocabulary, a round with a grading) and carried at their own tier, generated, with every claim starting unchecked. A generated entry becomes an addition only when its claims are receipted.
The D9 entries carry one context label in invariants.js, compartment-context, for the per-process contamination rule the operator ruled for the Phone (a process that has read a compartment’s data emits as that compartment until reset): raised by the entries that bring labeled data in, forbidden at every entry that may break E9-NOEGRESS, cleared by none. It is coarse on purpose and catches what explicit-flow checkers miss, a decision taken on the data.
android.js binds the D9 entries to Android APIs at one pinned AOSP tag, from the MM-DR-002 round. Each binding grades the platform primitive and the whole D9 contract separately (enforced, monitored, unknown, not observable); its sources are hash-only rows of files read at the tag, five of whose hashes this repository’s grading fetched and reproduced. Where the grading added a fact the generator missed, it sits in gradingNote, apart from the generator’s text.