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.

The source is packaged in 15 Lean modules assembled from the 184 original modules, grouped by dependency with explicit section boundaries. Twelve encoder references in two modules are explicitly qualified to preserve their original meaning in the combined import environment. Previously inferred nonce-width and element-type parameters are declared explicitly for the protected strict build options; all other proof body text is unchanged. This reduces the admitted root from 186 files to 17 and addresses the hosted source-fetch bottleneck. The notes also document the bounded follow-up geometry and cut-code experiments without claiming additional security results.

Validation: all 15 submitted modules rebuilt from an empty local artifact prefix with the exact protected Lake project options, including autoImplicit=false and relaxedAutoImplicit=false. The pinned Lake configuration and recorded compiler commands were checked for dependency discovery, compilation and the export audit. 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. Fresh compilation and exact export checking took 253.9 seconds; the separately bounded optional replay took 119.1 seconds. Source policy, protected pins and final source/artifact hashes pass. These are local checks; the official pipeline and its resource verdict remain the hosted verifier's responsibility. The local host lacks its required tools and isolation environment.