Upper bound · compressions verified

Upper bound in compressions: 85 = 1 index query + 82 in-graph compressions + a 2-compression root.

This is the checked 86 construction (PR #68) on a different graph. The signing schedule, 86-bit nonce, 129-bit values, class count and security argument are unchanged.

Idea. A graph of this family is 42 long chains: a spine of ternary nodes ending in a private chain, or a plain chain. A cut is a composition of the in-graph cost over those 42 chains in which every chain with a positive entry is reachable from the tops. So the number of cuts of cost r is C(r+41, 41) times the probability that a uniform composition is reachable. The 86 graph keeps 88.60% of C(123, 41). A graph laid out top-down, where each target takes the strongest free reference slots above it and at most one per spine, keeps 92.32% with only seven tops.

Graph. 42 chains of length 24, 213 ternary nodes, seven tops. The root reads 16 + 7*129 = 919 bits, two compressions. Exact count at in-graph cost 82: 705154647346183708283501533499397, which is 4.311% above the 676013856769711926075368867014708 classes the schedule needs. Key generation costs 1223.

Proof changes. The graph tables, the generating number and the exact count in LongChain91Geometry.lean; the root arity, root cost and key-generation cost constants elsewhere; and the root case of sprRate_le_query_cost, which becomes an equality. The ProofBundle and schedule files are untouched. The counting certificate has 2260 recurrence states against 72680 for the 86 graph.

Verification. python3 .contract/verifier/verify.py upper-compressions --source . reports verified at claim 85 in 336.5 seconds with 8.2 GB peak resident size. That run was local on macOS, where the verifier is not sandboxed, so it is development evidence and not a hosted verdict.

Credits. The proof is the 86 record's, by nconsigny (PR #68), which builds on the 88 record by lucemans (PR #58) and the 91 record (PR #19). NOTES.md has the method, the exact counts for other root sizes and what is left for 84.