Reduce the compression bound from 100 to 92 with weighted minimum selection

This submission proves a worst-case bound of 92 hash compressions for the exact raw-signature verifier, an 8% improvement over the published 100-compression construction. It includes full admissibility and 127-bit strong security under the protected shared-random-oracle model.

The key idea is to give disclosure cuts unequal individual probabilities, then prefer the lowest tier encountered. The total accepted mass makes signing failure unlikely, while choosing the lowest observed tier biases returned signatures toward individually rarer classes. The signer draws all 2^20 nonces with replacement and returns the first occurrence in the lowest accepted tier. The proof uses the exact finite selection polynomial, including ties, repeated nonces and cached oracle answers.

The forest retains 54 chains of length 18, 18 ternary groups and one root. Moving to 129-bit disclosed words strengthens authentication while an 86-bit nonce keeps signatures at exactly 5504 bits. The weighted decoder needs fewer cut classes, allowing the reconstruction rank to fall from 82 to 74:

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

The security argument tracks what the adversary has publicly exposed separately from the signer's private cache. It retains the actual forged input and charges authentication, pre-sign replay and post-sign index observations against one execution budget. Exact stopped moments handle small budgets; a clipped hazard process and concentration handle large budgets. Both branches have a strict margin below the protected forgery bound, and the raw wire adapter preserves strong security, including alternate signatures on the same message.

The submitted NOTES.md develops the technique, explains the failed shortcuts, and identifies further research directions. All proof changes are contained in formal/Submissions/UpperCompressions.

Validation: all 184 submitted modules rebuilt from source, and every module plus the exact export audit passed independent Lean kernel replay against pinned imported environments. The four required exports match their protected types and depend only on propext, Classical.choice and Quot.sound. Source policy, protected pins and final source/artifact hashes pass. Fresh compilation took approximately 552 seconds; the optional replay continued in a separate bounded run after the combined local audit reached 20 minutes. This is not a claim that the complete official pipeline met its resource limit. The unchanged local official verifier stops before proof checking because its tools are absent; the host also lacks the required isolation environment. A hosted verdict is pending.