Mathesis
Dhruv GuptaDhruv GuptaZetetic-Dhruvperson2026-09-24T00:00:00Z
ClaimMTH.C-2026-6014ArgumentMTH.R-2026-6014

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
Layout
ThesisStepDefinition
ambainis_tower_lockedtheoremtower_not_protocolizabletheoremtower_goodtheoremzerosOf_congrtheoremonesOf_congrtheoremcomp_rowConnectedtheoremcross_step_rowtheoremcluster_linked_rowtheoremcomp_rowTouch_sametheoremcomp_monoValidtheoremcomp_distincttheorempairwise_disjoint_of_netheoremcomp_isPartitiontheoremrowSideSel_valtheoremrowSideSel_nonemptytheoremcomp_pairwisetheoremmem_rows_compRecttheoremdisjointtheoremcomp_colConnectedtheoremcross_step_coltheoremexists_point₂theoremcolSideSel_nonemptytheoremcomp_Q_ne_niltheorempartition_ne_niltheoremcoverstheoremcluster_linked_coltheoremmem_compPartitiontheoremlinked_all_memtheoremcomp_colTouch_sametheoremmem_cols_compRecttheoremexists_pointtheoremcolSideSel_valtheoremmem_zerosOftheoremmem_onesOftheoremcontainedtheoremrowctheoremparttheoremontotheoremmonotheoremdisttheoremcolctheoremFd_ontotheoremcomp_ontotheoremconnected_not_protocoliza…theoremrow_side_invarianttheoremcol_side_invarianttheoremleaves_ne_niltheoremfollows_leaf_subtheoremnonemptytheoremambainis_towerHyptheorempA_rowConnectedtheoremsymmtheorempA_monotheorempA_isPartitiontheorempA_distincttheorempA_colConnectedtheoremconnectedVia_of_walktheoremlinked_of_walktheoremlinked_mem_symmtheoremsymmtheoremfA_ontotheoremColConnecteddefColTouchdefConnectedViadefFddefIsPartitionstructureIsWalkdefKRectstructureCelldefcolsdeflabeldeforientdefrowsdefLabdefMonoValiddefProtocolinductiveFollowsdefgodefleavesdefRealizesdefRowConnecteddefRowTouchdefSpdefTStepdefTowerHypstructureblockPatdefcolSideSeldefcompFundefcompPartitiondefcompRectdeffAdefinstDecidableCellOfDecida…definstDecidableColTouchOfDe…definstDecidableEqKRectdefinstDecidableEqSpdefinstDecidableIsWalkdefinstDecidableRowTouchOfDe…definstFintypeSpdefonesOfdefpAdefrA1defrA2defrA3defrA4defrA5defrA6defrA7defrA8defrowSideSeldeftowerPdefvvaldefzerosOfdef
  1. DeclKWLock.ambainis_tower_lockedDeclaration kindtheorem
    ∀ (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
    KWLock.FdKWLock.LabKWLock.ProtocolKWLock.RealizesKWLock.SpKWLock.fAKWLock.instDecidableEqSpKWLock.instFintypeSpKWLock.onesOfKWLock.pAKWLock.towerPKWLock.zerosOf
    Uses
  2. DeclKWLock.tower_not_protocolizableDeclaration kindtheorem

    The composition lock. Under the base hypotheses, the product partition of the (d+1)-fold iterate is not the leaf partition of any deterministic protocol, for every depth.

    ∀ (k : ℕ) (f : (Fin k → Bool) → Bool) (P₀ : List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k))),
  KWLock.TowerHyp k f P₀ →
    ∀ (d : ℕ),
      ¬∃ t,
          KWLock.Realizes (KWLock.onesOf (KWLock.Fd k f (d + 1))) (KWLock.zerosOf (KWLock.Fd k f (d + 1)))
            (KWLock.towerP k f P₀ d) t
    KWLock.ColConnectedKWLock.FdKWLock.IsPartitionKWLock.KRectKWLock.LabKWLock.MonoValidKWLock.ProtocolKWLock.RealizesKWLock.RowConnectedKWLock.SpKWLock.TowerHypKWLock.instDecidableEqSpKWLock.instFintypeSpKWLock.onesOfKWLock.towerPKWLock.vvalKWLock.zerosOf
    Uses
    Used by
  3. DeclKWLock.tower_goodDeclaration kindtheorem

    Everything transfers up the tower: at every depth the product partition is a valid, monochromatic partition of the iterate's game, with both overlap graphs connected and two distinct members.

    ∀ (k : ℕ) (f : (Fin k → Bool) → Bool) (P₀ : List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k))),
  KWLock.TowerHyp k f P₀ →
    ∀ (d : ℕ),
      KWLock.IsPartition (KWLock.onesOf (KWLock.Fd k f (d + 1))) (KWLock.zerosOf (KWLock.Fd k f (d + 1)))
          (KWLock.towerP k f P₀ d) ∧
        KWLock.MonoValid (KWLock.vval k d) (KWLock.vval k d) (KWLock.towerP k f P₀ d) ∧
          KWLock.RowConnected (KWLock.towerP k f P₀ d) ∧
            KWLock.ColConnected (KWLock.towerP k f P₀ d) ∧
              ∃ r ∈ KWLock.towerP k f P₀ d, ∃ s ∈ KWLock.towerP k f P₀ d, r ≠ s
    KWLock.ColConnectedKWLock.FdKWLock.IsPartitionKWLock.KRectKWLock.LabKWLock.MonoValidKWLock.RowConnectedKWLock.SpKWLock.TowerHypKWLock.compFunKWLock.compPartitionKWLock.instDecidableEqSpKWLock.instFintypeSpKWLock.onesOfKWLock.towerPKWLock.vvalKWLock.zerosOf
    Uses
    Used by
  4. DeclKWLock.zerosOf_congrDeclaration kindtheorem

    Pointwise-equal Boolean functions have equal zeros.

    ∀ {α : Type} [inst : Fintype α] {h₁ h₂ : α → Bool}, (∀ (x : α), h₁ x = h₂ x) → KWLock.zerosOf h₁ = KWLock.zerosOf h₂
    KWLock.zerosOf
    Uses
    Used by
  5. DeclKWLock.onesOf_congrDeclaration kindtheorem

    Pointwise-equal Boolean functions have equal ones.

    ∀ {α : Type} [inst : Fintype α] {h₁ h₂ : α → Bool}, (∀ (x : α), h₁ x = h₂ x) → KWLock.onesOf h₁ = KWLock.onesOf h₂
    KWLock.onesOf
    Uses
    Used by
  6. DeclKWLock.comp_rowConnectedDeclaration kindtheorem

    The connectivity transfer, rows. Outer connectivity plus block connectivity (both graphs of every block partition) yields row connectivity of the product.

    ∀ {k : ℕ} {V : Fin k → Type} [inst : (i : Fin k) → DecidableEq (V i)] [inst_1 : (i : Fin k) → Fintype (V i)]
  {κ : Fin k → Type} (g : (i : Fin k) → V i → Bool) (f : (Fin k → Bool) → Bool)
  {Po : List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k))}
  {Q : (i : Fin k) → List (KWLock.KRect (V i) (V i) (κ i))},
  (∀ (i : Fin k) (b : Bool), ∃ v, g i v = b) →
    KWLock.IsPartition (KWLock.onesOf f) (KWLock.zerosOf f) Po →
      KWLock.MonoValid (fun u i => u i) (fun u i => u i) Po →
        (∀ (i : Fin k), KWLock.IsPartition (KWLock.onesOf (g i)) (KWLock.zerosOf (g i)) (Q i)) →
          KWLock.RowConnected Po →
            (∀ (i : Fin k), KWLock.RowConnected (Q i)) →
              (∀ (i : Fin k), KWLock.ColConnected (Q i)) → KWLock.RowConnected (KWLock.compPartition g Po Q)
    KWLock.ColConnectedKWLock.IsPartitionKWLock.KRectKWLock.KRect.labelKWLock.MonoValidKWLock.RowConnectedKWLock.RowTouchKWLock.TStepKWLock.compPartitionKWLock.compRectKWLock.onesOfKWLock.zerosOf
    Uses
    Used by
  7. DeclKWLock.cross_step_rowDeclaration kindtheorem

    The hop. Outer rectangles sharing a row yield touching composed rectangles: directly across distinct blocks, and through a common block rectangle when the blocks coincide (in which case the shared pattern forces equal orientations).

    ∀ {k : ℕ} {V : Fin k → Type} [inst : (i : Fin k) → DecidableEq (V i)] [inst_1 : (i : Fin k) → Fintype (V i)]
  {κ : Fin k → Type} (g : (i : Fin k) → V i → Bool) {Po : List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k))}
  {Q : (i : Fin k) → List (KWLock.KRect (V i) (V i) (κ i))},
  (∀ (i : Fin k) (b : Bool), ∃ v, g i v = b) →
    KWLock.MonoValid (fun u i => u i) (fun u i => u i) Po →
      (∀ (i : Fin k), KWLock.IsPartition (KWLock.onesOf (g i)) (KWLock.zerosOf (g i)) (Q i)) →
        (∀ (i : Fin k) (b : Bool), ∃ v, g i v = b) →
          ∀ {Ro So : KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k)},
            Ro ∈ Po →
              So ∈ Po →
                KWLock.RowTouch Ro So →
                  ∀ {q : KWLock.KRect (V Ro.label) (V Ro.label) (κ Ro.label)},
                    q ∈ Q Ro.label → ∃ p ∈ Q So.label, KWLock.RowTouch (KWLock.compRect g Ro q) (KWLock.compRect g So p)
    KWLock.IsPartitionKWLock.KRectKWLock.KRect.colsKWLock.KRect.labelKWLock.KRect.orientKWLock.KRect.rowsKWLock.MonoValidKWLock.RowTouchKWLock.blockPatKWLock.compRectKWLock.onesOfKWLock.rowSideSelKWLock.zerosOf
    Uses
    Used by
  8. DeclKWLock.cluster_linked_rowDeclaration kindtheorem

    Within one outer rectangle, composed rectangles over linked block rectangles are linked: the cluster inherits the block partition's row graph in the standard orientation and its column graph in the reversed one.

    ∀ {k : ℕ} {V : Fin k → Type} [inst : (i : Fin k) → DecidableEq (V i)] [inst_1 : (i : Fin k) → Fintype (V i)]
  {κ : Fin k → Type} (g : (i : Fin k) → V i → Bool) (f : (Fin k → Bool) → Bool)
  {Po : List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k))}
  {Q : (i : Fin k) → List (KWLock.KRect (V i) (V i) (κ i))},
  (∀ (i : Fin k) (b : Bool), ∃ v, g i v = b) →
    KWLock.IsPartition (KWLock.onesOf f) (KWLock.zerosOf f) Po →
      KWLock.MonoValid (fun u i => u i) (fun u i => u i) Po →
        (∀ (i : Fin k), KWLock.IsPartition (KWLock.onesOf (g i)) (KWLock.zerosOf (g i)) (Q i)) →
          (∀ (i : Fin k), KWLock.RowConnected (Q i)) →
            (∀ (i : Fin k), KWLock.ColConnected (Q i)) →
              ∀ {Ro : KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k)},
                Ro ∈ Po →
                  ∀ {q q' : KWLock.KRect (V Ro.label) (V Ro.label) (κ Ro.label)},
                    q ∈ Q Ro.label →
                      q' ∈ Q Ro.label →
                        Relation.ReflTransGen (KWLock.TStep KWLock.RowTouch (KWLock.compPartition g Po Q))
                          (KWLock.compRect g Ro q) (KWLock.compRect g Ro q')
    KWLock.ColConnectedKWLock.ColTouchKWLock.IsPartitionKWLock.KRectKWLock.KRect.colsKWLock.KRect.labelKWLock.KRect.orientKWLock.KRect.rowsKWLock.MonoValidKWLock.RowConnectedKWLock.RowTouchKWLock.TStepKWLock.compPartitionKWLock.compRectKWLock.onesOfKWLock.rowSideSelKWLock.zerosOf
    Uses
    Used by
  9. DeclKWLock.comp_rowTouch_sameDeclaration kindtheorem

    Same-outer composed rectangles sharing a side value share a row.

    ∀ {k : ℕ} {V : Fin k → Type} [inst : (i : Fin k) → DecidableEq (V i)] [inst_1 : (i : Fin k) → Fintype (V i)]
  {κ : Fin k → Type} (g : (i : Fin k) → V i → Bool) {Po : List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k))}
  {Q : (i : Fin k) → List (KWLock.KRect (V i) (V i) (κ i))},
  (∀ (i : Fin k) (b : Bool), ∃ v, g i v = b) →
    KWLock.MonoValid (fun u i => u i) (fun u i => u i) Po →
      (∀ (i : Fin k), KWLock.IsPartition (KWLock.onesOf (g i)) (KWLock.zerosOf (g i)) (Q i)) →
        ∀ {Ro : KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k)},
          Ro ∈ Po →
            Ro.rows.Nonempty →
              ∀ {q q' : KWLock.KRect (V Ro.label) (V Ro.label) (κ Ro.label)},
                q ∈ Q Ro.label →
                  ∀ {v₀ : V Ro.label},
                    v₀ ∈ KWLock.rowSideSel Ro.orient q →
                      v₀ ∈ KWLock.rowSideSel Ro.orient q' →
                        KWLock.RowTouch (KWLock.compRect g Ro q) (KWLock.compRect g Ro q')
    KWLock.IsPartitionKWLock.KRectKWLock.KRect.colsKWLock.KRect.labelKWLock.KRect.orientKWLock.KRect.rowsKWLock.MonoValidKWLock.RowTouchKWLock.blockPatKWLock.compRectKWLock.onesOfKWLock.rowSideSelKWLock.zerosOf
    Uses
    Used by
  10. DeclKWLock.comp_monoValidDeclaration kindtheorem

    Labels transfer. The composed partition is monochromatic at its physical coordinates, under the composed valuation.

    ∀ {k : ℕ} {V : Fin k → Type} [inst : (i : Fin k) → DecidableEq (V i)] [inst_1 : (i : Fin k) → Fintype (V i)]
  {κ : Fin k → Type} (g : (i : Fin k) → V i → Bool) {Po : List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k))}
  {Q : (i : Fin k) → List (KWLock.KRect (V i) (V i) (κ i))} (vκ : (i : Fin k) → V i → κ i → Bool),
  (∀ (i : Fin k), KWLock.MonoValid (vκ i) (vκ i) (Q i)) →
    KWLock.MonoValid (fun w s => vκ s.fst (w s.fst) s.snd) (fun w s => vκ s.fst (w s.fst) s.snd)
      (KWLock.compPartition g Po Q)
    KWLock.KRectKWLock.KRect.colsKWLock.KRect.labelKWLock.KRect.orientKWLock.KRect.rowsKWLock.MonoValidKWLock.blockPatKWLock.colSideSelKWLock.compPartitionKWLock.compRectKWLock.rowSideSel
    Uses
    Used by
  11. DeclKWLock.comp_distinctDeclaration kindtheorem

    Distinctness transfers: children of two distinct outer rectangles are distinct, because their cells are nonempty and outer-disjoint.

    ∀ {k : ℕ} {V : Fin k → Type} [inst : (i : Fin k) → DecidableEq (V i)] [inst_1 : (i : Fin k) → Fintype (V i)]
  {κ : Fin k → Type} (g : (i : Fin k) → V i → Bool) (f : (Fin k → Bool) → Bool)
  {Po : List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k))}
  {Q : (i : Fin k) → List (KWLock.KRect (V i) (V i) (κ i))},
  (∀ (i : Fin k) (b : Bool), ∃ v, g i v = b) →
    KWLock.IsPartition (KWLock.onesOf f) (KWLock.zerosOf f) Po →
      KWLock.MonoValid (fun u i => u i) (fun u i => u i) Po →
        (∀ (i : Fin k), KWLock.IsPartition (KWLock.onesOf (g i)) (KWLock.zerosOf (g i)) (Q i)) →
          (∃ r ∈ Po, ∃ s ∈ Po, r ≠ s) → ∃ r ∈ KWLock.compPartition g Po Q, ∃ s ∈ KWLock.compPartition g Po Q, r ≠ s
    KWLock.IsPartitionKWLock.KRectKWLock.KRect.CellKWLock.KRect.colsKWLock.KRect.labelKWLock.KRect.orientKWLock.KRect.rowsKWLock.MonoValidKWLock.blockPatKWLock.colSideSelKWLock.compFunKWLock.compPartitionKWLock.compRectKWLock.onesOfKWLock.rowSideSelKWLock.zerosOf
    Uses
    Used by
  12. DeclKWLock.pairwise_disjoint_of_neDeclaration kindtheorem

    Extract pairwise cell-disjointness for two distinct members.

    ∀ {X Y ι : Type} {P : List (KWLock.KRect X Y ι)},
  List.Pairwise (fun r s => ∀ (x : X) (y : Y), ¬(r.Cell x y ∧ s.Cell x y)) P →
    ∀ {r s : KWLock.KRect X Y ι}, r ∈ P → s ∈ P → r ≠ s → ∀ (x : X) (y : Y), ¬(r.Cell x y ∧ s.Cell x y)
    KWLock.KRectKWLock.KRect.Cell
    Used by
  13. DeclKWLock.comp_isPartitionDeclaration kindtheorem

    Validity transfers. The product of a valid labeled outer partition with valid block partitions is a valid partition of the composed game.

    ∀ {k : ℕ} {V : Fin k → Type} [inst : (i : Fin k) → DecidableEq (V i)] [inst_1 : (i : Fin k) → Fintype (V i)]
  {κ : Fin k → Type} (g : (i : Fin k) → V i → Bool) (f : (Fin k → Bool) → Bool)
  {Po : List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k))}
  {Q : (i : Fin k) → List (KWLock.KRect (V i) (V i) (κ i))},
  KWLock.IsPartition (KWLock.onesOf f) (KWLock.zerosOf f) Po →
    KWLock.MonoValid (fun u i => u i) (fun u i => u i) Po →
      (∀ (i : Fin k), KWLock.IsPartition (KWLock.onesOf (g i)) (KWLock.zerosOf (g i)) (Q i)) →
        (∀ (i : Fin k) (b : Bool), ∃ v, g i v = b) →
          KWLock.IsPartition (KWLock.onesOf (KWLock.compFun g f)) (KWLock.zerosOf (KWLock.compFun g f))
            (KWLock.compPartition g Po Q)
    KWLock.IsPartitionKWLock.KRectKWLock.KRect.CellKWLock.KRect.colsKWLock.KRect.labelKWLock.KRect.orientKWLock.KRect.rowsKWLock.MonoValidKWLock.blockPatKWLock.colSideSelKWLock.compFunKWLock.compPartitionKWLock.compRectKWLock.onesOfKWLock.rowSideSelKWLock.zerosOf
    Uses
    Used by
  14. DeclKWLock.rowSideSel_valDeclaration kindtheorem

    A value on the row side of a block rectangle evaluates, under the block function, to the orientation — provided the block partition is contained in its game.

    ∀ {k : ℕ} {V : Fin k → Type} [inst : (i : Fin k) → Fintype (V i)] {κ : Fin k → Type} (g : (i : Fin k) → V i → Bool)
  {a : Fin k} {q : KWLock.KRect (V a) (V a) (κ a)},
  q.rows ⊆ KWLock.onesOf (g a) →
    q.cols ⊆ KWLock.zerosOf (g a) → ∀ (o : Bool) {v : V a}, v ∈ KWLock.rowSideSel o q → g a v = o
    KWLock.KRectKWLock.KRect.colsKWLock.KRect.rowsKWLock.onesOfKWLock.rowSideSelKWLock.zerosOf
    Uses
    Used by
  15. DeclKWLock.rowSideSel_nonemptyDeclaration kindtheorem

    Row sides of members of a valid block partition are nonempty.

    ∀ {k : ℕ} {V κ : Fin k → Type} {a : Fin k} {q : KWLock.KRect (V a) (V a) (κ a)},
  q.rows.Nonempty ∧ q.cols.Nonempty → ∀ (o : Bool), (KWLock.rowSideSel o q).Nonempty
    KWLock.KRectKWLock.KRect.colsKWLock.KRect.rowsKWLock.rowSideSel
    Used by
  16. DeclKWLock.comp_pairwiseDeclaration kindtheorem

    Pairwise cell-disjointness transfers to the product: a shared composed cell projects to a shared outer cell (across outer rectangles) or a shared block cell in the orientation's order (within one outer rectangle).

    ∀ {k : ℕ} {V : Fin k → Type} [inst : (i : Fin k) → DecidableEq (V i)] [inst_1 : (i : Fin k) → Fintype (V i)]
  {κ : Fin k → Type} (g : (i : Fin k) → V i → Bool) {Po : List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k))}
  {Q : (i : Fin k) → List (KWLock.KRect (V i) (V i) (κ i))},
  List.Pairwise (fun r s => ∀ (x y : Fin k → Bool), ¬(r.Cell x y ∧ s.Cell x y)) Po →
    (∀ (i : Fin k), List.Pairwise (fun r s => ∀ (x y : V i), ¬(r.Cell x y ∧ s.Cell x y)) (Q i)) →
      List.Pairwise (fun r s => ∀ (x y : (i : Fin k) → V i), ¬(r.Cell x y ∧ s.Cell x y)) (KWLock.compPartition g Po Q)
    KWLock.KRectKWLock.KRect.CellKWLock.KRect.colsKWLock.KRect.labelKWLock.KRect.orientKWLock.KRect.rowsKWLock.blockPatKWLock.colSideSelKWLock.compPartitionKWLock.compRectKWLock.rowSideSel
    Uses
    Used by
  17. DeclKWLock.mem_rows_compRectDeclaration kindtheorem
    ∀ {k : ℕ} {V : Fin k → Type} [inst : (i : Fin k) → DecidableEq (V i)] [inst_1 : (i : Fin k) → Fintype (V i)]
  {κ : Fin k → Type} (g : (i : Fin k) → V i → Bool) {Ro : KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k)}
  {q : KWLock.KRect (V Ro.label) (V Ro.label) (κ Ro.label)} {w : (i : Fin k) → V i},
  w ∈ (KWLock.compRect g Ro q).rows ↔ KWLock.blockPat g w ∈ Ro.rows ∧ w Ro.label ∈ KWLock.rowSideSel Ro.orient q
    KWLock.KRectKWLock.KRect.labelKWLock.KRect.orientKWLock.KRect.rowsKWLock.blockPatKWLock.compRectKWLock.rowSideSel
    Used by
  18. DeclKWLock.IsPartition.disjointDeclaration kindtheorem
    ∀ {X Y ι : Type} {RX : Finset X} {CY : Finset Y} {P : List (KWLock.KRect X Y ι)},
  KWLock.IsPartition RX CY P → List.Pairwise (fun r s => ∀ (x : X) (y : Y), ¬(r.Cell x y ∧ s.Cell x y)) P
    KWLock.IsPartitionKWLock.KRectKWLock.KRect.Cell
    Used by
  19. DeclKWLock.comp_colConnectedDeclaration kindtheorem

    The connectivity transfer, columns.

    ∀ {k : ℕ} {V : Fin k → Type} [inst : (i : Fin k) → DecidableEq (V i)] [inst_1 : (i : Fin k) → Fintype (V i)]
  {κ : Fin k → Type} (g : (i : Fin k) → V i → Bool) (f : (Fin k → Bool) → Bool)
  {Po : List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k))}
  {Q : (i : Fin k) → List (KWLock.KRect (V i) (V i) (κ i))},
  (∀ (i : Fin k) (b : Bool), ∃ v, g i v = b) →
    KWLock.IsPartition (KWLock.onesOf f) (KWLock.zerosOf f) Po →
      KWLock.MonoValid (fun u i => u i) (fun u i => u i) Po →
        (∀ (i : Fin k), KWLock.IsPartition (KWLock.onesOf (g i)) (KWLock.zerosOf (g i)) (Q i)) →
          KWLock.ColConnected Po →
            (∀ (i : Fin k), KWLock.RowConnected (Q i)) →
              (∀ (i : Fin k), KWLock.ColConnected (Q i)) → KWLock.ColConnected (KWLock.compPartition g Po Q)
    KWLock.ColConnectedKWLock.ColTouchKWLock.IsPartitionKWLock.KRectKWLock.KRect.labelKWLock.MonoValidKWLock.RowConnectedKWLock.TStepKWLock.compPartitionKWLock.compRectKWLock.onesOfKWLock.zerosOf
    Uses
    Used by
  20. DeclKWLock.cross_step_colDeclaration kindtheorem

    The column mirror of cross_step_row.

    ∀ {k : ℕ} {V : Fin k → Type} [inst : (i : Fin k) → DecidableEq (V i)] [inst_1 : (i : Fin k) → Fintype (V i)]
  {κ : Fin k → Type} (g : (i : Fin k) → V i → Bool) {Po : List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k))}
  {Q : (i : Fin k) → List (KWLock.KRect (V i) (V i) (κ i))},
  (∀ (i : Fin k) (b : Bool), ∃ v, g i v = b) →
    KWLock.MonoValid (fun u i => u i) (fun u i => u i) Po →
      (∀ (i : Fin k), KWLock.IsPartition (KWLock.onesOf (g i)) (KWLock.zerosOf (g i)) (Q i)) →
        (∀ (i : Fin k) (b : Bool), ∃ v, g i v = b) →
          ∀ {Ro So : KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k)},
            Ro ∈ Po →
              So ∈ Po →
                KWLock.ColTouch Ro So →
                  ∀ {q : KWLock.KRect (V Ro.label) (V Ro.label) (κ Ro.label)},
                    q ∈ Q Ro.label → ∃ p ∈ Q So.label, KWLock.ColTouch (KWLock.compRect g Ro q) (KWLock.compRect g So p)
    KWLock.ColTouchKWLock.IsPartitionKWLock.KRectKWLock.KRect.colsKWLock.KRect.labelKWLock.KRect.orientKWLock.KRect.rowsKWLock.MonoValidKWLock.blockPatKWLock.colSideSelKWLock.compRectKWLock.onesOfKWLock.zerosOf
    Uses
    Used by
  21. DeclKWLock.exists_point₂Declaration kindtheorem

    Build a composed point with a prescribed block pattern and prescribed values at two distinct blocks.

    ∀ {k : ℕ} {V : Fin k → Type} (g : (i : Fin k) → V i → Bool),
  (∀ (i : Fin k) (b : Bool), ∃ v, g i v = b) →
    ∀ (u : Fin k → Bool) {a₁ a₂ : Fin k},
      a₁ ≠ a₂ →
        ∀ (v₁ : V a₁) (v₂ : V a₂),
          g a₁ v₁ = u a₁ → g a₂ v₂ = u a₂ → ∃ w, KWLock.blockPat g w = u ∧ w a₁ = v₁ ∧ w a₂ = v₂
    KWLock.blockPat
    Used by
  22. DeclKWLock.colSideSel_nonemptyDeclaration kindtheorem

    Column sides of members of a valid block partition are nonempty.

    ∀ {k : ℕ} {V κ : Fin k → Type} {a : Fin k} {q : KWLock.KRect (V a) (V a) (κ a)},
  q.rows.Nonempty ∧ q.cols.Nonempty → ∀ (o : Bool), (KWLock.colSideSel o q).Nonempty
    KWLock.KRectKWLock.KRect.colsKWLock.KRect.rowsKWLock.colSideSel
    Used by
  23. DeclKWLock.comp_Q_ne_nilDeclaration kindtheorem

    Block partitions of a game with a surjective block function are nonempty lists.

    ∀ {k : ℕ} {V : Fin k → Type} [inst : (i : Fin k) → Fintype (V i)] {κ : Fin k → Type} (g : (i : Fin k) → V i → Bool)
  {Q : (i : Fin k) → List (KWLock.KRect (V i) (V i) (κ i))},
  (∀ (i : Fin k) (b : Bool), ∃ v, g i v = b) →
    (∀ (i : Fin k), KWLock.IsPartition (KWLock.onesOf (g i)) (KWLock.zerosOf (g i)) (Q i)) → ∀ (i : Fin k), Q i ≠ []
    KWLock.IsPartitionKWLock.KRectKWLock.onesOfKWLock.zerosOf
    Uses
    Used by
  24. DeclKWLock.partition_ne_nilDeclaration kindtheorem

    A valid nonempty-sided partition of a nonempty product is a nonempty list.

    ∀ {X Y ι : Type} {RX : Finset X} {CY : Finset Y} {P : List (KWLock.KRect X Y ι)},
  KWLock.IsPartition RX CY P → RX.Nonempty → CY.Nonempty → P ≠ []
    KWLock.IsPartitionKWLock.KRectKWLock.KRect.Cell
    Uses
    Used by
  25. DeclKWLock.IsPartition.coversDeclaration kindtheorem
    ∀ {X Y ι : Type} {RX : Finset X} {CY : Finset Y} {P : List (KWLock.KRect X Y ι)},
  KWLock.IsPartition RX CY P → ∀ x ∈ RX, ∀ y ∈ CY, ∃ r ∈ P, r.Cell x y
    KWLock.IsPartitionKWLock.KRectKWLock.KRect.Cell
    Used by
  26. DeclKWLock.cluster_linked_colDeclaration kindtheorem

    The column mirror of cluster_linked_row.

    ∀ {k : ℕ} {V : Fin k → Type} [inst : (i : Fin k) → DecidableEq (V i)] [inst_1 : (i : Fin k) → Fintype (V i)]
  {κ : Fin k → Type} (g : (i : Fin k) → V i → Bool) (f : (Fin k → Bool) → Bool)
  {Po : List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k))}
  {Q : (i : Fin k) → List (KWLock.KRect (V i) (V i) (κ i))},
  (∀ (i : Fin k) (b : Bool), ∃ v, g i v = b) →
    KWLock.IsPartition (KWLock.onesOf f) (KWLock.zerosOf f) Po →
      KWLock.MonoValid (fun u i => u i) (fun u i => u i) Po →
        (∀ (i : Fin k), KWLock.IsPartition (KWLock.onesOf (g i)) (KWLock.zerosOf (g i)) (Q i)) →
          (∀ (i : Fin k), KWLock.RowConnected (Q i)) →
            (∀ (i : Fin k), KWLock.ColConnected (Q i)) →
              ∀ {Ro : KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k)},
                Ro ∈ Po →
                  ∀ {q q' : KWLock.KRect (V Ro.label) (V Ro.label) (κ Ro.label)},
                    q ∈ Q Ro.label →
                      q' ∈ Q Ro.label →
                        Relation.ReflTransGen (KWLock.TStep KWLock.ColTouch (KWLock.compPartition g Po Q))
                          (KWLock.compRect g Ro q) (KWLock.compRect g Ro q')
    KWLock.ColConnectedKWLock.ColTouchKWLock.IsPartitionKWLock.KRectKWLock.KRect.colsKWLock.KRect.labelKWLock.KRect.orientKWLock.KRect.rowsKWLock.MonoValidKWLock.RowConnectedKWLock.RowTouchKWLock.TStepKWLock.colSideSelKWLock.compPartitionKWLock.compRectKWLock.onesOfKWLock.zerosOf
    Uses
    Used by
  27. DeclKWLock.mem_compPartitionDeclaration kindtheorem
    ∀ {k : ℕ} {V : Fin k → Type} [inst : (i : Fin k) → DecidableEq (V i)] [inst_1 : (i : Fin k) → Fintype (V i)]
  {κ : Fin k → Type} (g : (i : Fin k) → V i → Bool) {Po : List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k))}
  {Q : (i : Fin k) → List (KWLock.KRect (V i) (V i) (κ i))}
  {r : KWLock.KRect ((i : Fin k) → V i) ((i : Fin k) → V i) ((i : Fin k) × κ i)},
  r ∈ KWLock.compPartition g Po Q ↔ ∃ Ro ∈ Po, ∃ q ∈ Q Ro.label, r = KWLock.compRect g Ro q
    KWLock.KRectKWLock.KRect.labelKWLock.compPartitionKWLock.compRect
    Used by
  28. DeclKWLock.linked_all_memDeclaration kindtheorem

    Along linkage from a member, every node is a member.

    ∀ {X Y ι : Type} (T : KWLock.KRect X Y ι → KWLock.KRect X Y ι → Prop) {P : List (KWLock.KRect X Y ι)}
  {r s : KWLock.KRect X Y ι}, r ∈ P → Relation.ReflTransGen (KWLock.TStep T P) r s → s ∈ P
    KWLock.KRectKWLock.TStep
    Used by
  29. DeclKWLock.comp_colTouch_sameDeclaration kindtheorem

    Same-outer composed rectangles sharing a side value share a column.

    ∀ {k : ℕ} {V : Fin k → Type} [inst : (i : Fin k) → DecidableEq (V i)] [inst_1 : (i : Fin k) → Fintype (V i)]
  {κ : Fin k → Type} (g : (i : Fin k) → V i → Bool) {Po : List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k))}
  {Q : (i : Fin k) → List (KWLock.KRect (V i) (V i) (κ i))},
  (∀ (i : Fin k) (b : Bool), ∃ v, g i v = b) →
    KWLock.MonoValid (fun u i => u i) (fun u i => u i) Po →
      (∀ (i : Fin k), KWLock.IsPartition (KWLock.onesOf (g i)) (KWLock.zerosOf (g i)) (Q i)) →
        ∀ {Ro : KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k)},
          Ro ∈ Po →
            Ro.cols.Nonempty →
              ∀ {q q' : KWLock.KRect (V Ro.label) (V Ro.label) (κ Ro.label)},
                q ∈ Q Ro.label →
                  ∀ {v₀ : V Ro.label},
                    v₀ ∈ KWLock.colSideSel Ro.orient q →
                      v₀ ∈ KWLock.colSideSel Ro.orient q' →
                        KWLock.ColTouch (KWLock.compRect g Ro q) (KWLock.compRect g Ro q')
    KWLock.ColTouchKWLock.IsPartitionKWLock.KRectKWLock.KRect.colsKWLock.KRect.labelKWLock.KRect.orientKWLock.KRect.rowsKWLock.MonoValidKWLock.blockPatKWLock.colSideSelKWLock.compRectKWLock.onesOfKWLock.zerosOf
    Uses
    Used by
  30. DeclKWLock.mem_cols_compRectDeclaration kindtheorem
    ∀ {k : ℕ} {V : Fin k → Type} [inst : (i : Fin k) → DecidableEq (V i)] [inst_1 : (i : Fin k) → Fintype (V i)]
  {κ : Fin k → Type} (g : (i : Fin k) → V i → Bool) {Ro : KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k)}
  {q : KWLock.KRect (V Ro.label) (V Ro.label) (κ Ro.label)} {w : (i : Fin k) → V i},
  w ∈ (KWLock.compRect g Ro q).cols ↔ KWLock.blockPat g w ∈ Ro.cols ∧ w Ro.label ∈ KWLock.colSideSel Ro.orient q
    KWLock.KRectKWLock.KRect.colsKWLock.KRect.labelKWLock.KRect.orientKWLock.blockPatKWLock.colSideSelKWLock.compRect
    Used by
  31. DeclKWLock.exists_pointDeclaration kindtheorem

    Build a composed point with a prescribed block pattern and a prescribed value at one block, from surjectivity of the block functions.

    ∀ {k : ℕ} {V : Fin k → Type} (g : (i : Fin k) → V i → Bool),
  (∀ (i : Fin k) (b : Bool), ∃ v, g i v = b) →
    ∀ (u : Fin k → Bool) (a : Fin k) (v : V a), g a v = u a → ∃ w, KWLock.blockPat g w = u ∧ w a = v
    KWLock.blockPat
    Used by
  32. DeclKWLock.colSideSel_valDeclaration kindtheorem

    A value on the column side of a block rectangle evaluates to the negated orientation.

    ∀ {k : ℕ} {V : Fin k → Type} [inst : (i : Fin k) → Fintype (V i)] {κ : Fin k → Type} (g : (i : Fin k) → V i → Bool)
  {a : Fin k} {q : KWLock.KRect (V a) (V a) (κ a)},
  q.rows ⊆ KWLock.onesOf (g a) →
    q.cols ⊆ KWLock.zerosOf (g a) → ∀ (o : Bool) {v : V a}, v ∈ KWLock.colSideSel o q → g a v = !o
    KWLock.KRectKWLock.KRect.colsKWLock.KRect.rowsKWLock.colSideSelKWLock.onesOfKWLock.zerosOf
    Uses
    Used by
  33. DeclKWLock.mem_zerosOfDeclaration kindtheorem
    ∀ {α : Type} [inst : Fintype α] {h : α → Bool} {x : α}, x ∈ KWLock.zerosOf h ↔ h x = false
    KWLock.zerosOf
    Used by
  34. DeclKWLock.mem_onesOfDeclaration kindtheorem
    ∀ {α : Type} [inst : Fintype α] {h : α → Bool} {x : α}, x ∈ KWLock.onesOf h ↔ h x = true
    KWLock.onesOf
    Used by
  35. DeclKWLock.IsPartition.containedDeclaration kindtheorem
    ∀ {X Y ι : Type} {RX : Finset X} {CY : Finset Y} {P : List (KWLock.KRect X Y ι)},
  KWLock.IsPartition RX CY P → ∀ r ∈ P, r.rows ⊆ RX ∧ r.cols ⊆ CY
    KWLock.IsPartitionKWLock.KRectKWLock.KRect.colsKWLock.KRect.rows
    Used by
  36. DeclKWLock.TowerHyp.rowcDeclaration kindtheorem
    ∀ {k : ℕ} {f : (Fin k → Bool) → Bool} {P₀ : List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k))},
  KWLock.TowerHyp k f P₀ → KWLock.RowConnected P₀
    KWLock.KRectKWLock.RowConnectedKWLock.TowerHyp
    Used by
  37. DeclKWLock.TowerHyp.partDeclaration kindtheorem
    ∀ {k : ℕ} {f : (Fin k → Bool) → Bool} {P₀ : List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k))},
  KWLock.TowerHyp k f P₀ → KWLock.IsPartition (KWLock.onesOf f) (KWLock.zerosOf f) P₀
    KWLock.IsPartitionKWLock.KRectKWLock.TowerHypKWLock.onesOfKWLock.zerosOf
    Used by
  38. DeclKWLock.TowerHyp.ontoDeclaration kindtheorem
    ∀ {k : ℕ} {f : (Fin k → Bool) → Bool} {P₀ : List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k))},
  KWLock.TowerHyp k f P₀ → ∀ (b : Bool), ∃ u, f u = b
    KWLock.KRectKWLock.TowerHyp
    Used by
  39. DeclKWLock.TowerHyp.monoDeclaration kindtheorem
    ∀ {k : ℕ} {f : (Fin k → Bool) → Bool} {P₀ : List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k))},
  KWLock.TowerHyp k f P₀ → KWLock.MonoValid (fun u i => u i) (fun u i => u i) P₀
    KWLock.KRectKWLock.MonoValidKWLock.TowerHyp
    Used by
  40. DeclKWLock.TowerHyp.distDeclaration kindtheorem
    ∀ {k : ℕ} {f : (Fin k → Bool) → Bool} {P₀ : List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k))},
  KWLock.TowerHyp k f P₀ → ∃ r ∈ P₀, ∃ s ∈ P₀, r ≠ s
    KWLock.KRectKWLock.TowerHyp
    Used by
  41. DeclKWLock.TowerHyp.colcDeclaration kindtheorem
    ∀ {k : ℕ} {f : (Fin k → Bool) → Bool} {P₀ : List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k))},
  KWLock.TowerHyp k f P₀ → KWLock.ColConnected P₀
    KWLock.ColConnectedKWLock.KRectKWLock.TowerHyp
    Used by
  42. DeclKWLock.Fd_ontoDeclaration kindtheorem

    The iterate is surjective at every level.

    ∀ (k : ℕ) (f : (Fin k → Bool) → Bool),
  (∀ (b : Bool), ∃ u, f u = b) → ∀ (d : ℕ) (b : Bool), ∃ w, KWLock.Fd k f (d + 1) w = b
    KWLock.FdKWLock.Sp
    Uses
    Used by
  43. DeclKWLock.comp_ontoDeclaration kindtheorem

    Surjectivity composes.

    ∀ {k : ℕ} {V : Fin k → Type} (g : (i : Fin k) → V i → Bool) (f : (Fin k → Bool) → Bool),
  (∀ (b : Bool), ∃ u, f u = b) →
    (∀ (i : Fin k) (b : Bool), ∃ v, g i v = b) → ∀ (b : Bool), ∃ w, KWLock.compFun g f w = b
    KWLock.blockPatKWLock.compFun
    Used by
  44. DeclKWLock.connected_not_protocolizableDeclaration kindtheorem

    The atomicity obstruction. Any list of nonempty-sided rectangles with two distinct members whose row-overlap graph and column-overlap graph are both connected is not the leaf list of any deterministic protocol — full partition validity is not needed. At the root split, every leaf's live side lies within one half; sharing a row (column) forces the same half; connectivity drags every rectangle to one half; yet both subtrees own a leaf.

    ∀ {X Y ι : Type} [inst : DecidableEq X] [inst_1 : DecidableEq Y] {RX : Finset X} {CY : Finset Y}
  {P : List (KWLock.KRect X Y ι)},
  (∀ r ∈ P, r.rows.Nonempty ∧ r.cols.Nonempty) →
    KWLock.RowConnected P → KWLock.ColConnected P → (∃ r ∈ P, ∃ s ∈ P, r ≠ s) → ¬∃ t, KWLock.Realizes RX CY P t
    KWLock.ColConnectedKWLock.KRectKWLock.KRect.colsKWLock.KRect.rowsKWLock.ProtocolKWLock.Protocol.FollowsKWLock.Protocol.leavesKWLock.RealizesKWLock.RowConnected
    Uses
    Used by
  45. DeclKWLock.row_side_invariantDeclaration kindtheorem

    Lying inside a fixed half of a row split is invariant along the row-overlap graph, provided every member of P lies inside one half or the other: a shared row cannot be on both sides.

    ∀ {X Y ι : Type} [inst : DecidableEq X] {P : List (KWLock.KRect X Y ι)} {RX A : Finset X},
  (∀ p ∈ P, p.rows ⊆ RX ∩ A ∨ p.rows ⊆ RX \ A) →
    ∀ {p q : KWLock.KRect X Y ι},
      Relation.ReflTransGen (KWLock.TStep KWLock.RowTouch P) p q → p.rows ⊆ RX ∩ A → q.rows ⊆ RX ∩ A
    KWLock.KRectKWLock.KRect.rowsKWLock.RowTouchKWLock.TStep
    Used by
  46. DeclKWLock.col_side_invariantDeclaration kindtheorem

    The column mirror of row_side_invariant.

    ∀ {X Y ι : Type} [inst : DecidableEq Y] {P : List (KWLock.KRect X Y ι)} {CY B : Finset Y},
  (∀ p ∈ P, p.cols ⊆ CY ∩ B ∨ p.cols ⊆ CY \ B) →
    ∀ {p q : KWLock.KRect X Y ι},
      Relation.ReflTransGen (KWLock.TStep KWLock.ColTouch P) p q → p.cols ⊆ CY ∩ B → q.cols ⊆ CY ∩ B
    KWLock.ColTouchKWLock.KRectKWLock.KRect.colsKWLock.TStep
    Used by
  47. DeclKWLock.Protocol.leaves_ne_nilDeclaration kindtheorem
    ∀ {X Y ι : Type} (t : KWLock.Protocol X Y ι), t.leaves ≠ []
    KWLock.KRectKWLock.ProtocolKWLock.Protocol.brecOn.goKWLock.Protocol.leaves
    Used by
  48. DeclKWLock.Protocol.follows_leaf_subDeclaration kindtheorem

    Every leaf of a following protocol sits inside the current rectangle.

    ∀ {X Y ι : Type} [inst : DecidableEq X] [inst_1 : DecidableEq Y] {RX : Finset X} {CY : Finset Y}
  (t : KWLock.Protocol X Y ι), KWLock.Protocol.Follows RX CY t → ∀ r ∈ t.leaves, r.rows ⊆ RX ∧ r.cols ⊆ CY
    KWLock.KRectKWLock.KRect.colsKWLock.KRect.rowsKWLock.ProtocolKWLock.Protocol.FollowsKWLock.Protocol.brecOn.goKWLock.Protocol.leaves
    Used by
  49. DeclKWLock.IsPartition.nonemptyDeclaration kindtheorem
    ∀ {X Y ι : Type} {RX : Finset X} {CY : Finset Y} {P : List (KWLock.KRect X Y ι)},
  KWLock.IsPartition RX CY P → ∀ r ∈ P, r.rows.Nonempty ∧ r.cols.Nonempty
    KWLock.IsPartitionKWLock.KRectKWLock.KRect.colsKWLock.KRect.rows
    Used by
  50. DeclKWLock.ambainis_towerHypDeclaration kindtheorem

    The Ambainis base satisfies every tower hypothesis.

    KWLock.TowerHyp 4 KWLock.fA KWLock.pA
    KWLock.TowerHypKWLock.fAKWLock.pA
    Uses
    Used by
  51. DeclKWLock.pA_rowConnectedDeclaration kindtheorem

    The row-overlap graph is connected: an explicit spanning walk.

    KWLock.RowConnected KWLock.pA
    KWLock.IsWalkKWLock.KRectKWLock.RowConnectedKWLock.RowTouchKWLock.instDecidableEqKRectKWLock.instDecidableIsWalkKWLock.instDecidableRowTouchOfDecidableEqKWLock.pAKWLock.rA1KWLock.rA2KWLock.rA3KWLock.rA4KWLock.rA5KWLock.rA6KWLock.rA7KWLock.rA8
    Uses
    Used by
  52. DeclKWLock.RowTouch.symmDeclaration kindtheorem
    ∀ {X Y ι : Type} {r s : KWLock.KRect X Y ι}, KWLock.RowTouch r s → KWLock.RowTouch s r
    KWLock.KRectKWLock.KRect.rowsKWLock.RowTouch
    Used by
  53. DeclKWLock.pA_monoDeclaration kindtheorem

    Kernel re-check: every rectangle is monochromatic at its label, in its orientation.

    KWLock.MonoValid (fun u i => u i) (fun u i => u i) KWLock.pA
    KWLock.KRectKWLock.KRect.colsKWLock.KRect.labelKWLock.KRect.orientKWLock.KRect.rowsKWLock.MonoValidKWLock.pA
    Used by
  54. DeclKWLock.pA_isPartitionDeclaration kindtheorem

    Kernel re-check: the eight rectangles form a valid partition of the Ambainis game.

    KWLock.IsPartition (KWLock.onesOf KWLock.fA) (KWLock.zerosOf KWLock.fA) KWLock.pA
    KWLock.IsPartitionKWLock.KRectKWLock.KRect.CellKWLock.KRect.colsKWLock.KRect.rowsKWLock.fAKWLock.instDecidableCellOfDecidableEqKWLock.onesOfKWLock.pAKWLock.zerosOf
    Used by
  55. DeclKWLock.pA_distinctDeclaration kindtheorem

    Two distinct members.

    ∃ r ∈ KWLock.pA, ∃ s ∈ KWLock.pA, r ≠ s
    KWLock.KRectKWLock.instDecidableEqKRectKWLock.pA
    Used by
  56. DeclKWLock.pA_colConnectedDeclaration kindtheorem

    The column-overlap graph is connected: an explicit spanning walk.

    KWLock.ColConnected KWLock.pA
    KWLock.ColConnectedKWLock.ColTouchKWLock.IsWalkKWLock.KRectKWLock.instDecidableColTouchOfDecidableEqKWLock.instDecidableEqKRectKWLock.instDecidableIsWalkKWLock.pAKWLock.rA1KWLock.rA2KWLock.rA3KWLock.rA4KWLock.rA5KWLock.rA6KWLock.rA7KWLock.rA8
    Uses
    Used by
  57. DeclKWLock.connectedVia_of_walkDeclaration kindtheorem

    A spanning walk — inside P, visiting every member — yields connectivity.

    ∀ {X Y ι : Type} (T : KWLock.KRect X Y ι → KWLock.KRect X Y ι → Prop),
  (∀ {r s : KWLock.KRect X Y ι}, T r s → T s r) →
    ∀ {P w : List (KWLock.KRect X Y ι)},
      w ≠ [] → KWLock.IsWalk T w → (∀ r ∈ w, r ∈ P) → (∀ r ∈ P, r ∈ w) → KWLock.ConnectedVia T P
    KWLock.ConnectedViaKWLock.IsWalkKWLock.KRectKWLock.TStep
    Uses
    Used by
  58. DeclKWLock.linked_of_walkDeclaration kindtheorem

    The head of a walk inside P links to every element of the walk.

    ∀ {X Y ι : Type} (T : KWLock.KRect X Y ι → KWLock.KRect X Y ι → Prop) {P : List (KWLock.KRect X Y ι)}
  {a : KWLock.KRect X Y ι} {l : List (KWLock.KRect X Y ι)},
  KWLock.IsWalk T (a :: l) → (∀ r ∈ a :: l, r ∈ P) → ∀ b ∈ a :: l, Relation.ReflTransGen (KWLock.TStep T P) a b
    KWLock.IsWalkKWLock.KRectKWLock.TStep
    Used by
  59. DeclKWLock.linked_mem_symmDeclaration kindtheorem

    From a member of P, every linked rectangle is a member, and the linkage reverses when the touch relation is symmetric.

    ∀ {X Y ι : Type} (T : KWLock.KRect X Y ι → KWLock.KRect X Y ι → Prop),
  (∀ {r s : KWLock.KRect X Y ι}, T r s → T s r) →
    ∀ {P : List (KWLock.KRect X Y ι)} {r s : KWLock.KRect X Y ι},
      r ∈ P → Relation.ReflTransGen (KWLock.TStep T P) r s → s ∈ P ∧ Relation.ReflTransGen (KWLock.TStep T P) s r
    KWLock.KRectKWLock.TStep
    Used by
  60. DeclKWLock.ColTouch.symmDeclaration kindtheorem
    ∀ {X Y ι : Type} {r s : KWLock.KRect X Y ι}, KWLock.ColTouch r s → KWLock.ColTouch s r
    KWLock.ColTouchKWLock.KRectKWLock.KRect.cols
    Used by
  61. DeclKWLock.fA_ontoDeclaration kindtheorem

    The base function is surjective.

    ∀ (b : Bool), ∃ u, KWLock.fA u = b
    KWLock.fA
    Used by
  62. DefinitionKWLock.ColConnecteddef

    Column connectivity.

    {X Y ι : Type} → List (KWLock.KRect X Y ι) → Prop
  63. DefinitionKWLock.ColTouchdef

    Two rectangles touch on columns when some column lies in both column sets.

    {X Y ι : Type} → KWLock.KRect X Y ι → KWLock.KRect X Y ι → Prop
  64. DefinitionKWLock.ConnectedViadef

    The touch graph of P is connected.

    {X Y ι : Type} → (KWLock.KRect X Y ι → KWLock.KRect X Y ι → Prop) → List (KWLock.KRect X Y ι) → Prop
  65. DefinitionKWLock.Fddef

    The d-th iterate of the base function.

    (k : ℕ) → ((Fin k → Bool) → Bool) → (d : ℕ) → KWLock.Sp k d → Bool
  66. DefinitionKWLock.IsPartitionstructure

    A valid partition of the product RX × CY into nonempty rectangles: contained, pairwise cell-disjoint, covering.

    {X Y ι : Type} → Finset X → Finset Y → List (KWLock.KRect X Y ι) → Prop
  67. DefinitionKWLock.IsWalkdef

    A walk: consecutive elements touch.

    {X Y ι : Type} → (KWLock.KRect X Y ι → KWLock.KRect X Y ι → Prop) → List (KWLock.KRect X Y ι) → Prop
  68. DefinitionKWLock.KRectstructure

    A labeled rectangle: row and column sets, a coordinate label, and the rectangle's orientation (true when rows carry value true at the label). The atomicity results never read label/orient; the composition and validity results do.

    Type → Type → Type → Type
  69. DefinitionKWLock.KRect.Celldef

    Cell membership.

    {X Y ι : Type} → KWLock.KRect X Y ι → X → Y → Prop
  70. DefinitionKWLock.KRect.colsdef
    {X Y ι : Type} → KWLock.KRect X Y ι → Finset Y
  71. DefinitionKWLock.KRect.labeldef
    {X Y ι : Type} → KWLock.KRect X Y ι → ι
  72. DefinitionKWLock.KRect.orientdef
    {X Y ι : Type} → KWLock.KRect X Y ι → Bool
  73. DefinitionKWLock.KRect.rowsdef
    {X Y ι : Type} → KWLock.KRect X Y ι → Finset X
  74. DefinitionKWLock.Labdef

    Physical coordinates at depth d: paths of blocks ending in a base coordinate.

    ℕ → ℕ → Type
  75. DefinitionKWLock.MonoValiddef

    Per-rectangle monochromaticity relative to valuations: rows carry the rectangle's orientation at its label, columns the negation.

    {X Y ι : Type} → (X → ι → Bool) → (Y → ι → Bool) → List (KWLock.KRect X Y ι) → Prop
  76. DefinitionKWLock.Protocolinductive

    A deterministic protocol tree: the row player splits the current row set, the column player the current column set; leaves announce rectangles.

    Type → Type → Type → Type
  77. DefinitionKWLock.Protocol.Followsdef

    The protocol respects the current rectangle (RX, CY): each split partitions the live side, and every leaf rectangle sits inside its branch's constraints.

    {X Y ι : Type} → [DecidableEq X] → [DecidableEq Y] → Finset X → Finset Y → KWLock.Protocol X Y ι → Prop
  78. DefinitionKWLock.Protocol.brecOn.godef
    {X Y ι : Type} →
  {motive : KWLock.Protocol X Y ι → Sort u} →
    (t : KWLock.Protocol X Y ι) →
      ((t : KWLock.Protocol X Y ι) → KWLock.Protocol.below t → motive t) → motive t ×' KWLock.Protocol.below t
  79. DefinitionKWLock.Protocol.leavesdef

    The leaves of a protocol tree.

    {X Y ι : Type} → KWLock.Protocol X Y ι → List (KWLock.KRect X Y ι)
  80. DefinitionKWLock.Realizesdef

    t realizes the partition P on (RX, CY): it follows the tree constraints and its leaves are exactly the members of P.

    {X Y ι : Type} →
  [DecidableEq X] → [DecidableEq Y] → Finset X → Finset Y → List (KWLock.KRect X Y ι) → KWLock.Protocol X Y ι → Prop
  81. DefinitionKWLock.RowConnecteddef

    Row connectivity.

    {X Y ι : Type} → List (KWLock.KRect X Y ι) → Prop
  82. DefinitionKWLock.RowTouchdef

    Two rectangles touch on rows when some row lies in both row sets.

    {X Y ι : Type} → KWLock.KRect X Y ι → KWLock.KRect X Y ι → Prop
  83. DefinitionKWLock.Spdef

    The input space of the d-th iterate: Sp 1 is the base pattern space.

    ℕ → ℕ → Type
  84. DefinitionKWLock.TStepdef

    One linkage step inside P: the target is a member and the rectangles touch.

    {X Y ι : Type} →
  (KWLock.KRect X Y ι → KWLock.KRect X Y ι → Prop) →
    List (KWLock.KRect X Y ι) → KWLock.KRect X Y ι → KWLock.KRect X Y ι → Prop
  85. DefinitionKWLock.TowerHypstructure

    The base hypotheses of the tower: a valid, monochromatic, doubly-connected base partition with two distinct members, over a surjective base function.

    (k : ℕ) → ((Fin k → Bool) → Bool) → List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k)) → Prop
  86. DefinitionKWLock.blockPatdef

    The block pattern of a composed point: the vector of block outputs.

    {k : ℕ} → {V : Fin k → Type} → ((i : Fin k) → V i → Bool) → ((i : Fin k) → V i) → Fin k → Bool
  87. DefinitionKWLock.colSideSeldef

    The column side of a block rectangle, in a given orientation.

    {k : ℕ} → {V κ : Fin k → Type} → Bool → {a : Fin k} → KWLock.KRect (V a) (V a) (κ a) → Finset (V a)
  88. DefinitionKWLock.compFundef

    The composed function.

    {k : ℕ} → {V : Fin k → Type} → ((i : Fin k) → V i → Bool) → ((Fin k → Bool) → Bool) → ((i : Fin k) → V i) → Bool
  89. DefinitionKWLock.compPartitiondef

    The product partition of the composed game.

    {k : ℕ} →
  {V : Fin k → Type} →
    [(i : Fin k) → DecidableEq (V i)] →
      [(i : Fin k) → Fintype (V i)] →
        {κ : Fin k → Type} →
          ((i : Fin k) → V i → Bool) →
            List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k)) →
              ((i : Fin k) → List (KWLock.KRect (V i) (V i) (κ i))) →
                List (KWLock.KRect ((i : Fin k) → V i) ((i : Fin k) → V i) ((i : Fin k) × κ i))
  90. DefinitionKWLock.compRectdef

    The composed rectangle: outer patterns from the outer rectangle, the active block constrained to the block rectangle's side in the outer orientation, other blocks free. The label is the physical coordinate; the orientation composes.

    {k : ℕ} →
  {V : Fin k → Type} →
    [(i : Fin k) → DecidableEq (V i)] →
      [(i : Fin k) → Fintype (V i)] →
        {κ : Fin k → Type} →
          ((i : Fin k) → V i → Bool) →
            (Ro : KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k)) →
              KWLock.KRect (V Ro.label) (V Ro.label) (κ Ro.label) →
                KWLock.KRect ((i : Fin k) → V i) ((i : Fin k) → V i) ((i : Fin k) × κ i)
  91. DefinitionKWLock.fAdef

    The four-variable Ambainis function, in Ueno's ten-leaf form (truth table 0xd18b: exactly the monotone four-bit sequences evaluate to one).

    (Fin 4 → Bool) → Bool
  92. DefinitionKWLock.instDecidableCellOfDecidableEqdef
    {X Y ι : Type} →
  [DecidableEq X] → [DecidableEq Y] → (r : KWLock.KRect X Y ι) → (x : X) → (y : Y) → Decidable (r.Cell x y)
  93. DefinitionKWLock.instDecidableColTouchOfDecidableEqdef
    {X Y ι : Type} → [DecidableEq Y] → (r s : KWLock.KRect X Y ι) → Decidable (KWLock.ColTouch r s)
  94. DefinitionKWLock.instDecidableEqKRectdef
    {X Y ι : Type} → [DecidableEq X] → [DecidableEq Y] → [DecidableEq ι] → DecidableEq (KWLock.KRect X Y ι)
  95. DefinitionKWLock.instDecidableEqSpdef
    (k d : ℕ) → DecidableEq (KWLock.Sp k d)
  96. DefinitionKWLock.instDecidableIsWalkdef
    {X Y ι : Type} →
  (T : KWLock.KRect X Y ι → KWLock.KRect X Y ι → Prop) →
    [(r s : KWLock.KRect X Y ι) → Decidable (T r s)] → (w : List (KWLock.KRect X Y ι)) → Decidable (KWLock.IsWalk T w)
  97. DefinitionKWLock.instDecidableRowTouchOfDecidableEqdef
    {X Y ι : Type} → [DecidableEq X] → (r s : KWLock.KRect X Y ι) → Decidable (KWLock.RowTouch r s)
  98. DefinitionKWLock.instFintypeSpdef
    (k d : ℕ) → Fintype (KWLock.Sp k d)
  99. DefinitionKWLock.onesOfdef

    The ones of a Boolean function, as a finite set.

    {α : Type} → [Fintype α] → (α → Bool) → Finset α
  100. DefinitionKWLock.pAdef

    The witness partition.

    List (KWLock.KRect (Fin 4 → Bool) (Fin 4 → Bool) (Fin 4))
  101. DefinitionKWLock.rA1def

    The eight-rectangle base partition, found by exact search and re-verified by the kernel below: eight monochromatic rectangles of eight cells each, in mixed orientations.

    KWLock.KRect (Fin 4 → Bool) (Fin 4 → Bool) (Fin 4)
  102. DefinitionKWLock.rA2def
    KWLock.KRect (Fin 4 → Bool) (Fin 4 → Bool) (Fin 4)
  103. DefinitionKWLock.rA3def
    KWLock.KRect (Fin 4 → Bool) (Fin 4 → Bool) (Fin 4)
  104. DefinitionKWLock.rA4def
    KWLock.KRect (Fin 4 → Bool) (Fin 4 → Bool) (Fin 4)
  105. DefinitionKWLock.rA5def
    KWLock.KRect (Fin 4 → Bool) (Fin 4 → Bool) (Fin 4)
  106. DefinitionKWLock.rA6def
    KWLock.KRect (Fin 4 → Bool) (Fin 4 → Bool) (Fin 4)
  107. DefinitionKWLock.rA7def
    KWLock.KRect (Fin 4 → Bool) (Fin 4 → Bool) (Fin 4)
  108. DefinitionKWLock.rA8def
    KWLock.KRect (Fin 4 → Bool) (Fin 4 → Bool) (Fin 4)
  109. DefinitionKWLock.rowSideSeldef

    The row side of a block rectangle, in a given orientation (the transposed side for the reversed orientation).

    {k : ℕ} → {V κ : Fin k → Type} → Bool → {a : Fin k} → KWLock.KRect (V a) (V a) (κ a) → Finset (V a)
  110. DefinitionKWLock.towerPdef

    The tower of product partitions: depth 0 is the base partition; each next depth composes the base as the outer partition with the previous depth at every block.

    (k : ℕ) →
  ((Fin k → Bool) → Bool) →
    List (KWLock.KRect (Fin k → Bool) (Fin k → Bool) (Fin k)) →
      (d : ℕ) → List (KWLock.KRect (KWLock.Sp k (d + 1)) (KWLock.Sp k (d + 1)) (KWLock.Lab k d))
  111. DefinitionKWLock.vvaldef

    The valuation of an iterate point at a physical coordinate.

    (k d : ℕ) → KWLock.Sp k (d + 1) → KWLock.Lab k d → Bool
  112. DefinitionKWLock.zerosOfdef

    The zeros of a Boolean function, as a finite set.

    {α : Type} → [Fintype α] → (α → Bool) → Finset α
DOIMTH.R-2026-6014
Cite

Verification

Replay
accepted
Axioms
Classical.choiceQuot.soundpropext
Statement identity
not-applicable
Substrate
Lean 4 kernel v4.31.0
Dictionary pin
design-lab@5802df4 · initial
Frozen export
d7bd4a249109
Verified
2026-09-24T00:00:00Z