Mathesis

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) t

Arguments

DOIAuthorDate
MTH.R-2026-6014Dhruv GuptaDhruv Gupta2026-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