DegreeGeneratingFunction

Abstract

Degree enumeration for labelled circular run-constrained words.

Definition 1.1 (degSeries).

$$\mathrm{degSeries}=(\mathrm{PowerSeries}.\mathrm{mk}(\mathrm{fun}n\mapsto \sum k\in \mathrm{Finset}.\mathrm{range}(n+1),\mathrm{Polynomial}.C(Nnk:\mathbb{Z})\cdot \mathrm{Polynomial}.X^k))$$

Formalization. D5/S1/Words/AssociatedMersenne/DegreeGeneratingFunction.degSeries (✓ std3).

Source. Repository-derived.

Acknowledgement. J. Wei and Y. Yang (2024). Associated Mersenne graphs. DOI: 10.48550/arXiv.2407.08237. URL: https://arxiv.org/abs/2407.08237v1.

Commentary.

Each length coefficient is the polynomial histogram of admissible labelled words by degree.

Definition 1.2 (numCoeff).

$$\begin{array}{r}\forall (n:\mathrm{Nat}),(n=0)\to (\mathrm{numCoeff}n=1)\\ \forall (n:\mathrm{Nat}),(n=1)\to (\mathrm{numCoeff}n=1-(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}))\\ \forall (n:\mathrm{Nat}),(n=2)\to (\mathrm{numCoeff}n=-(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z})-3)\\ \forall (n:\mathrm{Nat}),(n=3)\to (\mathrm{numCoeff}n=(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^3+5\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z})-4)\\ \forall (n:\mathrm{Nat}),(n=4)\to (\mathrm{numCoeff}n=-3\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^2+7\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z})+2)\\ \forall (n:\mathrm{Nat}),(n=5)\to (\mathrm{numCoeff}n=(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^3-11\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z})+6)\\ \forall (n:\mathrm{Nat}),(n=6)\to (\mathrm{numCoeff}n=-5\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^3+17\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^2-18\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z})+2)\\ \forall (n:\mathrm{Nat}),(n=7)\to (\mathrm{numCoeff}n=7\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^4-22\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^3+7\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^2+14\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z})-4)\\ \forall (n:\mathrm{Nat}),(n=8)\to (\mathrm{numCoeff}n=-(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^4+15\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^3-32\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^2+22\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z})-3)\\ \forall (n:\mathrm{Nat}),(n=9)\to (\mathrm{numCoeff}n=-(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^5-24\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^4+57\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^3-22\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^2-11\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z})+1)\\ \forall (n:\mathrm{Nat}),(n=10)\to (\mathrm{numCoeff}n=-2\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^5+8\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^4-21\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^3+27\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^2-13\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z})+1)\\ \forall (n:\mathrm{Nat}),(n=11)\to (\mathrm{numCoeff}n=-2\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^6-2\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^5+43\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^4-71\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^3+27\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^2+5\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}))\\ \forall (n:\mathrm{Nat}),(n=12)\to (\mathrm{numCoeff}n=-(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^6+8\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^5-19\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^4+21\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^3-12\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^2+3\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}))\\ \forall (n:\mathrm{Nat}),(n=13)\to (\mathrm{numCoeff}n=-(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^7-7\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^6+39\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^5-72\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^4+59\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^3-17\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^2-(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}))\\ \forall (n:\mathrm{Nat}),(n=14)\to (\mathrm{numCoeff}n=2\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^6-10\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^5+18\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^4-14\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^3+4\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^2)\\ \forall (n:\mathrm{Nat}),(n=15)\to (\mathrm{numCoeff}n=-14\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^7+64\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^6-114\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^5+98\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^4-40\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^3+6\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^2)\\ \forall (n:\mathrm{Nat}),(n=16)\to (\mathrm{numCoeff}n=-(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^6+4\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^5-6\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^4+4\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^3-(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^2)\\ \forall (n:\mathrm{Nat}),(n=17)\to (\mathrm{numCoeff}n=-6\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^8+39\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^7-97\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^6+118\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^5-72\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^4+19\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^3-(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^2)\\ \forall (n:\mathrm{Nat}),(n=19)\to (\mathrm{numCoeff}n=4\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^8-20\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^7+40\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^6-40\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^5+20\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^4-4\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^3)\\ \forall (n:\mathrm{Nat}),(\neg (n\in [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,19]))\to (\mathrm{numCoeff}n=0)\end{array}$$

Formalization. D5/S1/Words/AssociatedMersenne/DegreeGeneratingFunction.numCoeff (✓ std3).

Source. Repository-derived.

Acknowledgement. J. Wei and Y. Yang (2024). Associated Mersenne graphs. DOI: 10.48550/arXiv.2407.08237. URL: https://arxiv.org/abs/2407.08237v1.

Commentary.

The explicit finite polynomial coefficients specify the numerator in the length variable.

Definition 1.3 (denCoeff).

$$\begin{array}{r}\forall (n:\mathrm{Nat}),(n=0)\to (\mathrm{denCoeff}n=1)\\ \forall (n:\mathrm{Nat}),(n=1)\to (\mathrm{denCoeff}n=-(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}))\\ \forall (n:\mathrm{Nat}),(n=2)\to (\mathrm{denCoeff}n=-4)\\ \forall (n:\mathrm{Nat}),(n=3)\to (\mathrm{denCoeff}n=3\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}))\\ \forall (n:\mathrm{Nat}),(n=4)\to (\mathrm{denCoeff}n=6)\\ \forall (n:\mathrm{Nat}),(n=5)\to (\mathrm{denCoeff}n=-(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^2-2\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}))\\ \forall (n:\mathrm{Nat}),(n=6)\to (\mathrm{denCoeff}n=-4)\\ \forall (n:\mathrm{Nat}),(n=7)\to (\mathrm{denCoeff}n=(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^3+2\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^2-2\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}))\\ \forall (n:\mathrm{Nat}),(n=8)\to (\mathrm{denCoeff}n=1)\\ \forall (n:\mathrm{Nat}),(n=9)\to (\mathrm{denCoeff}n=2\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^4-6\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^3+(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^2+3\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}))\\ \forall (n:\mathrm{Nat}),(n=11)\to (\mathrm{denCoeff}n=(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^5-7\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^4+12\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^3-5\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^2-(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}))\\ \forall (n:\mathrm{Nat}),(n=13)\to (\mathrm{denCoeff}n=-2\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^5+8\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^4-10\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^3+4\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^2)\\ \forall (n:\mathrm{Nat}),(n=15)\to (\mathrm{denCoeff}n=(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^5-3\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^4+3\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^3-(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^2)\\ \forall (n:\mathrm{Nat}),(\neg (n\in [0,1,2,3,4,5,6,7,8,9,11,13,15]))\to (\mathrm{denCoeff}n=0)\end{array}$$

Formalization. D5/S1/Words/AssociatedMersenne/DegreeGeneratingFunction.denCoeff (✓ std3).

Source. Repository-derived.

Acknowledgement. J. Wei and Y. Yang (2024). Associated Mersenne graphs. DOI: 10.48550/arXiv.2407.08237. URL: https://arxiv.org/abs/2407.08237v1.

Commentary.

The explicit finite polynomial coefficients specify the denominator with constant coefficient one.

Definition 1.4 (NUM).

$$\mathrm{NUM}=(\mathrm{PowerSeries}.\mathrm{mk}\mathrm{numCoeff})$$

Formalization. D5/S1/Words/AssociatedMersenne/DegreeGeneratingFunction.NUM (✓ std3).

Source. Repository-derived.

Acknowledgement. J. Wei and Y. Yang (2024). Associated Mersenne graphs. DOI: 10.48550/arXiv.2407.08237. URL: https://arxiv.org/abs/2407.08237v1.

Commentary.

The numerator coefficient list defines a power series with finite support in the length variable.

Definition 1.5 (DEN).

$$\mathrm{DEN}=(\mathrm{PowerSeries}.\mathrm{mk}\mathrm{denCoeff})$$

Formalization. D5/S1/Words/AssociatedMersenne/DegreeGeneratingFunction.DEN (✓ std3).

Source. Repository-derived.

Acknowledgement. J. Wei and Y. Yang (2024). Associated Mersenne graphs. DOI: 10.48550/arXiv.2407.08237. URL: https://arxiv.org/abs/2407.08237v1.

Commentary.

The denominator coefficient list defines a power series with finite support in the length variable.

Definition 1.6 (claim).

$$\mathrm{claim}⟺(\mathrm{degSeries}\cdot \mathrm{DEN}=\mathrm{NUM})$$

Formalization. D5/S1/Words/AssociatedMersenne/DegreeGeneratingFunction.claim (✓ std3).

Source. Repository-derived.

Acknowledgement. J. Wei and Y. Yang (2024). Associated Mersenne graphs. DOI: 10.48550/arXiv.2407.08237. URL: https://arxiv.org/abs/2407.08237v1.

Commentary.

Wei and Yang, Question 6.2, arXiv v1, p. 18: “For given n and k, how many vertices of Associated Mersenne graph ℳₙ have degree k?” N n k counts labelled admissible Boolean words, without identifying rotations. The PowerSeries index is length and Polynomial.X records degree. The displayed formula clears the explicit denominator.

Theorem 1.7 (result).

$$\mathrm{claim}$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/DegreeGeneratingFunction.result (✓ std3). ∎

Resolves. Problems/wei-yang-2024-associated-mersenne-degree-series (proved) by D5/S1/Words/AssociatedMersenne/DegreeGeneratingFunction.result.

Source. Repository-derived.

Acknowledgement. J. Wei and Y. Yang (2024). Associated Mersenne graphs. DOI: 10.48550/arXiv.2407.08237. URL: https://arxiv.org/abs/2407.08237v1.

Commentary.

The marked tuple bijection and pair-local flip classification give the degree statistic. The marked double count and finite transfer resolvent, with the exact singleton correction, yield the displayed denominator-cleared degree generating function for every length.

References

• Truth anchor: D5/S1/Words/AssociatedMersenne/DegreeGeneratingFunction.DEN
• Truth anchor: D5/S1/Words/AssociatedMersenne/DegreeGeneratingFunction.NUM
• Truth anchor: D5/S1/Words/AssociatedMersenne/DegreeGeneratingFunction.claim
• Truth anchor: D5/S1/Words/AssociatedMersenne/DegreeGeneratingFunction.degSeries
• Truth anchor: D5/S1/Words/AssociatedMersenne/DegreeGeneratingFunction.denCoeff
• Truth anchor: D5/S1/Words/AssociatedMersenne/DegreeGeneratingFunction.numCoeff
• Truth anchor: D5/S1/Words/AssociatedMersenne/DegreeGeneratingFunction.result
• Dependency: D5/S1/Words/AssociatedMersenne/TransferResolvent