Upper bound · compressions rejected

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.

Verifier context for the current notes-only head. Its latest recheck ran after the contract raised keygenBudget from 1024 to 2^20. One unchanged proof line still asked Lean to change the new obligation to the literal old bound; elaboration recovery inserted sorryAx, which caused the visible rejection. The construction's actual key-generation cost is 995, so the new obligation is weaker. PR #13 applies that one-line compatibility migration and is hosted-verified at 92 under the same protected contract digest. The original accepted verdict remains the authority for this PR's record source.

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. The latest correction rejects both sub-92 response-dependent candidates, including the full-first-answer second-query variants. One bounded predecessor search at a disclosed 124-bit chain boundary creates at least 16 lower-ranked neighboring cuts for almost every tier-zero class. Exact whole-game calculations give forgery probability above 0.43569 while the protected allowance is below 0.25000001; an independent certificate proves the simpler separation above 5/12 versus below 1/3. These counterexamples do not affect the verified 92-compression construction, whose disclosed graph words are 129 bits and whose original proof remains unchanged. The notes retain the executable resource results, supporting probability lemmas and Lean components with their corrected scope, and record broad negative screens for immediate repairs. 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.