# Independently checked complete all-natural two-square closure

Date: **2026-08-25**.

The exact previously enrolled constructive theorem

```text
two_square_iff_zero_or_even_three_mod_four_prime_valuations
```

now has complete self-contained ordinary intuitionistic proof data. Its
unchanged first-order statement includes the zero boundary and classifies all
natural numbers by the parity of every prime valuation in the class three
modulo four. No statement is weakened or made conditional, no classical rule
is added, and no theorem name or digest is accepted as proof.

The exact immutable Alpha-v17 dependency closure contains **517 theorem
nodes** and **1,599 exact direct dependencies**. Of these, **377** already have
Alpha-v17 checked-use authority, while **140** remain release-level
`body_checked`. Exactly **356** complete ordinary proof bodies are reused
from the independently checked quadratic-reciprocity artifact; the remaining
**161** bodies consist of all 140 currently body-only theorems and 21
already-checked prerequisites absent from that artifact.

Every reconstructed body is derived from its exact unchanged dependency-
curried first-order tactic script and checked by the original intuitionistic
kernel. Reconstruction uses twenty-one batches: twenty batches of eight proofs
and one final singleton. The largest observed batch contains **1,025
structural proof nodes** and **976 proof objects**, strictly below the
unchanged sixteen-body, 125,000-node, and 25,000-object ceilings.

The canonical complete proof artifact is:

```text
research/arithmetic-library/artifacts/two-square-proof-bundle-v1.json
```

Its independently checked identities and proof metrics are:

```text
parent Alpha edition:           v17
parent edition SHA-256:         db2e6e5796169600d17cc54313e9306bac46fb680f914cb2a5a91d247bb746c4
exact root statement SHA-256:   4c39da833a313bab5ae810215dae5bbc9cc78ea951fe97fb177c36a5347cecd5
canonical artifact SHA-256:     f2e77dc6e8c87c715bf2c4f3325e999e7180a2c3ab0fa93f3e9a5006d3e1684e
canonical artifact bytes:       1868714
exact theorem proof bodies:     517
exact dependency edges:         1599
total structural body nodes:    33546
original Python-kernel calls:   517
exact root local ID:            516
```

The independent separately compiled Lean proof-bundle verifier reports:

```text
ACCEPT  two-square-proof-bundle-v1.json  nodes=517  root=516
```

Additionally, the complete dependency graph was compiled into one ordinary
certificate using only the existing layered intuitionistic `Cut` rule. The
unchanged original kernel independently accepted the exact zero-inclusive
all-natural endpoint from the empty context:

```text
ordinary exact endpoint structural proof nodes: 45173
check((), ordinary_certificate, exact_original_formula): True
```

This complete independently checked proof does **not** change the immutable
Alpha-v17 evidence partition, checked-use boundary, default Stable edition,
or any frozen historical artifact. A subsequent immutable promotion requires
its own separately reviewed evidence-only release.