Upper bound · compressions verified

This submission lowers verification from 102 to 100 compressions by tightening the security proof for the index. The index now retains 127 bits, while the nonce retains 128 bits. The smaller index universe needs half as many distinct cuts at the same signing success rate, allowing two fewer chain hashes on the existing forest.

The complete certificate passes a frozen dependency rebuild, independent kernel replay, and exact protected-interface and axiom checks. This PR requests official hosted verification of the 100-compression claim.

The construction

54 independent 128-bit seeds
        │  18 tagged hash steps per chain
54 chain tips
        │  3 tips per group
18 group digests
        │  one tagged root hash
128-bit public key

A signature discloses six group digests and 36 chain values from the other twelve groups. The remaining chain costs sum to 82. Each hash input includes its 16-bit node tag, so the chain, group and root inputs cost one, one and five compressions.

Resource	Exact accounting
Key generation	54*18 + 18 + 5 = 995
Signature	128 + 42*128 = 5504 bits
Reconstruction	82 + 12 + 5 = 99 compressions
Index	1 compression
Verification	100 compressions, on every input and answer path

The certified family contains

$$ \binom{18}{6}x^{82}^{36} =14{,}696{,}477{,}531{,}177{,}027{,}506{,}903{,}935{,}123{,}070{,}536 $$

distinct cuts, enough for M = 45·2^108. With a 127-bit index, a fresh trial succeeds with probability 45/524288. The existing availability argument therefore still bounds failure after 2^20 trials by 2^-128.

Why 127 index bits suffice

The proof uses a property of the protected whole-experiment budget: every possible signing result has a path costing the full signing budget. Force rejected answers at distinct nonces, then the desired accepted result on the final trial. The same continuation is reached after L = 2^20 calls. Failure also has an L-call path. Thus the resource bound reserves L calls even when the actual signer stops early.

This is a resource argument under CostAtMost, which covers every raw oracle-answer path. The probability proof continues to use the ordinary single memoized random oracle.

For the pre-sign index cache, let A count accepted entries, v count distinct accepted classes, and q count all entries. Repeated-class counting gives bad entries ≤ 2(A−v). Since the nonce universe has size twice the index universe, the signing-row bound is controlled by max(A, p(q+L)/2)/M, where p=M/2^127.

The new potential is

$$ \rho=\frac{A+pL/2+\exp(pq/2-A)}{M}. $$

Its exponential term has nonpositive expected drift. The accepted-entry term charges exactly 2^-127 per fresh index query. Its initial value is positive, but

$$ \rho(\varnothing)=\frac{L}{2\cdot2^{127}}+\frac1M <\frac{L}{2^{127}},\qquad pL=90. $$

The reserved signing budget pays that initial cost. Index queries and authentication queries have different input lengths, so their charges combine in the same simulation without charging either query twice. The proof retains all strong-forgery cases and canonical raw encodings, including alternative signatures on the signed message and attacks after signing failure.

Proof and provenance

RepeatedFibers, TightRow, TightDrift and TightPotential prove the new cache analysis. SigningReserve, ReservedHazard and MasterReserve connect it to the actual programs and their budgets. The graph proof and raw-signature adapter are reused with the smaller family. The obsolete equal-width index potential is removed.

All proof changes belong to formal/Submissions/UpperCompressions/; the protected contract is unchanged. NOTES.md includes the technique and scoped results from the intervening experiments. The earlier 102-compression verdict remains tied to its exact original source.

Validation

• Every submitted dependency of Solution was rebuilt from frozen sources and independently replayed with unmodified Lean 4.33.1 leanchecker: 49 modules, plus a separate admissibility audit, all passed without retries.
• Rebuild and replay took 526.41 seconds locally; the largest observed checker process used 9.31 GiB. Each module was replayed against its imported environment; external libraries were not replayed from empty.
• Exact protected export types passed for the safe scheme definition, admissibility, strong security, and literal cost 100. The only transitive axioms are propext, Quot.sound, and Classical.choice.
• All 21 protected source hashes match. Source and artifact manifests remained unchanged throughout validation. Submission policy, sibling imports, patch application and whitespace checks pass.
• A separate semantic review confirms the whole-experiment budget, strong-forgery cases, 127/128 index–nonce split, and canonical raw encoding.

Official verifier command:

python3 .contract/verifier/verify.py upper-compressions --source . --json

The local attempt stopped before proof checking because verifier tools are missing. These local checks are not a hosted verdict; official verification is pending.