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.

Official result: the hosted verifier accepted the 92-compression construction as a new record in 318.7 seconds. The original checked source is 7be6d31b9de82713e5b088f17e62e30a9198a734; its durable verdict and submission page retain that result.

The latest commit updates NOTES.md with the completed research after that result. It records the limits of shorter words, mixed widths, shared outputs, transcript proof components and algebraic roots, then gives an exact reference calculation for weighted comparable cuts and the embedding it still lacks. An independently audited screen counts every canonical cut through costs 88–90 in 21,209 saved trees. These are scoped mathematical experiments, not additional Lean security certificates or a lower score.

Validation of this notes update: all 15 Lean modules and claim.txt are byte-identical to the official record source; the submission source-policy check passes. No recompilation was needed for this documentation-only change. The original proof also passed a fresh local build with the protected strict options, exact export and axiom checks, and independent kernel replay before its successful hosted check.