What the map holds against the design in README.md, as of 2026-10-14 (built from commit 30646836d4f1b1e167286395195589e7f1e9dbdc). Generated by node scripts/build.mjs from the data; never edited by hand.
2052 entries in 9 domains: the 8 the landed map declares, and D9 (systems and effects), added in mapfill/domains.js. 2049 have full types and invariants.
| Axis | Counts |
|---|---|
| Origin | map 1100, clone 329, fill 525, added 59, generated 39 |
| Tier | landed 1337, audited 116, authored 494, receipted 65, flagged 1, generated 39 |
| Field evidence | contradicted 0, unsupported 100, unchecked 11206, imprecise 20, sourced 912, formal 74 |
| Invariant-claim evidence | contradicted 0, unsupported 0, unchecked 433, imprecise 0, sourced 29, formal 20 |
Conditions: 10 entries. Corrections: 22 entries. Flags: 7 recorded, 6 resolved by corrections, 1 still withheld.
Named invariants: 56 in the vocabulary, linked to 20 entries.
60 entries in the fixed random sample (seed 20260929), 58 targeted grades. Error rates are in reports/AUDIT.md.
Mathlib pinned at 380f2aafb622cb2c1c93dac545b6389083c68c51: 173 links on 85 entries (exact 116, conflicts 4, related 12, special 17, general 17, ingredient 7).
Lean (leanprover/lean4:v4.35.0-rc3): 45 claims on 12 entries, 45 proved and 0 stated, over 36 receipted definitions.
Android: 51 bindings at AOSP android-16.0.0_r4 (build BP4A.251205.006), over 81 hashed source files, from round MM-DR-002.
NixOS: 38 bindings at nixpkgs 7c8764b (nixos-26.05, kernel 6.18.55, systemd 260.5), over 60 hashed source files, from round MM-DR-004.
reports/FORMAL-QUEUE.md. Notions Mathlib lacks: lean/WISHLIST.md.