10.1.1 Classification by computation architecture
The live capstone has no native families: all formerly native families retired from its axiom closure. The following five classes retain the historical architecture catalog used to audit that retirement; they are not current NATIVE dependencies.
- Exact finite folds and sweeps
41 retired historical atoms in 8 families. Bounded iteration over primes, prime powers, Moebius or Liouville values, or exact integer/rational recurrences. These checkers do not infer an unbounded analytic statement; ordinary Lean supplies the range theorem or continuation after the finite endpoint.
- Fixed-point accumulator certificates
7 retired historical atoms in 1 family. Integer accumulators with an explicit scale and directed rounding encode finite rational sums or products. The scale, terminal state, and comparison are part of the closed proposition.
- Rational and logarithmic ladder enclosures
1,025 retired historical atoms in 1 family. Linked rational checkpoint inequalities and outward logarithm enclosures cover a long range by overlapping steps. The large atom count comes mainly from deliberately small reviewable shards.
- Compact interval and parameter-grid inequalities
230 retired historical atoms in 4 families. Exact rational interval evaluation, bisection, derivative bounds, or finite parameter grids certify inequalities on compact cells. Soundness theorems transport successful cells to the real or complex analytic expression.
- Mixed interval and sieve certificates
55 retired historical atoms in 1 family. A single mathematical family combines compact rational interval cells with exact finite sieve or product folds, so neither a pure interval nor a pure arithmetic label describes every member.