Irwin's hook-sum conjecture for OEIS A138099

Paul Curtz's OEIS A138099, revision 26, NAME and FORMULA blocks, contains Benedict W. J. Irwin's unnumbered conjecture:

Conjecture: a(n) = HookSum(T(n))-HookSum(T(n-1)), where HookSum(A) is the sum of all hooks across a tableau A, and T(n) are the spiraling sequence of tableaux:

The complete displayed diagrams and arithmetic rows are reproduced in Library/FiniteGeometry/irwin2016a138099.md. The arithmetic row is $R(k,j)=j+\lfloor k/2\rfloor$, for $k\geq1$ and $1\leq j\leq\lceil k/2\rceil$. Put $S(k)=\sum_{i=1}^{k}\lceil i/2\rceil$. A source sequence satisfies $a(S(k-1)+j)=R(k,j)$ on that domain, with no restriction on $a(0)$.

The literal square spiral begins at $(0,0)$, travels west, south, east, north, and repeats these directions with leg lengths $1,1,2,2,3,3,\ldots$. $T_0=\varnothing$ and $T_{n+1}$ inserts walk cell $n$ into $T_n$. For occupied integer cells, an ordinary hook contains its own cell and the occupied cells strictly right in its row and strictly below in its column. $H(D)$ sums these hook lengths; $H(\varnothing)=0$.

Statement echo

| Source clause or binding interpretation | Lean counterpart | Scope | | --- | --- | --- | | Irregular triangle read by rows | triangleEntry, trianglePrefix, IsSourceSequence | Every positive row and admissible column; index zero unused | | Spiraling sequence of the displayed tableaux | legDirection, WalkState, advance, walk, IsSourceSpiral | Actual occupied positions; no Ferrers replacement | | Sum of all ordinary hooks | hookLength, hookSum | Every finite integer-cell diagram, including holes | | Both implicitly specified sequences exist | First two conjuncts of claim | Conclusions, not hypotheses | | Every source sequence and source spiral | Universal binders and two source predicates in claim | No extra shape assumptions | | Increment at every positive index | Final conjunct of claim, proved by result | Both hook sums cast to integers before subtraction |

The finite cell carrier is the existing type $\mathbb Z\times\mathbb Z$. The counters implement the literal walk; they add no hypothesis to the source identity. Natural division has positive denominator two, remainder has positive modulus four, and the predecessor expressions are guarded by positive indices.

The settling declaration is D5/S3/Combinatorics/Polyomino/IrwinA138099HookSum.result. It proves the full identity, including both existence conclusions. Issue #23678 preregisters the source statement, literal definitions, tier-1 classification and proposed square/strip bridge. The module uses admission_basis: open-problem-resolution (#23678; Proved) and utility: none: the proof is symbolic over arbitrary indices, with no finite numerical certificate as new mathematical content.

The source labels the formula a conjecture and supplies no proof. The bounded literature screen recorded in #23678 found no settlement in the material actually read. It covers the source and history, arXiv metadata and selected full-text searches, Zenodo metadata, MathDB, formal-conjectures, sequence implementations and the repository. The partition hook identities in arXiv:2205.07322v1 and arXiv:1508.00772v3 do not state this spiral/triangle assertion. Completeness is ASSUMED-UNVERIFIED: citation APIs were rate-limited, MathOverflow access failed, later-author full texts remained unread, and capped metadata searches do not clear all prior art.

The private helper hook_sum_insert proves that inserting a fresh cell $p$ into an arbitrary finite diagram $D$ gives $H(D\cup{p})=H(D)+1+r+c$, where $r$ and $c$ are the old row and column sizes. The proof partitions each line about $p$ and sums hook changes.

The private square_invariant and layer_diagrams identify the actual walk with a complete $m$ by $m$ square followed by its two boundary strips. At the $j$th insertion in the first strip the old line sizes are $(m,j-1)$; in the second they are $(j-1,m)$. Thus both increments are $m+j$. The private first_block and second_block compare these with rows $2m$ and $2m+1$, using $S(2m-1)=m^2$ for $m\geq1$ and $S(2m)=m^2+m$ for $m\geq0$. The singleton at $m=0$ is handled separately. Row addresses construct a source arithmetic sequence, while insertion constructs and uniquely determines the spiral sequence. These arguments are used by result.

A mismatch in the occupied-cell interpretation, unit-step order, one-based arithmetic indexing, ordinary right/down hooks or integer subtraction would invalidate the source correspondence. The public statement retains these conventions and both existence conclusions. No bounded computation is used to infer the all-index conclusion.

• Source: OEIS A138099 revision 26; its complete NAME, Irwin FORMULA, diagrams and example rows are in the Library note.
• Preregistration and literature scope: #23678.
• Lean: D5/S3/Combinatorics/Polyomino/IrwinA138099HookSum.lean, namespace D5.S3.Combinatorics.Polyomino.IrwinA138099HookSum.
• The public theorem is result : claim. Its claim includes existence of both objects and the equality at every positive index.
• Escape audit unfinished: #25040. The whole conjunction needs a faithful enrolled realization and source reconstruction, bridge, variation, sensitivity and dependence evidence. No Reg registration is supplied or claimed complete.

Exact-arithmetic experiment

Experiment directory at b86f125a1e8275098b8eb697908ea40b1ec1dad9. The script is docs/reports/irwin-a138099/check.py, SHA-256 0348041fc8d9768048ffc0b3d53ad661ec9228238d275e27ad4187b326e9c33a. Command: python3 /tmp/op-irwin138099/stageb/check.py, exit 0; the executed file is the byte-identical extraction of that immutable blob. It matches all 77 published terms, eight arithmetic rows and ten diagrams (empty through nine cells) by translation; Merca's formula and direct hook increments for $1\leq n\leq1001$; direct hooks against pair counts for $0\leq n\leq1001$; and all eight coordinate symmetries for $0\leq n\leq100$. The final result is ALL_CHECKS_OK. These are bounded computations, separate from the universal Lean proof.

What the settlement shows

| Item | Status and evidence kind | Result and boundary | | --- | --- | --- | | Fresh insertion in an arbitrary finite integer-cell diagram | Proved; kernel-checked private hook_sum_insert | Change is $1+r+c$; neither holes nor absence of Ferrers structure causes an exception | | Squares, strips, no repetition, cardinality and injectivity | Proved; kernel-checked private square_invariant, layer_walk, layer_diagrams, column_counts, row_counts for the geometric assertions; proof in prose below for cardinality and injectivity | Literal walk, every index | | Two strip blocks and singleton base | Proved; kernel-checked private first_block, second_block, used by public result | Source rows $2m$ and $2m+1$; singleton $m=0$ retained | | Published terms, rows and diagrams; increments, pair counts and symmetries | Computed; exact-arithmetic experiment above | Exactly the finite ranges stated in Evidence | | Other growth paths | Open | Require their own strip counts and source-index bridge | | Downstream source results using this conjecture | Computed source-document inspection; the complete OEIS entry read in #23678 | The entry states no downstream theorem depending on the conjecture; this is a document-scope finding, not a statement about all literature |

For cardinality and injectivity, the geometric lemmas give freshness of each inserted cell: every positive index lies in exactly one of the two row-address blocks, whose column_counts or row_counts excludes the next cell from the old diagram. The first cell is outside the empty set. By induction, inserting a fresh cell increases cardinality by one, so $|T_n|=n$. If walk cells $i<j$ were equal, the cell at $i$ would already belong to $T_j$, contradicting freshness at $j$. This is a proof in prose from the indicated formal geometry; no additional public Lean theorem for cardinality or injectivity is claimed.

For any finite diagram, each horizontal or vertical unordered pair of cells contributes exactly once to the hook sum. Hence $H(D)=|D|+\sum_y\binom{r_y}{2}+\sum_x\binom{c_x}{2}$. This is a proof in prose by assigning each pair to its left or upper cell. It explains orientation invariance and why only old line sizes matter at insertion. At the complete square $T_{m^2}$, its $m$ rows and $m$ columns all have size $m$, so the same argument gives $H(T_{m^2})=m^2+2m\binom m2=m^3$ (proved in prose). These explanations are not separately claimed as kernel-checked statements. Other growth paths remain open. No source downstream conclusion needs adjustment because none is stated in the read entry.

• Literature-screen completeness, unread later-author full texts and unresolved citation-graph/MathOverflow access; this is no priority claim.
• Exhaustiveness beyond the exact OEIS entry for the downstream-source inspection. The bounded experiment does not establish other growth paths or an unbounded symmetry claim.
• Four-slot escape registration for result; the missing evidence and audit target are recorded in #25040.