A nonheavy partition below a heavy rectangle

Abstract

The PNim heavy-interval conjecture fails at a = 8, b = 7.

Definition 1.1 (Row lengths).

$$Position=\mathrm{List}\left(\mathrm{Nat}\right)$$

Formalization. D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.Position (✓ std3).

Citation. Eric Gottlieb; Matjaž Krnc; Peter Muršič (2025). Nim on Integer Partitions and Hyperrectangles. DOI: 10.48550/arXiv.2506.04991. URL: https://arxiv.org/abs/2506.04991.

Commentary.

Positions are lists of natural row lengths. The predicate IsPartition restricts them to nonincreasing positive lists, including the empty list.

Definition 1.2 (Deleting diagram columns).

$$\forall p\in Position,\forall deleted\in Position,\mathrm{deleteColumns}\left(p,deleted\right)=List.filter\left((\lambda n\mapsto n\ne 0),List.map\left((\lambda n\mapsto n-List.length\left(List.filter\left((\lambda j\mapsto j<n),deleted\right)\right)),p\right)\right)$$

Formalization. D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.deleteColumns (✓ std3).

Citation. Eric Gottlieb; Matjaž Krnc; Peter Muršič (2025). Nim on Integer Partitions and Hyperrectangles. DOI: 10.48550/arXiv.2506.04991. URL: https://arxiv.org/abs/2506.04991.

Commentary.

Columns are numbered from zero. Each row n loses precisely the deleted indices j smaller than n; rows reduced to zero are omitted. Remaining columns merge. The filter tests are Boolean comparisons. The deleted list is generated without repetition from the first-row column range.

Definition 1.3 (Deleting nonempty row subsets).

$$\forall p\in Position,\mathrm{rowMoves}\left(p\right)=List.filter\left((\lambda q\mapsto \mathrm{length}\left(q\right)<\mathrm{length}\left(p\right)),List.sublists\left(p\right)\right)$$

Formalization. D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.rowMoves (✓ std3).

Citation. Eric Gottlieb; Matjaž Krnc; Peter Muršič (2025). Nim on Integer Partitions and Hyperrectangles. DOI: 10.48550/arXiv.2506.04991. URL: https://arxiv.org/abs/2506.04991.

Commentary.

List.sublists enumerates all retained row subsequences. Strictly smaller length selects exactly deletions of at least one row; the empty subsequence deletes every row.

Definition 1.4 (Deleting nonempty column subsets).

$$\forall p\in Position,\mathrm{columnMoves}\left(p\right)=List.map\left((\lambda deleted\mapsto \mathrm{deleteColumns}\left(p,deleted\right)),List.filter\left((\lambda deleted\mapsto deleted\ne []),List.sublists\left(List.range\left(\mathrm{headD}\left(p,0\right)\right)\right)\right)\right)$$

Formalization. D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.columnMoves (✓ std3).

Citation. Eric Gottlieb; Matjaž Krnc; Peter Muršič (2025). Nim on Integer Partitions and Hyperrectangles. DOI: 10.48550/arXiv.2506.04991. URL: https://arxiv.org/abs/2506.04991.

Commentary.

The first row supplies every diagram column of a partition. All nonempty subsets of its zero-based range are deleted by deleteColumns. headD(p,0) is the first row, with default zero for the empty list.

Definition 1.5 (All PNim followers).

$$\forall p\in Position,\mathrm{moves}\left(p\right)=List.filter\left((\lambda q\mapsto \mathrm{sum}\left(q\right)<\mathrm{sum}\left(p\right)),List.append\left(\mathrm{rowMoves}\left(p\right),\mathrm{columnMoves}\left(p\right)\right)\right)$$

Formalization. D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.moves (✓ std3).

Citation. Eric Gottlieb; Matjaž Krnc; Peter Muršič (2025). Nim on Integer Partitions and Hyperrectangles. DOI: 10.48550/arXiv.2506.04991. URL: https://arxiv.org/abs/2506.04991.

Commentary.

The row and column options are concatenated, then restricted to strictly smaller cell count. This last filter changes no move of a positive nonincreasing partition. It extends termination to arbitrary natural lists. Repeated followers do not affect the finite set used by mex.

Definition 1.6 (Grundy evaluation by cell count).

$$\forall p\in Position,\mathrm{grundy}\left(p\right)=\mathrm{mex}\left(\left\{\mathrm{grundy}\left(q\right)\mid q\in \mathrm{moves}\left(p\right)\right\}\right)$$

Formalization. D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.grundy (✓ std3).

Citation. Eric Gottlieb; Matjaž Krnc; Peter Muršič (2025). Nim on Integer Partitions and Hyperrectangles. DOI: 10.48550/arXiv.2506.04991. URL: https://arxiv.org/abs/2506.04991.

Commentary.

mex is the frozen least-excluded-value function of CrimGrundyRefutation, imported rather than restated. The Lean definition uses well-founded recursion on cell count; the termination measure is discharged inside the definition and is not part of the mathematical statement. The terminal empty list has value zero.

Definition 1.7 (Positive nonincreasing partitions).

$$\forall p\in Position,(\mathrm{IsPartition}\left(p\right))\iff ((List.Pairwise\left((\lambda x\mapsto (\lambda y\mapsto x\ge y)),p\right))\wedge (List.all\left((\lambda n\mapsto n>0),p\right)=true))$$

Formalization. D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.IsPartition (✓ std3).

Citation. Eric Gottlieb; Matjaž Krnc; Peter Muršič (2025). Nim on Integer Partitions and Hyperrectangles. DOI: 10.48550/arXiv.2506.04991. URL: https://arxiv.org/abs/2506.04991.

Commentary.

Pairwise requires each earlier row to be at least each later row. The Boolean all test requires every row length to be positive.

Definition 1.8 (Young’s-lattice order).

$$\forall p\in Position,\forall q\in Position,(\mathrm{youngLE}\left(p,q\right))\iff ((\mathrm{length}\left(p\right)\le \mathrm{length}\left(q\right))\wedge (List.all\left((\lambda pair\mapsto \mathrm{fst}\left(pair\right)\le \mathrm{snd}\left(pair\right)),List.zip\left(p,q\right)\right)=true))$$

Formalization. D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.youngLE (✓ std3).

Citation. Eric Gottlieb; Matjaž Krnc; Peter Muršič (2025). Nim on Integer Partitions and Hyperrectangles. DOI: 10.48550/arXiv.2506.04991. URL: https://arxiv.org/abs/2506.04991.

Commentary.

The lower list must be no longer than the upper list, and each aligned pair must satisfy first component at most second component. zip therefore checks every lower row. fst and snd denote pair projections.

Definition 1.9 (The upper rectangle).

$$\forall a\in \mathrm{Nat},\forall b\in \mathrm{Nat},\mathrm{rectangle}\left(a,b\right)=List.replicate\left(b+1,a+1\right)$$

Formalization. D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.rectangle (✓ std3).

Citation. Eric Gottlieb; Matjaž Krnc; Peter Muršič (2025). Nim on Integer Partitions and Hyperrectangles. DOI: 10.48550/arXiv.2506.04991. URL: https://arxiv.org/abs/2506.04991.

Commentary.

The rectangle contains b+1 copies of a+1, exactly the upper endpoint in printed Conjecture 2.

Definition 1.10 (The lower staircase).

$$\forall a\in \mathrm{Nat},\forall b\in \mathrm{Nat},\mathrm{staircase}\left(a,b\right)=List.map\left((\lambda i\mapsto a+1-i),List.range\left(b+1\right)\right)$$

Formalization. D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.staircase (✓ std3).

Citation. Eric Gottlieb; Matjaž Krnc; Peter Muršič (2025). Nim on Integer Partitions and Hyperrectangles. DOI: 10.48550/arXiv.2506.04991. URL: https://arxiv.org/abs/2506.04991.

Commentary.

Mapping i to a+1-i over range(b+1) gives [a+1,a,…,a-b+1]. Subtraction is natural subtraction; b at most a makes all parts positive.

Definition 1.11 (Heaviness and longest play).

$$\forall p\in Position,(\mathrm{heavy}\left(p\right))\iff ((p\ne [])\wedge (\mathrm{grundy}\left(p\right)=\mathrm{headD}\left(p,0\right)+\mathrm{length}\left(p\right)-1))$$

Formalization. D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.heavy (✓ std3).

Citation. Eric Gottlieb; Matjaž Krnc; Peter Muršič (2025). Nim on Integer Partitions and Hyperrectangles. DOI: 10.48550/arXiv.2506.04991. URL: https://arxiv.org/abs/2506.04991.

Commentary.

A nonempty partition is heavy when its Grundy value equals its first row plus its row count minus one. Proposition 2 gives exactly this longest-play length. All arithmetic here is on natural numbers.

Definition 1.12 (Conjecture 2 as printed).

$$(claim)\iff (\forall a\in \mathrm{Nat},\forall b\in \mathrm{Nat},(b\le a)\Rightarrow ((\mathrm{heavy}\left(\mathrm{rectangle}\left(a,b\right)\right))\Rightarrow (\forall p\in Position,(\mathrm{IsPartition}\left(p\right))\Rightarrow ((\mathrm{youngLE}\left(\mathrm{staircase}\left(a,b\right),p\right))\Rightarrow ((\mathrm{youngLE}\left(p,\mathrm{rectangle}\left(a,b\right)\right))\Rightarrow (\mathrm{heavy}\left(p\right)))))))$$

Formalization. D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.claim (✓ std3).

Citation. Eric Gottlieb; Matjaž Krnc; Peter Muršič (2025). Nim on Integer Partitions and Hyperrectangles. DOI: 10.48550/arXiv.2506.04991. URL: https://arxiv.org/abs/2506.04991.

Commentary.

Natural a,b with b at most a encode exactly the integer parameters for which both endpoints are partitions. For every partition p in the closed Young interval, the conjecture predicts heaviness whenever the upper rectangle is heavy.

Theorem 1.13 (The printed heavy-interval conjecture is false).

$$\neg claim$$

Proof. Machine-checked in Lean as D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.result (✓ std3). ∎

Resolves. Problems/gottlieb-krnc-mursic-pnim-heavy-interval-refutation (refuted) by D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.result.

Source. Repository-derived.

Acknowledgement. Eric Gottlieb; Matjaž Krnc; Peter Muršič (2025). Nim on Integer Partitions and Hyperrectangles. DOI: 10.48550/arXiv.2506.04991. URL: https://arxiv.org/abs/2506.04991.

Commentary.

At a=8 and b=7 the rectangle is [9,9,9,9,9,9,9,9], with Grundy value 16 and longest-play length 16. The partition [9,9,8,8,8,5,5,5] lies above [9,8,7,6,5,4,3,2] and below that rectangle, but its Grundy value is 3 rather than 16.

A finite table contains the partition and all its descendants. At every entry, the kernel verifies that all followers are present, the assigned value is absent from their values, and every smaller natural occurs. Induction on cell count equates the table with the recursive Grundy function. A second table establishes the rectangle premise. Only printed Conjecture 2 is refuted; no priority or corrected formula is asserted.

References

• Truth anchor: D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.IsPartition
• Truth anchor: D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.Position
• Truth anchor: D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.claim
• Truth anchor: D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.columnMoves
• Truth anchor: D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.deleteColumns
• Truth anchor: D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.grundy
• Truth anchor: D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.heavy
• Truth anchor: D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.moves
• Truth anchor: D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.rectangle
• Truth anchor: D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.result
• Truth anchor: D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.rowMoves
• Truth anchor: D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.staircase
• Truth anchor: D5/S0/Certificates/Games/PnimHeavyIntervalRefutation.youngLE
• Dependency: D5/S0/Certificates/Games/CrimGrundyRefutation