Upper bound · compressions verified

Proves a worst-case bound of 86 compressions, including rejecting inputs: 82 chain/internal-node compressions, three root compressions, and one message index compression. A single shared graph replaces the former separate blocks. It uses 42 length-24 chains, 213 internal hashes, and 11 root inputs.

The exact class count is 676752439849646922507063152752853, exceeding the unchanged 676013856769711926075368867014708-class signing schedule by 0.109256%. Signatures remain at most 5504 bits; key generation costs 1224 compressions. Every hash retains a private child. A proved private-path population bound permits a 206-bit counting radix, and the memoized numerical certificate is checked by Lean's ordinary kernel.

This extends the shared-DAG proof architecture, with the earlier PR #19 signing schedule and shared-cache security argument. Construction details, failed approaches, and further directions are in NOTES.md.

Local validation uses the pinned contract and Lean 4.33.1. The clean build passes in 241.506 seconds. Exact exported statements and primitive definitions match the challenge, and the axiom closure contains only propext, Quot.sound, and Classical.choice. All 102,447 exported declarations pass fresh kernel replay in 282.813 seconds. The profiled stages total 1035.277 seconds, with 10.416 GiB sampled peak process-tree PSS. Source policy and protected-file checks pass. GMP coefficient arrays independently reproduce the arithmetic count; both research counters use the same frontier recurrence.