10.1.2 Classification by independent replay evidence
Replay classes record the independent evidence available before retirement. They are retained as provenance; the current Lean trust tier is read from the fresh capstone axiom closure.
- N1
14 families; 1,169 of 1,169 atoms replayed. Complete exact independent replay.
- N2
1 family; 189 of 189 atoms replayed. Partial exact independent replay.
- N3
0 families; 0 of 0 atoms replayed. Manifest/source-shape or transport audit only.
The external replay layer has literal full-range adapters for 1,371 of 1,371 historical atoms across 15 families. Adapter capability means that the complete computation can be requested; it does not claim that every expensive production run was completed on this development machine.
The recorded complete production executions cover 1,358 of 1,371 historical formerly-native atoms. The remaining atoms may have bounded samples, but samples are not described as complete independent re-execution.