Upper bound · compressions verified
- Claim
- 91 compressions record
- Submitter
- saucegodbased
- Assisted by
- Codex
- Commit
c2fdd92c27inhttps://github.com/leanEthereum/ots.golf-submissions.git- Pull request
- #19
- Code
- View source on GitHub
- Queued
- 2026-09-20 23:56:58 UTC
- Finished
- 2026-09-21 00:04:11 UTC · 422 s
Description
This submits a 91-compression candidate for the generic upper-bound track.
The central idea is to create an enormous family of disclosure cuts while making every supported cut cost exactly the same. The DAG has 66 chains of length 18, followed by 18 lower ternary hashes, 10 upper ternary hashes, and a ten-word root hash. A frontier may expand up to 16 ternary nodes. Each expansion adds one fixed reconstruction compression, while the active chain positions reduce the remaining chain work by exactly the compensating amount. Every supported cut therefore reconstructs in exactly 90 compressions.
A signature contains an 86-bit nonce and at most 42 disclosed 129-bit words:
86 + 42 × 129 = 5504 bits.
The 342-bit message/nonce index query costs one further compression, giving the claimed worst-case total of 91.
The supported family contains exactly
676013856769711926075368867014708
distinct cuts. A 160-tier exact schedule assigns integer alias multiplicities across the full 256-bit oracle-output space. Signing draws 2^20 nonces with replacement and retains the earliest occurrence in the lowest accepted tier. Lean checks the literal class populations, multiplicities, and outward-rounded kernel tables.
Equal reconstruction cost makes distinct signed and forged cuts incomparable, yielding a concrete cross-cut authentication witness. The security proof works in the actual shared memoized oracle and explicitly accounts for nonce reuse, repeated decoding of one class, private nonwinning queries, and their later public exposure. Below B = 2^86 / 64, stopped first and second moments give the coefficient
6235189 / 6272000.
Above that threshold, an equality-collision martingale, Freedman bounds, a global diagonal clock, and a simultaneous occupancy cap give
2423 / 2450.
Both coefficients are strictly below one; budgets above 2^127 close by the universal probability bound.
The raw scheme has deterministic verification, rejects oversized signatures, uses 1,219 key-generation compressions, uses at most 2^20 signing compressions, and has honest signing failure at most 2^-129.
Validation
- Current-contract source policy: PASS (52 files, 1,876,830 bytes).
- A cache-cleared build of the exact submitted root completed in 9m22s at 18.1 GiB peak aggregate RSS and 213 KiB output.
- Declaration-kind, exact-type, universe, transitive-axiom, and
leancheckerreplay checks passed. The exported declarations use onlypropext,Classical.choice, andQuot.sound.
The official wrapper could not run in this container because its host infrastructure preflight stops before candidate evaluation: Landlock ABI 2 is below the required ABI 3, systemd 252 lacks PrivatePIDs, and no separate bounded work volume is available. I am therefore not claiming a local full-wrapper pass; the hosted verifier remains authoritative.