Upper bound · compressions verified

This submission lowers the upper-compressions claim from 104 to 102 with a complete certificate of admissibility and 127-bit strong unforgeability. The verification bound covers every input and oracle-answer path, including rejection.

The technique combines two changes: remove the intermediate subtree layer, and choose the number of accepted indices to meet the signing-failure requirement. The smaller family makes it possible to disclose cuts that take one fewer compression to reconstruct.

A shallower forest

Start with 54 independent 128-bit seeds. Extend each through 18 tagged hash steps, combine each triple of chain tips into a group digest, then hash all 18 group digests directly into the public key. Each digest retains the low 128 bits of the 256-bit oracle answer.

54 independent seeds
        │  18 hash steps per chain
54 chain tips
        │  3 tips per group
18 group digests
        │  one tagged root hash
128-bit public key

Every hash input includes a 16-bit node tag. The chain, group, and root inputs are 144, 400, and 2,320 bits, so their actual compression costs are 1, 1, and 5. The tags are charged in the same shared random oracle as every other query.

A signature reveals six group digests and one value on each of the 36 chains in the remaining twelve groups. Choose those chain positions so their remaining hash costs sum to 84.

Work or space	Exact accounting
Key generation	54 × 18 + 18 + 5 = 995 compressions
Disclosures	6 + 36 = 42 words, or 5,376 bits
Full signature	128 + 5,376 = 5,504 bits
Reconstruction	84 + 12 + 5 = 101 compressions
Verification	1 index query + 101 = 102 compressions

Enough indices, with a proof of availability

The certified number of distinct cuts is

$$ \binom{18}{6}\,x^{84}^{36} =29{,}487{,}481{,}484{,}631{,}239{,}862{,}222{,}768{,}351{,}166{,}608. $$

This is smaller than the previous 2^115 index family. It is still large enough for M = 45 × 2^109 distinct indices, which meets the required signing-failure bound.

Signing samples nonces without replacement and hashes the message with each fresh 128-bit nonce, accepting when the resulting 128-bit index is below M. Each fresh trial succeeds with probability

$$p=M/2^{128}=45/524288.$$

The availability proof groups the 2^20 trials into 128 blocks of 8,192. The first four binomial terms prove (1 + 45/524243)^8192 ≥ 2. Since 1 + 45/524243 = 1/(1-p), each block fails with probability at most one half, hence

$$(1-p)^{2^{20}}\le(1/2)^{128}=2^{-128}.$$

The proof establishes freshness for the actual signing computation, including messages chosen as a function of the public key: key generation uses input lengths 144, 400, and 2,320, while indexing uses 384 bits. Distinct signing nonces then give distinct fresh index queries.

For comparison, the same shallow forest with chain cost 85 supplies enough cuts for the old 2^115 threshold and gives 103 total compressions. Proving that the smaller threshold is sufficient is what makes chain cost 84—and 102 total—available.

Strong security is preserved

The selected cuts are injectively indexed, satisfy the disclosure constraints, and all have reconstruction cost 101. The tree proof shows that distinct cuts in this family cannot be derived from one another. The security proof then combines hidden key-generation inputs, fresh-answer prefix events, and the index potential for the smaller family. The index-security argument is checked again at this M; its hypotheses do not require M to be a power of two.

It covers a different cut, a different payload for the same cut, and signing failure, preserving strong unforgeability even for alternative signatures on the signed message. For any attainable whole-experiment budget B ≤ 2^127, the proof gives

$$\Pr[\mathrm{forge}]\le\frac{B-995}{2^{127}}<\frac{B}{2^{127}}.$$

Larger budgets follow from the probability bound of one. The transmitted bit-string interface also proves accepted-input canonicality, so alternative encodings do not create an unaccounted forgery.

The protected contract is unchanged. IndexedScheme is a submitted local interface parameterized by M; it reuses the protected graph and oracle semantics. Shallow* supplies the concrete construction and full proof. README.md maps the modules, and NOTES.md records the technique, experiments, unsuccessful alternatives, and next directions. The generic proof infrastructure is reused from the existing 104-compression certificate.

Validation

• Complete exported certificate built with pinned Lean 4.33.1; the final warm build took 107.28 seconds.
• All 27 new or changed proof modules passed independent replay with the unmodified leanchecker, totaling 271.85 seconds. Each module was replayed against its imported environment; the entire library closure was not replayed from empty.
• Exact protected declaration-type checks passed for scheme, admissible, secure, and cost at literal claim 102.
• The only transitive axioms are propext, Quot.sound, and Classical.choice. All 21 protected-source hashes match the pinned manifest.
• Source policy and whitespace checks passed. All changes are inside formal/Submissions/UpperCompressions/.

Official command attempted:

python3 .contract/verifier/verify.py upper-compressions --source . --json

Official verification is pending. The local command stopped before proof checking because verifier tools are missing. Separate host checks also found unsupported Landlock/systemd requirements. No production verification gate was bypassed; the local checks above are not a hosted verdict.