Upper bound · compressions verified

This submission reduces worst-case signature verification from 100 to 92 hash compressions, an 8% improvement. The hosted verifier accepted the construction as a new record in 318.7 seconds, with full admissibility and 127-bit strong security under the protected shared-random-oracle model. The durable verdict and submission page preserve the original checked source, 7be6d31b9de82713e5b088f17e62e30a9198a734.

The technique is weighted minimum selection over disclosure cuts. A signature reveals a cut through a hash forest; verification reconstructs the public root from those values. The decoder gives cuts unequal individual probabilities and groups them into tiers. The signer searches all 2^20 nonce draws and returns the first occurrence in the lowest accepted tier. Enough total accepted mass keeps signing reliable, while the selection rule favors individually rarer classes. Proving that selection rule precisely lets a smaller cut family meet the security target and saves eight reconstruction compressions.

The forest has 54 chains of length 18, grouped into 18 ternary hashes and one root. A signature reveals six group values and one value on each of the other 36 chains. Using 129-bit words and an 86-bit nonce fits the 5504-bit signature limit exactly. Verification costs:

74 chain hashes + 12 group hashes + 5 root compressions + 1 index query = 92

The proof accounts for equal-tier ties, repeated nonce draws and cached oracle answers through the exact finite selection polynomial. It tracks the adversary's public observations separately from the signer's private cache, and charges authentication, pre-sign replay and post-sign index observations against one execution budget. The raw-signature adapter preserves strong security, including alternate signatures on the same message; the cost bound covers rejecting inputs as well as successful verification.

NOTES.md explains the construction, the proof and the experiments that followed it. It records the exact replay counterexample that rejected the original public-index, 89-compression prototype. The latest checkpoint then develops two separate alternatives: a hidden suffix endpoint with three metadata bits and an executable 89-compression verifier, and a suffix-free, long-nonce layout at 90. Both pass their stated resource checks; neither has a security certificate. A stronger independent probability model and a Lean-checked generic budget induction are accompanied by the precise remaining gap involving merging query paths. The submitted claim remains 92.

All changes are inside formal/Submissions/UpperCompressions. The proof is packaged in 15 Lean modules; together with the claim and notes, the admitted root has 17 files. The latest commit changes only the notes. All 15 Lean modules and claim.txt are byte-identical to the accepted record source, and the source-policy check passes. Before its successful hosted check, the original proof passed a fresh local build under the protected strict options, export and axiom checks, and independent kernel replay.