TransferResolvent

Abstract

Degree enumeration for labelled circular run-constrained words.

Definition 1.1 (dMatrix).

$$\forall (M:\mathrm{Matrix}(\mathrm{Fin}2)(\mathrm{Fin}2)(\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z}))),\mathrm{dMatrix}M=(\mathrm{fun}ij\mapsto (\mathrm{PowerSeries}.\mathrm{derivative}(\mathrm{Polynomial}\mathbb{Z}))(Mij))$$

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

Applying the power-series derivative to each matrix entry differentiates the transfer matrix.

Definition 1.2 (matrixGeom).

$$\forall (ij:\mathrm{Fin}2),\mathrm{matrixGeom}ij=\mathrm{PowerSeries}.\mathrm{mk}(\mathrm{fun}n\mapsto \sum k\in \mathrm{Finset}.\mathrm{range}(n+1),\mathrm{PowerSeries}.\mathrm{coeff}n((A^k)ij))$$

Formalization. D5/S1/Words/AssociatedMersenne/TransferResolvent.matrixGeom (✓ 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 coefficient uses only powers k≤n, because A is divisible by PowerSeries.X³. All displayed sums are finite.

Theorem 1.3 (matrixGeom inverse).

$$(1-A)\cdot \mathrm{matrixGeom}=1$$

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

At each coefficient only finitely many powers contribute, and the finite geometric-sum identity gives the inverse.

Definition 1.4 (transferDet).

$$\mathrm{transferDet}=(\mathrm{Matrix}.\det (1-A))$$

Formalization. D5/S1/Words/AssociatedMersenne/TransferResolvent.transferDet (✓ 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 determinant of one minus the transfer matrix supplies the cleared transfer denominator.

Definition 1.5 (transferTrace).

$$\mathrm{transferTrace}=(\mathrm{Matrix}.\mathrm{trace}(\mathrm{matrixGeom}\cdot \mathrm{dMatrix}A))$$

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

Tracing the matrix resolvent times the differentiated transfer matrix records marked cyclic paths.

Theorem 1.6 (transfer trace cleared).

$$\mathrm{transferDet}\cdot \mathrm{transferTrace}=-(\mathrm{PowerSeries}.\mathrm{derivative}(\mathrm{Polynomial}\mathbb{Z}))\mathrm{transferDet}$$

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

Multiplying the resolvent by its determinant gives the adjugate and hence the negative determinant derivative.

Lemma 1.7 (coeff euler).

$$\forall (f:(\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z}))),\forall (n:\mathrm{Nat}),\mathrm{PowerSeries}.\mathrm{coeff}n((\mathrm{PowerSeries}.X:\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z}))\cdot (\mathrm{PowerSeries}.\mathrm{derivative}(\mathrm{Polynomial}\mathbb{Z}))f)=(n:(\mathrm{Polynomial}\mathbb{Z}))\cdot \mathrm{PowerSeries}.\mathrm{coeff}nf$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/TransferResolvent.coeff_euler (✓ 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 the length variable after differentiation multiplies the nth coefficient by n.

Theorem 1.8 (trace marked coefficient).

$$\forall (\mathrm{ell}:\mathrm{Nat}),\forall (n:\mathrm{Nat}),((\mathrm{ell}+1:(\mathrm{Polynomial}\mathbb{Z}))\cdot \mathrm{PowerSeries}.\mathrm{coeff}n((\mathrm{PowerSeries}.X:\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z}))\cdot \mathrm{Matrix}.\mathrm{trace}(A^{\mathrm{ell}}\cdot \mathrm{dMatrix}A)))=(n:(\mathrm{Polynomial}\mathbb{Z}))\cdot \mathrm{PowerSeries}.\mathrm{coeff}n(\mathrm{Matrix}.\mathrm{trace}(A^{(\mathrm{ell}+1)}))$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/TransferResolvent.trace_marked_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.

Cyclic invariance of trace equates a marked matrix-power coefficient with its length-weighted derivative.

Theorem 1.9 (coeff euler transferTrace).

$$\forall (n:\mathrm{Nat}),\mathrm{PowerSeries}.\mathrm{coeff}n((\mathrm{PowerSeries}.X:\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z}))\cdot \mathrm{transferTrace})=\sum \mathrm{ell}\in \mathrm{Finset}.\mathrm{range}(n+1),\mathrm{PowerSeries}.\mathrm{coeff}n((\mathrm{PowerSeries}.X:\mathrm{PowerSeries}(\mathrm{Polynomial}\mathbb{Z}))\cdot \mathrm{Matrix}.\mathrm{trace}(A^{\mathrm{ell}}\cdot \mathrm{dMatrix}A))$$

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

Finite coefficient truncation expresses the marked resolvent trace as the sum of the length-weighted cyclic traces.

References

• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferResolvent.coeff_euler
• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferResolvent.coeff_euler_transferTrace
• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferResolvent.dMatrix
• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferResolvent.matrixGeom
• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferResolvent.matrixGeom_inverse
• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferResolvent.trace_marked_coefficient
• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferResolvent.transferDet
• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferResolvent.transferTrace
• Truth anchor: D5/S1/Words/AssociatedMersenne/TransferResolvent.transfer_trace_cleared
• Dependency: D5/S1/Words/AssociatedMersenne/TransferTuples