The attainable numbers of tiles in O_N-tile decompositions

The source's eleven printed O₃-tile decompositions of Z₃³ (s = 5..15) all check against the source's own definition

The bitmask model is the source's: formsTile S holds exactly when S is the cell set of a tile, and allTiles is all 343 tile codes

Z₃ x Z₃ x Z₃ admits no O₃-tile decomposition with exactly 3 tiles, and none with exactly 4

Every clause of the source's definition is refutable, and the sub-union quantifier is strictly stronger than its |J| = 2 instances

External, not certified in Lean: the attainable spectrum for Z₃ x Z₃ x Z₃ is exactly 5,...,15, with 5 064 336 decompositions in total; after ot-3 and ot-7 the only cell this row is load-bearing for is s = 16

No two tiles of an O₃-tile decomposition merge, hence no two agree in two of their three factor sets

Z₃ x Z₃ x Z₃ admits no O₃-tile decomposition with 17 or more tiles; and one with exactly 16 would consist of five single cells and eleven dominoes

Z₃ × Z₃ × Z₃ admits no O₃-tile decomposition with exactly 16 tiles

The attainable numbers of tiles for Z₃ × Z₃ × Z₃ are exactly 5,6,…,15 — the source's Problem 2, answered

Controls on the s = 16 search: it does not close for a degenerate reason, and it reproduces the external enumeration's own leaf count

The source's definitions over a general box Z_(d₁)×⋯×Z_(d_N), and the proof that at [3,3,3] they are the landed 3-cube model

The counting bound α·s ≤ λ·∏dᵢ + ∑_q ∏_(j≠q) dⱼ for a general box, with the merge lemma it rests on

Z₂×Z₃×Z₃ admits no O₃-tile decomposition with 3 or 4 tiles, and none with 12 or more; an 11-tile one would have every tile of at most three cells

Controls: every clause of def:ON-tile is refutable at Z₂×Z₃×Z₃, and the | J | =2 relaxation is strictly weaker even at the value the counting bound leaves open

The authors' own decompositions for Z₂×Z₃×Z₃ (s=5..10) and for [3,3,4], [3,3,5], [3,4,4], [2,3,3,3] (s=5..16) all check against the source's own definition

Upper bounds for the four larger boxes: s ≤ 21 on Z₃×Z₃×Z₄, s ≤ 25 on Z₃×Z₃×Z₅, s ≤ 27 on Z₃×Z₄×Z₄, s ≤ 34 on the quadripartite Z₂×Z₃×Z₃×Z₃

s = 3 is not attainable on any of Z₃×Z₃×Z₄, Z₃×Z₃×Z₅, Z₃×Z₄×Z₄, Z₂×Z₃×Z₃×Z₃, and s = 4 is not attainable on Z₃×Z₃×Z₄

External, not certified in Lean: the attainable spectrum is exactly 5,…,10 for Z₂×Z₃×Z₃ and exactly 5,…,20 for Z₃×Z₃×Z₄; s = 25 is unattainable on Z₃×Z₃×Z₅ and s = 27 on Z₃×Z₄×Z₄

The leaf test: Definition def:ON-tile's 2ˢ quantifier replaced by a scan of the tile alphabet, for a general box Z_(d₁)×⋯×Z_(d_N)

The sound depth-first search over an arbitrary box: Sixteen.lean's go/goₛound with the box, the tables and the budgets all free

Z₂×Z₃×Z₃ admits no O₃-tile decomposition with eleven tiles, so the attainable set is exactly 5,…,10

Every witness the authors' SAT archive contains for [3,3,4], [3,3,5], [3,4,4] and [2,3,3,3] — s up to 20, 23, 24 and 30 — certified against the source's own definition

Z₃×Z₃×Z₄ is decided at every number of tiles but one: s ∈ 5,…,20 iff attainable, for every s ≠ 21

Controls: the leaf test rejects what the definition rejects even where no pair merges, and the s = 11 search is not closing for a degenerate reason

The cell-mask encoding at the bit level: testBitₛpread and the cellsOf calculus (&&&, one-coordinate |||, monotonicity, the full code) for an arbitrary box, kernel-clean

The merge sweep is a theorem at every box: mergeSweepₜrue, hence tiles_disagree_gen kernel-clean everywhere

s = 3 is unattainable at every box Z_(d₁) × ⋯ × Z_(d_N) — no_decompₜhree_gen / threeₙotₐttainable, no search, no native axiom

Z₂ × Z₂ × Z₂ answered in full: the attainable numbers of tiles are exactly 5 — attainable₂22ᵢff, with zero native axioms (s=4 by decide +kernel)

Controls for the general theorem: a genuine 3-tile partition rejected only by the sub-union clause (with the predicted J = 2,3 merge exhibited), instantiations at Z₂¹⁰⁰ and Z_(10⁶) × Z_(10⁶), and the landed [3,3,4] sweep re-proved as an instance

Z₂ × Z₂ × Z₃ answered in full: the attainable numbers of tiles are exactly 5, 6, 7 — attainable₂23ᵢff, one native axiom (the s = 4 sweep); s = 8 decided for the first time, in the kernel

Controls on the s = 8 search: without the prune it reaches the census's 1 149 four-singles-four-dominoes covers; with the seven-tile budget it reaches the census's 24 seven-tile decompositions

s = 4 is unattainable at every bipartite box Zₘ × Zₙ; with ot-27 and s = 5 attained at [3,3], the minimum bipartite O₂-tile count is exactly 5

Z₂⁴ answered in full: the attainable numbers of tiles are exactly 5, 7, 8, 9 – attainable₂222ᵢff, the family's first spectrum with a hole; one native axiom (the s = 4 sweep), the three new negative cells kernel-clean

Controls at Z₂⁴: a six-tile tile partition with no mergeable pair whose smallest violating index set has |J| = 5, and four goCount runs that reproduce the independent census exactly

The counting bound at the all-qubit boxes run at (alpha, lambda) = (2N-1, N-1): s <= 23 on Z₂⁵, s <= 46 on Z₂⁶, s <= 93 on Z₂⁷ – strictly better than the UPB-shadow bound 2^N + 1 - f(N) = 27, 57, 121

At every all-qubit box Z₂^N, (2N-1)*s <= 2^(N-1)(3N-2), and this is the best bound BoundGen's two statistics can give there

The UPB-shadow bound s <= 2^N + 1 - f(N) at all-qubit boxes, with its two citations – and the correction that it is weaker than BoundGen from N = 5 on

Padding: prepending a full Z_d factor to every tile of an O_N-tile decomposition of C gives one of Z_d × C, so the attainable set is monotone under adding coordinates — at every box, dims and d free

Z₂⁵ decided in Lean at every number of tiles except s = 21, 22: the attainable values are 5 and 7,…,20

Controls at Z₂⁵: a six-tile tile partition with no mergeable pair, and goCount runs that reproduce the independent census exactly

External, not certified in Lean: the labelled Z₂⁵ census — 12 453 120 O₅-tile decompositions, 80 at s = 5, none at s = 6, 2 880, 1 000, 47 280, …, 3 840 at s = 7,…,20, none at s = 21, 22, 23; and the maximum-size one is unique up to isomorphism

Erratum: at an all-qubit box — and only there — the source's O_N-tile decompositions are exactly the irreducible subcube partitions of 0,1^N, so ot-35's "no such upper bound appears anywhere" is false, its bound is superseded, and the s = 4, 6 gaps are published