# Alpha v21 advanced constructive-layer closure receipt

The unchanged original intuitionistic kernel independently accepted every
ordinary proof node of the complete Alpha-v21 additive constructive campaign.

| Exact independent-check measurement | Value |
| --- | ---: |
| Immutable Alpha-v20 parent theorems | 1,776 |
| Unchanged Stable theorems | 432 |
| Newly checked constructive theorems | 54 |
| Arbitrary coded matrix theorem rows | 23 |
| Euclidean execution theorem rows | 15 |
| Binary modular exponentiation theorem rows | 16 |
| Historical prerequisites in complete proof cone | 154 |
| Actual theorem proof nodes | 208 |
| Unenrolled balanced conjunction roots | 1 |
| Independently kernel-checked bundle nodes | 209 |
| Theorem-only local dependency edges | 464 |
| Complete local dependency edges | 491 |
| Ordinary structural proof nodes | 10,304 |
| Canonical complete proof-bundle bytes | 1,005,317 |

Frozen canonical proof artifact:

```
research/arithmetic-library/artifacts/alpha-v21-advanced-layer-proof-bundle-v1.json
SHA-256 65ecae7cb6b3e102790efa281451db3da5ab83868afcf9d57e6656f7a3eafda0
```

The separately compiled Lean proof-bundle verifier also independently
accepted the same exact ordinary proof artifact:

```
../peano-lab-lean/.lake/build/bin/peano_lab_bundle_verify \
  research/arithmetic-library/artifacts/alpha-v21-advanced-layer-proof-bundle-v1.json
ACCEPT  nodes=209  root=208
```

The Alpha-v21 release builder reruns this independent compiled verification
before it emits any catalog or grants any Lean-verification metadata.

Actual historical body sources are 132 fully embedded original proof bodies
from the immutable Alpha-v19 frontier artifact, nine from its immutable
residual artifact, and 13 from the immutable Alpha-v20 artifact. No theorem
body is replaced by a digest, historical name, trusted reference, unchecked
statement, new axiom, or external solver.

The sealed exact ordered theorem-cone SHA-256 is
`4412c3b3b3d7479bbc5423e335e359fadbb5c006fe8b92248065f2839bb9ae20`.
The ordered 54-row additive enrollment SHA-256 is
`cbf76fb45efbae79a2b1cd2c7fc3cf806a6f8ebc593a5fceee6f5bea7cd734f5`.

All 27 maximal endpoints are joined only for packaging by an ordinary
balanced conjunction whose body is itself checked by the unchanged kernel.
This synthetic root is not enrolled as a theorem.

T13, G101, and G102 remain open in their exact blueprint formulations.
The new proofs establish complete arbitrary signed matrix multiplication,
but not arbitrary-dimensional determinants/rank/lattices; genuine Euclidean
two-step halving and complete histories with independently certified gcds,
but not terminal-state identification plus a formal bit-length bound; and
correct square-and-multiply transitions plus unique bounded modular outputs,
but not the combined object-language execution/bit-length complexity theorem.