The Ambainis composition lock, at every depth: the product partition of the (d+1)-fold Ambainis iterate — the construction giving the multiplicative upper bound on the partition number — is not the leaf partition of any deterministic protocol, for every depth d. Index 0 is the base partition itself (a kernel-checked eight-rectangle monochromatic partition of the base game); index 1 is the 64-rectangle object of the depth-two frontier.
DeclKWLock.ambainis_tower_locked
∀ (d : ℕ),
¬∃ t,
KWLock.Realizes (KWLock.onesOf (KWLock.Fd 4 KWLock.fA (d + 1))) (KWLock.zerosOf (KWLock.Fd 4 KWLock.fA (d + 1)))
(KWLock.towerP 4 KWLock.fA KWLock.pA d) tArguments
| DOI | Author | Date |
|---|---|---|
| MTH.R-2026-6014 | 2026-09-24T00:00:00Z |
DOIMTH.C-2026-6014
Cite
Verification
- Library
- FLT_Proofs.Complexity.KWCompositionLock
- Statement digest
- c6782e37c692
- First verified
- 2026-09-24T00:00:00Z