Jensen’s square principle with its order-type bound

Work in ZFC. For an infinite cardinal $\kappa$, let ${\kappa }^{+}$ be its successor cardinal, and use the ordinal order on cardinals as in Cardinal (initial ordinal) and cardinality. A ${\mathrm{\square }}_{\kappa }$-sequence is $(C_{\alpha })$ indexed by the nonzero limits $\alpha <{\kappa }^{+}$ such that $C_{\alpha }$ is club in $\alpha$, its ordinal order type satisfies $\mathrm{otp}(C_{\alpha })\le \kappa$, and

$\beta \in {\mathrm{acc}}_{\alpha }(C_{\alpha })⟹C_{\beta }=C_{\alpha }\cap \beta \mathrm{.}$

Club and nonzero limit points have the meanings in Closed unbounded subsets of ordinals. The principle ${\mathrm{\square }}_{\kappa }$ asserts existence of such a sequence. The bound is on ordinal order type, which is stronger than cardinality at most $\kappa$. A thread would be a club $D\subseteq {\kappa }^{+}$ with $D\cap \alpha =C_{\alpha }$ at every nonzero limit point $\alpha$ of $D$.

The stated order-type bound already excludes a thread. Assume AC as in The Axiom of Choice. The successor-cardinal regularity theorem ${\mathrm{\aleph }}_0$ is regular in ZF; assuming the Axiom of Choice every successor aleph ${\mathrm{\aleph }}_{\alpha +1}$ is regular; $\mathrm{cf}({\mathrm{\aleph }}_{\omega })={\mathrm{\aleph }}_0$, so ${\mathrm{\aleph }}_{\omega }$ is singular, and under choice it is the least singular infinite cardinal makes ${\kappa }^{+}$ regular, so the increasing enumeration $d$ of its unbounded subset $D$ has domain ${\kappa }^{+}$: its order type is at most ${\kappa }^{+}$ as a subset of that ordinal and its cofinality forces cardinality ${\kappa }^{+}$. Closedness gives continuity at nonzero limit indices. Choose the particular limit index $\xi =\kappa +\omega$. Cardinal absorption Absorption: for cardinals $\kappa ,\lambda$ with $\kappa$ infinite and $\lambda \le \kappa$, $\kappa \oplus \lambda =\kappa$, and $\kappa \otimes \lambda =\kappa$ when $\lambda \mathrm{\ne }0$ gives $\mathrm{\mid }\xi \mathrm{\mid }=\kappa$, so $\kappa <\xi <{\kappa }^{+}$. At $\alpha =d(\xi )$, continuity makes $\alpha$ a limit point of $D$ and $D\cap \alpha =d[\xi ]$ has order type $\xi >\kappa$. A thread would identify it with $C_{\alpha }$, contrary to the bound. This includes $\kappa =\omega$, where $\xi =\omega +\omega$.

There are no square entries at zero or successor indices in this convention. This is the width-one square principle at the successor of $\kappa$; no constructibility assumption or implication is part of its definition.