# Alpha v22 constructive transport closure receipt

The immutable parent is the fully original-kernel-checked 1,830-theorem Alpha
v21 edition. Every additive theorem is dependency-closed, represented by its
actual first-order statement and ordinary constructive proof body, and checked
by the unchanged intuitionistic proof kernel.

The self-contained artifact is
`research/arithmetic-library/artifacts/alpha-v22-transport-layer-proof-bundle-v1.json`.
Its final conjunction is a synthetic packaging root, not an enrolled theorem.
Historical parent proof artifacts are opened one at a time; only proof bodies
belonging to the actual additive dependency cone are retained. Resource-bounded
microbatches reconstruct genuinely new theorem bodies.

The exact release appends **60 independently checked theorems**: 21 binary
length, 20 Euclidean gcd transport, and 19 binary modular execution. Its
complete dependency cone has **239 theorem nodes**, **17 maximal checked
endpoints**, and **one synthetic packaging root**. The actual certificate has
**240 independently kernel-checked proof nodes**, **597 dependency edges**,
**11,848 ordinary structural proof nodes**, and **1,099,541 exact bytes**.
Its SHA-256 is
`95e5f8a3baef113721d748f9d7071864b4bf9511737a27a1272d2695428fb938`.

Historical bodies are retained from exact frozen provenance: **155 Alpha-v21
advanced-layer**, **7 Alpha-v19 frontier**, **11 Alpha-v19 residual**, and
**4 Alpha-v20 next-layer** proofs. **Two genuine historical parent proofs**
are rebuilt with the unchanged kernel; the remaining **60 reconstructed
bodies** are the new candidate theorems. No unrelated proof body is counted
as a new theorem.

The separately compiled Lean verifier independently checks the entire artifact
before the additive Alpha catalog is published. A digest authenticates proof
bytes but never substitutes for an original-kernel or independent Lean check.

The terminal state of every admitted anchored Euclidean execution is proved to
equal its actual relational gcd; this closes the specific v21 state/output
identification gap. Stronger full logarithmic Euclidean and modular-execution
bounds are not asserted without an exact independently checked theorem.