AI 中文总结
本研究提出三维强非周期单瓦片 Chair44，通过形状特征强制非周期性，证明其平铺无平移周期且对称群阶有限，并给出机器验证的严格证明。
AI 中文摘要
Socolar 和 Taylor 曾寻求一个单一、单连通的三维原型瓦片，仅凭形状本身强制非周期性，且不允许弱非周期平铺；Schmitt-Conway-Danzer 双棱柱和三维 Socolar-Taylor 瓦片允许螺旋运动或周期性堆叠方向。我们展示一个有理多面体 $3$-球 $Q$，称之为 Chair44 (R44)：一个七立方体椅子，其 $24$ 个暴露的单位面板带有微小的方形金字塔特征，并作为证明提交，证明 $Q$ 允许通过全等副本（允许反射）平铺 $\mathbb{R}^3$，且每个这样的平铺没有平移周期，对称群阶至多为 $24$；每个平铺都是同手性的，并带有唯一的无限嵌套超瓦片层级。该实体是根据“六鸟涌现演算”（第 3.3 节）所达到的非周期单瓦片现象的一种解读而设计的，构造依赖于一个由机器检查的单一有限测试：瓦片自身的接触规则在粗化后仍然成立，因此解码后的父平铺遵循瓦片的规则且无其他规则。证明结合了书面几何论证（即特征迫使每个平铺落在注册格上）与穷举有限枚举；伴随的普查由两个独立实现重放，每个有限门在 Lean 4 中通过内核检查（每个 native_decide 定理附带一个命名的编译器钩子），书面几何引理和逻辑组装也是 Lean 定理，因此该定理在内核检查下（模命名的编译器钩子）成立；书面证明仅作为说明。
英文摘要
Socolar and Taylor asked for a single, simply connected three-dimensional prototile that forces nonperiodicity by shape alone, admitting no weakly nonperiodic tiling; the Schmitt-Conway-Danzer biprism and the three-dimensional Socolar-Taylor tile admit screw motions or a periodic stacking direction. We exhibit a rational polyhedral $3$-ball $Q$, which we call Chair44 (R44): a seven-cube chair whose $24$ exposed unit panels carry tiny square-pyramid features, and prove, as a proof submission, that $Q$ admits tilings of $\mathbb{R}^3$ by congruent copies, reflections allowed, and that every such tiling has no translational period and a symmetry group of order at most $24$; every tiling is homochiral and carries a unique infinite hierarchy of nested supertiles. The solid was designed to a reading of the aperiodic-monotile phenomenon reached with the Six Birds emergence calculus (Section 3.3), and the construction turns on a single finite test, checked by machine: the tile's own contact rule survives coarsening, so that the decoded parent tiling obeys the tile's rule and no other. The proof combines a written geometric argument, that the features force every tiling onto a registered lattice, with exhaustive finite enumerations; the companion census is replayed by two independent implementations, every finite gate is kernel-checked in Lean 4 (modulo a named compiler hook per native_decide theorem), and the written geometric lemmas and the logical assembly are Lean theorems as well, so that the theorem is kernel-checked modulo the named compiler hooks; the written proofs remain as exposition.
