9.2 Two orthogonal classifications
The generated family catalog below classifies every one of the 1,371 live native atoms in two ways. Its five computation architectures say what the checker does: exact finite folds and sweeps, fixed-point accumulators, rational/logarithmic ladders, compact interval or parameter grids, or a mixed interval-and-sieve computation. These classes partition all fifteen families. They expose arithmetic and checker structure; they are not grades of logical trust.
The second classification records independent replay evidence:
- N1
every exact native predicate in the family has a recorded complete external production replay;
- N2
some, but not all, exact predicates in the family have a recorded complete production replay; and
- N3
no predicate in the family is currently credited with a complete exact external replay.
At this revision, literal full-range Python/GMP adapters cover all 1,371 atoms in all fifteen families. N1 records complete runs for fourteen families and 1,169 atoms; N2 adds 189 of the 202 Helfgott analytic atoms. Thus complete production executions cover 1,358 of 1,371. The remaining thirteen wide Appendix trees are implemented but have only bounded, explicitly non-production samples because each full run is projected to exceed one hour. N1, N2, and N3 all retain the NATIVE badge because an external replay corroborates an axiom but does not remove it from the Lean term. The machine-readable authority for this editorial classification is the native-decision classification; generation fails if its families, totals, replay states, or ledger anchors disagree with the exact live manifest. The repository records deterministic transcript digests and runtimes rather than raw machine logs. Those records are reproducibility targets, not cryptographic proof that a historical process ran; independent authentication requires rerunning the stated command against the pinned inputs.