A typed map of mathematical transformations. Each entry gives an operation’s input, output, preserved invariants and broken invariants, with functional tags from a controlled vocabulary. Every entry states where its content came from and how far it has been checked, and every field carries its own evidence level, so a use of the map can go only as far as its evidence does. Chains of entries compose: a checker reports whether each join fits, which invariants survive, and the weakest claim the chain rests on.
The machinery is general. The map is data: a landed source kept verbatim, an overlay that fills, corrects, adds and links it, and audit grades. Domains, entries, invariants and their bindings to platforms are rows in that data; the parser, evidence levels, composition checker, build and query tools work over whatever rows are there. One domain, systems and effects, holds operation contracts for software that the same checker composes, with bindings to platform primitives.
What is in the map, as counts derived from its data, is in STATUS.md, regenerated by the build. The fill layer’s design is mapfill/README.md.
Every entry states where its content comes from:
source/math_map.md, verbatim).excerpts/.mapfill/generated.js), landed at its own tier with the round recorded.Each entry carries a tier, strongest evidence first: flagged (known wrong, withheld from use), audited (graded field by field against cited sources; the worst verdict is shown), receipted (an addition whose every claim is quoted), landed (as written, not reviewed), authored (a fill, not reviewed), generated (from a graded generation round, not reviewed field by field; its claims start unchecked). A stronger tier is earned by evidence, never assigned. A flag withholds an entry from use and never rewrites it.
Entries may also carry conditions (the hypotheses their claims need) and counterexamples, each receipted like an addition (mapfill/conditions.js).
Entries of the systems domain can be bound to the platform primitives that would realize them: Android APIs (mapfill/android.js) and NixOS options, systemd unit settings and kernel features (mapfill/nixos.js), each at a pinned source release. A binding grades the platform primitive and the whole contract separately (enforced, monitored, unknown, not observable) and cites hashed source files. Bindings are generated claims from a graded round; none is a device or host test.
scripts/export-guardians.mjs exports the systems entries as tool specifications for Guardians (github.com/metareflection/guardians, MIT), and a personal policy (--source ID=label --forbid label) as its taint rules, so an existing checker verifies agent workflows against the map’s contracts. Relational and hyperproperty invariants and flows through branching stay outside it.
Free-text fields say what an entry preserves and breaks; mapfill/invariants.js names those invariants, with the relations between them, gives each a carrier (the kind of object that has it), records what kinds of object each linked entry takes and returns, and links entries to invariants. Each link is justified by a phrase in the entry’s own field or, where the entry is silent, by a receipted quote with a note. The vocabulary grows by use.
node scripts/compose.mjs --chain D2-118,D2-117 reports, for a chain of entries applied in order, whether each join fits (match, narrowing, partial: an input the previous step does not supply, or mismatch: an unstated conversion), and which invariants survive, break, are restored or created, judged only at the steps that act on their carrier. A step’s input kinds are joint operands, and an implication between invariants carries claims only when it relates preservation itself. Silence means the map does not say; the invariant is then reported as unknown.
Every field of every entry, and every named-invariant claim, carries an evidence level, weakest first: contradicted (a check found it wrong and it is not yet corrected), unsupported (checked; no source supports it), unchecked (never checked), imprecise (right idea, a detail wrong), sourced (a verbatim quote supports it), formal (Mathlib or this repository’s Lean project states it). scripts/evidence.mjs computes them from the audit grades, receipts, corrections and formal links. The composition checker reports, for every result and join of a chain, the weakest claim it rests on and where it is, so verification can go where a chain is weakest.
mapfill/corrections.js replaces landed fields that a check found wrong or imprecise with receipted text; the landed text is kept on the entry (corrected.landed). A correction needs a prior finding (an audit grade, a flag, or a Mathlib conflict) and a receipt for every field it changes. Correcting every field of a flagged entry resolves the flag. The audit’s error rates still describe the map as landed.
mapfill/formal.js links entries to declarations in Mathlib at a pinned commit. Each link names the field it bears on and grades the match: exact (Mathlib states the claim), general (Mathlib states something that implies it), special (a special case), related (a weaker or neighbouring result; the claim itself is not formalized), ingredient (the objects, not the claim), or conflicts (Mathlib’s statement conflicts with the claim as written; the note says how). The declaration statements are quoted in excerpts/mathlib-*.txt with the hash of each file at the pin; node scripts/formal.mjs --verify refetches them. A link says Mathlib proves the quoted statement, which its CI type-checked at that commit; the grade of how it bears on the entry is a judgment, like an audit grade. reports/FORMAL-QUEUE.md lists unreviewed name matches still to be read, and lean/WISHLIST.md what the claims need from Mathlib and do not find there.
lean/ is a Lean 4 project on the same pinned Mathlib. It states and proves claims of entries that Mathlib does not cover, over definitions of its own. mapfill/lean.js registers each definition with receipts from its source and each claim with the entry, field and invariant it bears on. Whether a claim is proved or only stated is read from Lean itself: node scripts/lean.mjs --audit runs #print axioms (a proof that uses sorry is only stated) and lists the definitions each statement depends on, all of which must be receipted; the result is lean/AUDIT.json, which CI regenerates after lake build and compares. A proved exact claim makes its invariant claim, or its whole field, formal. To build: cd lean && lake exe cache get && lake build.
audit.json holds field-by-field grades (confirmed, imprecise, wrong, unsupported) against cited sources: a fixed random sample, kept for unbiased error rates, and targeted grades for entries chosen for use (composites) or for citation (entries with a Mathlib counterpart), kept out of the estimates. Entries found misaligned are flagged with their evidence (mapfill/flags.js).
Sources, edited by hand and checked:
source/math_map.md: the map as landed, verbatim. source/Category_Theory_Transformation_Enumeration.pdf: the report the D7 names come from.mapfill/: the fill layer (clone resolution, authored fills, missing homes, flags), the additions (mapfill/additions.js), conditions, the invariant vocabulary, and the Mathlib links (mapfill/formal.js). See mapfill/README.md.audit/: the fixed sample, its grades, and the targeted receipts.excerpts/: the verbatim windows that receipt the additions, each with its source URL and the hash of the page or PDF as fetched. Quoted for reference; the sources keep their own licences.scripts/: the parser and query tool (mathmap.mjs), the composition checker (compose.mjs), the evidence levels (evidence.mjs), the Mathlib links (formal.mjs), the excerpt maker (excerpt.mjs), the MCP server (mcp.mjs), the Guardians export (export-guardians.mjs), the topology of the typed map (topology.mjs), the free typing pass (type-lexicon.mjs), the gap finder (gaps.mjs), the deformation generator (deform.mjs: exact Lie algebra cohomology, integration and contraction, with its algebras and rounds in deform-algebras.mjs); the HISTORY-001 round, retrodicting paradigm transitions under pre-registered controls, in deform-history.mjs), the audit (audit.mjs), this build (build.mjs), and the gate (check-all.mjs). Node 18 or later, no dependencies..infra/: the vendored Repo-Infrastructure kit, pinned by infra.lock.json and configured by infra.json. node .infra/run.mjs runs its checks, and check-all.mjs runs it. repo-map-manifest.json describes every directory and every file that has no Role header.Generated by node scripts/build.mjs, never edited by hand:
map.json: every entry, machine-readable. domains/D1.md to domains/D9.md: the same, readable. audit.json: the grades with their quotes and sources.README.md, this design, and STATUS.md, what the map holds as counts from its data, dated by the commit it was built from.reports/MATHMAP.md and reports/AUDIT.md: data quality and error rates (written by mathmap.mjs and audit.mjs).MANIFEST.json and SHA256SUMS: the source commit and file hashes, so an answer that cites this map can cite the exact version.Generated by node .infra/tools/repo-map.mjs: REPO-MAP.md, every directory and file with a one-line description, and the edges between files (imports, and paths a file names). The kit’s repomap check fails when a file is undescribed or the map is stale.
node scripts/mathmap.mjs --text quotient --domain D4 --full prints matching entries. Flags: --id, --domain, --tag, --kind, --text, --origin, --stubs, --limit, --full, --landed.
scripts/mcp.mjs serves the map over the Model Context Protocol on stdio, with no dependencies. Tools: map_info, search_entries (by text, domain, tag, kind, tier or named invariant), get_entry, list_invariants and compose_chain. Every answer carries the commit the map was built from, so a model’s citation names an exact version. To add it to Claude Code: claude mcp add math-map -- node /path/to/Math_Map/scripts/mcp.mjs. Other clients take the same command in their server configuration:
{ "mcpServers": { "math-map": { "command": "node", "args": ["/path/to/Math_Map/scripts/mcp.mjs"] } } }
The map’s data (the landed map, the fill layer, additions, conditions, invariants, audit grades and generated files) is licensed under CC BY 4.0; the scripts are under the MIT licence. See LICENSE. The excerpts in excerpts/ are short quotations from their sources, which keep their own licences (Wikipedia text is CC BY-SA; arXiv papers and the nLab under their authors’ terms).
A change to a field needs evidence: an addition or a correction carries receipts (verbatim quotes in excerpts/), and a grade carries a quote from its cited source. node scripts/check-all.mjs must pass.