A family with equal third and unequal second principal specializations

Abstract

For every positive j, the source caterpillars (5,j,j,4,3) and (4,j,j,5,3) have different second and identical third ordinary chromatic symmetric principal specializations.

Definition 1.1 (Positive parts).

$$\forall (l:\mathbb{N}),\mathrm{Parts}\left(l\right)=(\mathrm{Fin}\left(l\right)\to {\mathbb{N}}^{+})$$

Formalization. D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.Parts (✓ std3).

Source. Repository-derived.

Acknowledgement. Aram Bingham, Kyle Celano, Patricia Commins, Rosa Orellana, Jianping Pan, and Mary Claire Simone (2026). Principal specializations of the t-chromatic symmetric function. DOI: 10.48550/arXiv.2610.31785. URL: https://arxiv.org/abs/2610.31785v1.

Commentary.

A length-l composition is represented by a function from Fin l to the positive naturals. Fin l uses indices 0 through l−1. The source uses indices 1 through l; adding one identifies the spine indices.

Definition 1.2 (The source vertex carrier).

$$\forall (l:\mathbb{N}),\forall (a:\mathrm{Parts}\left(l\right)),\mathrm{Vertex}\left(a\right)={\Sigma }_{i:\mathrm{Fin}\left(l\right)}\mathrm{Fin}\left(PNat.val\left(a\left(i\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.Vertex (✓ std3).

Source. Repository-derived.

Acknowledgement. Aram Bingham, Kyle Celano, Patricia Commins, Rosa Orellana, Jianping Pan, and Mary Claire Simone (2026). Principal specializations of the t-chromatic symmetric function. DOI: 10.48550/arXiv.2610.31785. URL: https://arxiv.org/abs/2610.31785v1.

Commentary.

The dependent pair (i,0) represents the source spine vertex v_(i+1). The pair (i,r), for 1 ≤ r < val(a(i)), represents its leaf w_(i+1,r). Thus the ith block has exactly val(a(i)) vertices. A part equal to one has no leaves.

Definition 1.3 (The oriented source edge list).

$$\forall (l:\mathbb{N}),\forall (a:\mathrm{Parts}\left(l\right)),\forall (u:\mathrm{Vertex}\left(a\right)),\forall (v:\mathrm{Vertex}\left(a\right)),\mathrm{edgeRel}\left(a,u,v\right)\iff \left(((u_1=v_1)\wedge ((Fin.val\left(u_2\right)=0)\wedge (Fin.val\left(v_2\right)\ne 0)))\vee ((Fin.val\left(u_2\right)=0)\wedge ((Fin.val\left(v_2\right)=0)\wedge (Fin.val\left(u_1\right)+1=Fin.val\left(v_1\right))))\right)$$

Formalization. D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.edgeRel (✓ std3).

Source. Repository-derived.

Acknowledgement. Aram Bingham, Kyle Celano, Patricia Commins, Rosa Orellana, Jianping Pan, and Mary Claire Simone (2026). Principal specializations of the t-chromatic symmetric function. DOI: 10.48550/arXiv.2610.31785. URL: https://arxiv.org/abs/2610.31785v1.

Commentary.

Subscripts 1 and 2 denote the two projections of a vertex. The first disjunct lists spine-to-leaf edges inside a block; the second lists forward consecutive spine edges. The val maps are the natural-number projections of Fin elements.

Definition 1.4 (The caterpillar).

$$\forall (l:\mathbb{N}),\forall (a:\mathrm{Parts}\left(l\right)),\mathrm{caterpillar}\left(a\right)=SimpleGraph.fromRel\left(\mathrm{edgeRel}\left(a\right)\right)$$

Formalization. D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.caterpillar (✓ std3).

Citation. Aram Bingham, Kyle Celano, Patricia Commins, Rosa Orellana, Jianping Pan, and Mary Claire Simone (2026). Principal specializations of the t-chromatic symmetric function. DOI: 10.48550/arXiv.2610.31785. URL: https://arxiv.org/abs/2610.31785v1.

Commentary.

Mathlib SimpleGraph.fromRel symmetrizes the displayed relation and excludes loops. This is exactly Definition 2.1’s caterpillar whenever the source endpoint conditions hold. Both five-part families satisfy those conditions for every positive j. The definition is total on all positive part vectors.

Definition 1.5 (The ordinary principal specialization).

$$\forall (V:Type\ast ),[\mathrm{Fintype}\left(V\right)]\forall (G:\mathrm{SimpleGraph}\left(V\right)),\forall (k:\mathbb{N}),\mathrm{ps}\left(G,k\right)=\sum _{c:SimpleGraph.Coloring\left(G,\mathrm{Fin}\left(k\right)\right)}{Polynomial.X}^{{\sum }_{v:V}Fin.val\left(c\left(v\right)\right)}$$

Formalization. D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.ps (✓ std3).

Citation. Aram Bingham, Kyle Celano, Patricia Commins, Rosa Orellana, Jianping Pan, and Mary Claire Simone (2026). Principal specializations of the t-chromatic symmetric function. DOI: 10.48550/arXiv.2610.31785. URL: https://arxiv.org/abs/2610.31785v1.

Commentary.

Equation (2.1) of the source changes to colors 0 through k−1. SimpleGraph.Coloring means every edge has different endpoint colors; it imposes no surjectivity. Every proper coloring into Fin k occurs once in the finite sum. X is Polynomial.X over the integers. These polynomials embed injectively in the source’s complex coefficient ring, preserving equality and inequality. No t refinement is used.

Definition 1.6 (The first family).

$$\forall (j:{\mathbb{N}}^{+}),\mathrm{alpha}\left(j\right)=![5,j,j,4,3]$$

Formalization. D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.alpha (✓ std3).

Citation. Aram Bingham, Kyle Celano, Patricia Commins, Rosa Orellana, Jianping Pan, and Mary Claire Simone (2026). Principal specializations of the t-chromatic symmetric function. DOI: 10.48550/arXiv.2610.31785. URL: https://arxiv.org/abs/2610.31785v1.

Commentary.

The tuple denotes the Fin 5 indexed function with the displayed entries, all in the positive naturals.

Definition 1.7 (The second family).

$$\forall (j:{\mathbb{N}}^{+}),\mathrm{beta}\left(j\right)=![4,j,j,5,3]$$

Formalization. D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.beta (✓ std3).

Citation. Aram Bingham, Kyle Celano, Patricia Commins, Rosa Orellana, Jianping Pan, and Mary Claire Simone (2026). Principal specializations of the t-chromatic symmetric function. DOI: 10.48550/arXiv.2610.31785. URL: https://arxiv.org/abs/2610.31785v1.

Commentary.

The repeated internal part is the same arbitrary positive natural j in both positions. The proof uses the fixed end blocks 5,4,3 in the stated algebraic identity.

Definition 1.8 (Proper spine colors).

$$\forall (l:\mathbb{N}),\forall (k:\mathbb{N}),\forall (c:(\mathrm{Fin}\left(l\right))\to (\mathrm{Fin}\left(k\right))),\mathrm{SpineGood}\left(c\right)\iff \forall (i:\mathrm{Fin}\left(l\right)),\forall (j:\mathrm{Fin}\left(l\right)),(Fin.val\left(i\right)+1=Fin.val\left(j\right))\Rightarrow (c\left(i\right)\ne c\left(j\right))$$

Formalization. D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.SpineGood (✓ std3).

Source. Repository-derived.

Acknowledgement. Aram Bingham, Kyle Celano, Patricia Commins, Rosa Orellana, Jianping Pan, and Mary Claire Simone (2026). Principal specializations of the t-chromatic symmetric function. DOI: 10.48550/arXiv.2610.31785. URL: https://arxiv.org/abs/2610.31785v1.

Commentary.

Consecutive spine vertices receive distinct colors.

Definition 1.9 (The choices at one leaf).

$$\forall (k:\mathbb{N}),\forall (c:\mathrm{Fin}\left(k\right)),\mathrm{leafSum}\left(c\right)=\sum _{d:\{d:\mathrm{Fin}\left(k\right)\mid d\ne c\}}{Polynomial.X}^{Fin.val\left(Subtype.val\left(d\right)\right)}$$

Formalization. D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.leafSum (✓ std3).

Source. Repository-derived.

Acknowledgement. Aram Bingham, Kyle Celano, Patricia Commins, Rosa Orellana, Jianping Pan, and Mary Claire Simone (2026). Principal specializations of the t-chromatic symmetric function. DOI: 10.48550/arXiv.2610.31785. URL: https://arxiv.org/abs/2610.31785v1.

Commentary.

The sum ranges over every color different from the incident spine color.

Definition 1.10 (The weight of one block).

$$\forall (k:\mathbb{N}),\forall (m:{\mathbb{N}}^{+}),\forall (c:\mathrm{Fin}\left(k\right)),\mathrm{blockWeight}\left(m,c\right)={Polynomial.X}^{Fin.val\left(c\right)}\cdot \mathrm{leafSum}{\left(c\right)}^{PNat.val\left(m\right)-1}$$

Formalization. D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.blockWeight (✓ std3).

Source. Repository-derived.

Acknowledgement. Aram Bingham, Kyle Celano, Patricia Commins, Rosa Orellana, Jianping Pan, and Mary Claire Simone (2026). Principal specializations of the t-chromatic symmetric function. DOI: 10.48550/arXiv.2610.31785. URL: https://arxiv.org/abs/2610.31785v1.

Commentary.

A positive part m gives one spine vertex and val(m) minus one leaves. The zeroth power accounts for an empty leaf set.

Theorem 1.11 (The complete finite spine sum).

$$\forall (l:\mathbb{N}),\forall (k:\mathbb{N}),\forall (a:\mathrm{Parts}\left(l\right)),\mathrm{ps}\left(\mathrm{caterpillar}\left(a\right),k\right)=\sum _{c:(\mathrm{Fin}\left(l\right))\to (\mathrm{Fin}\left(k\right))}\mathrm{if}\mathrm{SpineGood}\left(c\right)\mathrm{then}\prod _{i:\mathrm{Fin}\left(l\right)}\mathrm{blockWeight}\left(a\left(i\right),c\left(i\right)\right)\mathrm{else}0$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.ps_spine_sum (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Aram Bingham, Kyle Celano, Patricia Commins, Rosa Orellana, Jianping Pan, and Mary Claire Simone (2026). Principal specializations of the t-chromatic symmetric function. DOI: 10.48550/arXiv.2610.31785. URL: https://arxiv.org/abs/2610.31785v1.

Commentary.

The coloring bijection and independent leaf choices give this identity for every positive part vector and every number of colors.

Theorem 1.12 (Expanding a finite function sum).

$$\forall (A:Type\ast ),[\mathrm{Fintype}\left(A\right)]\forall (n:\mathbb{N}),\forall (f:((\mathrm{Fin}\left(n+1\right))\to (A))\to (\mathrm{Polynomial}\left(\mathbb{Z}\right))),\sum _{c:(\mathrm{Fin}\left(n+1\right))\to (A)}f\left(c\right)=\sum _{x:A}\sum _{c:(\mathrm{Fin}\left(n\right))\to (A)}f\left(Fin.cons\left(x,c\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.sum_finfun_succ (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Aram Bingham, Kyle Celano, Patricia Commins, Rosa Orellana, Jianping Pan, and Mary Claire Simone (2026). Principal specializations of the t-chromatic symmetric function. DOI: 10.48550/arXiv.2610.31785. URL: https://arxiv.org/abs/2610.31785v1.

Commentary.

The first value and the remaining function uniquely determine a function on Fin (n+1).

Theorem 1.13 (A leaf sum over the whole color set).

$$\forall (k:\mathbb{N}),\forall (c:\mathrm{Fin}\left(k\right)),\mathrm{leafSum}\left(c\right)=\sum _{d:\mathrm{Fin}\left(k\right)}\mathrm{if}(d\ne c)\mathrm{then}{Polynomial.X}^{Fin.val\left(d\right)}\mathrm{else}0$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.leafSum_eq (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Aram Bingham, Kyle Celano, Patricia Commins, Rosa Orellana, Jianping Pan, and Mary Claire Simone (2026). Principal specializations of the t-chromatic symmetric function. DOI: 10.48550/arXiv.2610.31785. URL: https://arxiv.org/abs/2610.31785v1.

Commentary.

The forbidden color contributes zero; every other color contributes its monomial.

Definition 1.14 (Remark 3.11, first question).

$$claim\iff (\forall (j:{\mathbb{N}}^{+}),(\mathrm{ps}\left(\mathrm{caterpillar}\left(\mathrm{alpha}\left(j\right)\right),2\right)\ne \mathrm{ps}\left(\mathrm{caterpillar}\left(\mathrm{beta}\left(j\right)\right),2\right))\wedge (\mathrm{ps}\left(\mathrm{caterpillar}\left(\mathrm{alpha}\left(j\right)\right),3\right)=\mathrm{ps}\left(\mathrm{caterpillar}\left(\mathrm{beta}\left(j\right)\right),3\right)))$$

Formalization. D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.claim (✓ std3).

Citation. Aram Bingham, Kyle Celano, Patricia Commins, Rosa Orellana, Jianping Pan, and Mary Claire Simone (2026). Principal specializations of the t-chromatic symmetric function. DOI: 10.48550/arXiv.2610.31785. URL: https://arxiv.org/abs/2610.31785v1.

Commentary.

The domain is all positive integers, including j=1. Equality is formal polynomial equality in Z[X], with an indeterminate X. The second question, whether these are the only such pairs, is outside this statement.

Theorem 1.15 (The entire positive-parameter family).

$$\forall (j:{\mathbb{N}}^{+}),(\mathrm{ps}\left(\mathrm{caterpillar}\left(\mathrm{alpha}\left(j\right)\right),2\right)\ne \mathrm{ps}\left(\mathrm{caterpillar}\left(\mathrm{beta}\left(j\right)\right),2\right))\wedge (\mathrm{ps}\left(\mathrm{caterpillar}\left(\mathrm{alpha}\left(j\right)\right),3\right)=\mathrm{ps}\left(\mathrm{caterpillar}\left(\mathrm{beta}\left(j\right)\right),3\right))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.result (✓ std3). ∎

Resolves. Problems/bingham-2026-caterpillar-principal-specialization-family (proved) by D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.result.

Source. Repository-derived.

Acknowledgement. Aram Bingham, Kyle Celano, Patricia Commins, Rosa Orellana, Jianping Pan, and Mary Claire Simone (2026). Principal specializations of the t-chromatic symmetric function. DOI: 10.48550/arXiv.2610.31785. URL: https://arxiv.org/abs/2610.31785v1.

Commentary.

Restricting a proper coloring to the spine and its leaves gives a bijection with proper spine colorings and independent leaf assignments. Weight is additive over the actual vertices. Summing the leaf choices gives, for spine color c and positive part a, the block weight X^c times (the sum of X^d over d different from c) raised to val(a)−1. Empty leaf sets contribute one. The five spine colors are then summed subject to consecutive inequality. For three colors, an identity with an arbitrary repeated three-entry middle weight vector interchanges the fixed 5 and 4 blocks while keeping the final 3 block. Polynomial normalization proves that identity before substituting the weights for j, so no finite cutoff on j or numerical evaluation of X occurs. For two colors, the two alternating spine choices give X^(val(j)+5)+X^(val(j)+7) for alpha and X^(val(j)+6)+X^(val(j)+6) for beta. Their coefficients at degree val(j)+5 are one and zero. The proof settles the first question only; classification, the t-chromatic invariant, and the source’s four-color conjectures remain outside its scope.

References

• Truth anchor: D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.Parts
• Truth anchor: D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.SpineGood
• Truth anchor: D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.Vertex
• Truth anchor: D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.alpha
• Truth anchor: D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.beta
• Truth anchor: D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.blockWeight
• Truth anchor: D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.caterpillar
• Truth anchor: D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.claim
• Truth anchor: D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.edgeRel
• Truth anchor: D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.leafSum
• Truth anchor: D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.leafSum_eq
• Truth anchor: D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.ps
• Truth anchor: D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.ps_spine_sum
• Truth anchor: D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.result
• Truth anchor: D5/S3/Combinatorics/Graph/PrincipalSpecialization/BinghamCaterpillarPs3Family.sum_finfun_succ