# Alpha v23 complete constructive milestone closure receipt

The immutable parent is the complete independently original-kernel-checked
**1,890-theorem Alpha v22** release. Its exactly **432 Stable theorem entries**,
historical proof certificates, source bindings, intuitionistic arithmetic
kernel, and first-order signature remain unchanged.

The exact additive inventory consists of **17 Euclidean logarithmic-bound
proofs**, **24 arbitrary-exponent binary digit and modular-execution proofs**,
and **18 constructive three-modulo-four prime proofs**: **59 new original
theorems**, **1,949 checked-use Alpha entries**, and **6,285 checked direct
dependencies**.

The actual self-contained original-proof artifact is
`research/arithmetic-library/artifacts/alpha-v23-milestone-closure-proof-bundle-v1.json`.
Its actual dependency cone contains **616 original theorem bodies**, **nine
maximal checked theorem endpoints**, and **one unenrolled synthetic packaging
root**. The complete certificate contains **617 independently checked proof
nodes**, **1,871 actual dependency edges**, **39,161 structural proof-body
nodes**, and **2,518,315 exact bytes**. Its SHA-256 is
`cc0051da2cac31e382c79223999d448a1119f62aa448f1c7f68a6b9c3edf9d11`.

Exactly **59 new theorem bodies** and **24 required historical parent bodies**
are reconstructed in bounded one-body microbatches. Exact frozen proof bodies
are retained from Alpha v19 frontier (**305**), Alpha v19 residual closure
(**10**), Alpha v20 (**2**), Alpha v21 (**161**), and Alpha v22 (**55**).
Historical artifacts are opened one at a time and unrelated proof bodies are
discarded; no historical body or synthetic root is counted as a new theorem.

The exact G101 root is `euclidean_gcd_execution_logarithmic_bound`, artifact
node **572**, with statement SHA-256
`decf1f8be3a9dcaf2e8bdf7bebd59e46d08e9f91fee375ca325c6b53847c8d6e`.
It constructs the real terminal-gcd execution and proves
`steps <= 2*BitLen(b)+1`.

The exact G102 root is `binary_modular_execution_logarithmic_bound`, artifact
node **597**, with statement SHA-256
`3ac6949afecc26acc6e5fb9d8d9041be9a9f2b8120dcbc918b8e771a7a1bd27d`.
It constructs canonical digits for every exponent, an actual complete modular
execution, its unique correct output, and the witnessed operation bound
`steps <= 3*BitLen(exponent)+2`.

The exact G025 root is `infinitely_many_primes_three_mod_four`, artifact node
**615**, with statement SHA-256
`3ddac628b2e37925ee3d7a4bd56319de5e173e9065cce6437cab775cc646620b`.
It produces an actual prime `p=4*k+3` strictly greater than every supplied
natural bound.

Every node, actual dependency, first-order target formula, and ordinary proof
body must be accepted by the unchanged original intuitionistic kernel.
Additionally, the separately compiled Lean verifier independently accepts the
entire exact artifact before additive release authority is granted. Byte
digests never substitute for either independent mathematical verification.