TransferTuples

Abstract

Degree enumeration for labelled circular run-constrained words.

Definition 1.1 (geom).

$$\forall (z:\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z})),\mathrm{geom}z=(\mathrm{PowerSeries}.\mathrm{invOfUnit}(1-z)1)$$

Formalization. D5/S1/Words/AssociatedMersenne/TransferTuples.geom (✓ 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 inverse of one minus a positive-order series supplies its formal geometric series.

Definition 1.2 (Rser).

$$\mathrm{Rser}=((\mathrm{PowerSeries}.X:\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z}){)}^3\cdot (\mathrm{PowerSeries}.C(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}):\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z}))+(\mathrm{PowerSeries}.X:\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z}){)}^5\cdot (\mathrm{PowerSeries}.C(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}):\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z}){)}^2\cdot \mathrm{geom}((\mathrm{PowerSeries}.X:\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z}){)}^2))$$

Formalization. D5/S1/Words/AssociatedMersenne/TransferTuples.Rser (✓ 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 run series separates a singleton one-run weight from the geometric tail of longer runs.

Definition 1.3 (Qser).

$$\mathrm{Qser}=((\mathrm{PowerSeries}.X:\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z}))\cdot \mathrm{geom}((\mathrm{PowerSeries}.C(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}):\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z}))\cdot (\mathrm{PowerSeries}.X:\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z}))))$$

Formalization. D5/S1/Words/AssociatedMersenne/TransferTuples.Qser (✓ 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 slack series records a compulsory position followed by an arbitrary weighted slack tail.

Definition 1.4 (A).

$$\begin{array}{r}A00=\mathrm{Rser}\\ A01=\mathrm{Rser}\cdot \mathrm{Qser}\\ A10=\mathrm{Rser}\\ A11=\mathrm{Rser}\cdot (\mathrm{PowerSeries}.C(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}))\cdot \mathrm{Qser}\end{array}$$

Formalization. D5/S1/Words/AssociatedMersenne/TransferTuples.A (✓ 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 two slack states determine the transfer entries from run and gap weight factors.

Lemma 1.5 (det A).

$$\mathrm{Matrix}.\det (1-A)=1-\mathrm{Rser}-\mathrm{Rser}\cdot (\mathrm{PowerSeries}.C(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}):\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z}))\cdot \mathrm{Qser}+{\mathrm{Rser}}^2\cdot ((\mathrm{PowerSeries}.C(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}):\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z}))-1)\cdot \mathrm{Qser}$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/TransferTuples.det_A (✓ 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.

Expanding the two-by-two determinant expresses the transfer denominator in run and slack series.

Lemma 1.6 (geom X2).

$$(1-(\mathrm{PowerSeries}.X:\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z}){)}^2)\cdot \mathrm{geom}((\mathrm{PowerSeries}.X:\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z}){)}^2)=1$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/TransferTuples.geom_X2 (✓ 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.

Multiplication by one minus the square of the length variable cancels its geometric series.

Lemma 1.7 (geom YX).

$$(1-(\mathrm{PowerSeries}.C(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}):\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z}))\cdot (\mathrm{PowerSeries}.X:\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z})))\cdot \mathrm{geom}((\mathrm{PowerSeries}.C(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}):\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z}))\cdot (\mathrm{PowerSeries}.X:\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z})))=1$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/TransferTuples.geom_YX (✓ 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.

Multiplication by one minus the joint length-and-degree variable cancels its geometric series.

Definition 1.8 (AgreeUpTo).

$$\forall (N:\mathrm{Nat}),\forall (f:(\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z}))),\forall (g:(\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z}))),\mathrm{AgreeUpTo}Nfg⟺(\forall n,n\le N\to \mathrm{PowerSeries}.\mathrm{coeff}nf=\mathrm{PowerSeries}.\mathrm{coeff}ng)$$

Formalization. D5/S1/Words/AssociatedMersenne/TransferTuples.AgreeUpTo (✓ 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.

Agreement of coefficients through a bound records the finite precision needed for enumeration.

Theorem 1.9 (geom monomial approx).

$$\forall (m:\mathrm{Nat}),\forall (d:\mathrm{Nat}),\forall (N:\mathrm{Nat}),(0<m)\to (\mathrm{AgreeUpTo}N(\mathrm{geom}(\mathrm{PowerSeries}.\mathrm{monomial}m((\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^d)))(\sum j\in \mathrm{Finset}.\mathrm{range}(N+1),(\mathrm{PowerSeries}.\mathrm{monomial}m((\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^d){)}^j))$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/TransferTuples.geom_monomial_approx (✓ 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 finite geometric-sum identity and the positive monomial order remove all omitted low-degree coefficients.

Definition 1.10 (slackState).

$$\forall (s:\mathrm{Nat}),\mathrm{slackState}s=(\mathrm{if}s=0\mathrm{then}0\mathrm{else}1)$$

Formalization. D5/S1/Words/AssociatedMersenne/TransferTuples.slackState (✓ 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.

Zero slack selects one transfer state and positive slack selects the other.

Definition 1.11 (pairLocal).

$$\forall (b:\mathrm{Nat}\times \mathrm{Nat}),\mathrm{pairLocal}b=(\min b.12+(b.2-1))$$

Formalization. D5/S1/Words/AssociatedMersenne/TransferTuples.pairLocal (✓ 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 local weight counts run deletion endpoints and the interior contribution from one gap.

Definition 1.12 (adjacency).

$$\forall (i:\mathrm{Fin}2),\forall (j:\mathrm{Fin}2),\mathrm{adjacency}ij=(\mathrm{if}i=1\wedge j=1\mathrm{then}1\mathrm{else}0)$$

Formalization. D5/S1/Words/AssociatedMersenne/TransferTuples.adjacency (✓ 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 transition contributes one insertion exactly when both consecutive slack states are positive.

Definition 1.13 (openDegree).

$$\begin{array}{r}\forall (j:\mathrm{Fin}2),\mathrm{openDegree}j[]=0\\ \forall (j:\mathrm{Fin}2),\forall (b:\mathrm{Nat}\times \mathrm{Nat}),\mathrm{openDegree}j[b]=\mathrm{pairLocal}b+\mathrm{adjacency}(\mathrm{slackState}b.2)j\\ \forall (j:\mathrm{Fin}2),\forall (bc:\mathrm{Nat}\times \mathrm{Nat})(t:\mathrm{List}(\mathrm{Nat}\times \mathrm{Nat})),\mathrm{openDegree}j(b::c::t)=\mathrm{pairLocal}b+\mathrm{adjacency}(\mathrm{slackState}b.2)(\mathrm{slackState}c.2)+\mathrm{openDegree}j(c::t)\end{array}$$

Formalization. D5/S1/Words/AssociatedMersenne/TransferTuples.openDegree (✓ 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.

Accumulating pair-local weights and state transitions gives the weight of an open tuple path.

Definition 1.14 (provisionalDegree).

$$\begin{array}{r}\mathrm{provisionalDegree}[]=0\\ \forall (b:\mathrm{Nat}\times \mathrm{Nat})(u:\mathrm{List}(\mathrm{Nat}\times \mathrm{Nat})),\mathrm{provisionalDegree}(b::u)=\mathrm{openDegree}(\mathrm{slackState}b.2)(b::u)\end{array}$$

Formalization. D5/S1/Words/AssociatedMersenne/TransferTuples.provisionalDegree (✓ 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.

Closing the tuple path adds the final transition back to the initial slack state.

Theorem 1.15 (trace coefficient tuples).

$$\forall (n:\mathrm{Nat}),\forall (\mathrm{ell}:\mathrm{Nat}),\mathrm{PowerSeries}.\mathrm{coeff}n(\mathrm{Matrix}.\mathrm{trace}(A^{(\mathrm{ell}+1)}))=\sum t:\mathrm{RunTuples}n(\mathrm{ell}+1),(\mathrm{Polynomial}.X:(\mathrm{Polynomial}\mathbb{Z}){)}^{\mathrm{provisionalDegree}t.\mathrm{val}.\mathrm{val}}$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/TransferTuples.trace_coefficient_tuples (✓ 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 matrix trace enumerates ordered tuples at each finite length, with provisionalDegree. No rotations of the word are identified.

Theorem 1.16 (tuple transfer coefficient).

$$\forall (n:\mathrm{Nat}),\forall (\mathrm{ell}:\mathrm{Nat}),\mathrm{tuplePolynomial}n(\mathrm{ell}+1)=\mathrm{PowerSeries}.\mathrm{coeff}n(\mathrm{Matrix}.\mathrm{trace}(A^{(\mathrm{ell}+1)}))+\mathrm{if}\mathrm{ell}=0\mathrm{then}\mathrm{PowerSeries}.\mathrm{coeff}n((\mathrm{PowerSeries}.X:\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z}))\cdot (1-(\mathrm{PowerSeries}.C(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}):\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z})))\cdot \mathrm{Rser})\mathrm{else}0$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/TransferTuples.tuple_transfer_coefficient (✓ 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 correction PowerSeries.X * (1 - PowerSeries.C Polynomial.X) * Rser removes the extra singleton insertion. For [(r,1)], provisionalDegree is min r 2 + 1 and tupleDegree is min r 2.

References

• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferTuples.A
• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferTuples.AgreeUpTo
• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferTuples.Qser
• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferTuples.Rser
• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferTuples.adjacency
• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferTuples.det_A
• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferTuples.geom
• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferTuples.geom_X2
• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferTuples.geom_YX
• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferTuples.geom_monomial_approx
• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferTuples.openDegree
• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferTuples.pairLocal
• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferTuples.provisionalDegree
• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferTuples.slackState
• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferTuples.trace_coefficient_tuples
• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferTuples.tuple_transfer_coefficient
• Dependency: D5/S1/Words/AssociatedMersenne/MarkedDegreeEnumeration