MarkedDegreeEnumeration

Abstract

Degree enumeration for labelled circular run-constrained words.

Definition 1.1 (DegreeTuples).

$$\forall (n:\mathrm{Nat}),\forall (\mathrm{ell}:\mathrm{Nat}),\forall (k:\mathrm{Nat}),\mathrm{DegreeTuples}n\mathrm{ell}k=(\{t:\mathrm{GoodTuple}n//t.\mathrm{val}.\mathrm{length}=\mathrm{ell}\wedge \mathrm{tupleDegree}t.\mathrm{val}=k\})$$

Formalization. D5/S1/Words/AssociatedMersenne/MarkedDegreeEnumeration.DegreeTuples (✓ 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 subtype fixes the number of tuple pairs and their exact tuple degree.

Definition 1.2 (instFintypeDegreeTuples).

$$\forall (n:\mathrm{Nat}),\forall (\mathrm{ell}:\mathrm{Nat}),\forall (k:\mathrm{Nat}),\mathrm{instFintypeDegreeTuples}n\mathrm{ell}k:\mathrm{Fintype}(\mathrm{DegreeTuples}n\mathrm{ell}k)$$

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

This instance is inferInstanceAs for the subtype of RunTuples n ell whose tupleDegree equals k.

Theorem 1.3 (marked degree double count).

$$\forall (n:\mathrm{Nat}),\forall (\mathrm{ell}:\mathrm{Nat}),\forall (k:\mathrm{Nat}),\mathrm{ell}\cdot \mathrm{Fintype}.\mathrm{card}(\mathrm{DegreeRunWords}n\mathrm{ell}k)=n\cdot \mathrm{Fintype}.\mathrm{card}(\mathrm{DegreeTuples}n\mathrm{ell}k)$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/MarkedDegreeEnumeration.marked_degree_double_count (✓ 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 marked word-to-tuple equivalence preserves degree and converts run marks into labelled origins.

Definition 1.4 (degreePolynomial).

$$\forall (n:\mathrm{Nat}),\mathrm{degreePolynomial}n=(\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/MarkedDegreeEnumeration.degreePolynomial (✓ 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.

Summing the histogram with monomials in the degree records all labelled admissible words.

Definition 1.5 (instFintypeRunTuples).

$$\forall (n:\mathrm{Nat}),\forall (\mathrm{ell}:\mathrm{Nat}),\mathrm{instFintypeRunTuples}n\mathrm{ell}:\mathrm{Fintype}(\mathrm{RunTuples}n\mathrm{ell})$$

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

This instance is inferInstanceAs for the subtype of GoodTuple n whose underlying list has length ell.

Lemma 1.6 (runCount le).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\mathrm{runCount}w\le n$$

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

Marked starts form a subset of the labelled positions, bounding the number of runs by the length.

Definition 1.7 (runPolynomial).

$$\forall (n:\mathrm{Nat}),\forall (\mathrm{ell}:\mathrm{Nat}),\mathrm{runPolynomial}n\mathrm{ell}=(\sum k\in \mathrm{Finset}.\mathrm{range}(n+1),\mathrm{Polynomial}.C((\mathrm{Fintype}.\mathrm{card}(\mathrm{DegreeRunWords}n\mathrm{ell}k)):\mathbb{Z})\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^k)$$

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

Filtering additionally by the number of circular runs gives the degree-refined run polynomial.

Definition 1.8 (tuplePolynomial).

$$\forall (n:\mathrm{Nat}),\forall (\mathrm{ell}:\mathrm{Nat}),\mathrm{tuplePolynomial}n\mathrm{ell}=(\sum k\in \mathrm{Finset}.\mathrm{range}(n+1),\mathrm{Polynomial}.C((\mathrm{Fintype}.\mathrm{card}(\mathrm{DegreeTuples}n\mathrm{ell}k)):\mathbb{Z})\cdot (\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^k)$$

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

Counting positive tuples by their tuple degree gives the corresponding run-refined weight polynomial.

Theorem 1.9 (polynomial marked double count).

$$\forall (n:\mathrm{Nat}),\forall (\mathrm{ell}:\mathrm{Nat}),(\mathrm{ell}:(\mathrm{Polynomial}\mathbb{Z}))\cdot \mathrm{runPolynomial}n\mathrm{ell}=(n:(\mathrm{Polynomial}\mathbb{Z}))\cdot \mathrm{tuplePolynomial}n\mathrm{ell}$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/MarkedDegreeEnumeration.polynomial_marked_double_count (✓ 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 marked count to each degree coefficient gives the integer polynomial double-count identity.

Theorem 1.10 (tuplePolynomial eq sum).

$$\forall (n:\mathrm{Nat}),\forall (\mathrm{ell}:\mathrm{Nat}),\mathrm{tuplePolynomial}n\mathrm{ell}=\sum t:\mathrm{RunTuples}n\mathrm{ell},(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^{\mathrm{tupleDegree}t.\mathrm{val}.\mathrm{val}}$$

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

Partitioning the finite tuple set by degree turns the histogram polynomial into a sum of tuple weights.

Lemma 1.11 (degreePolynomial partition).

$$\forall (n:\mathrm{Nat}),\mathrm{degreePolynomial}n=\sum \mathrm{ell}\in \mathrm{Finset}.\mathrm{range}(n+1),\mathrm{runPolynomial}n\mathrm{ell}$$

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

Partitioning admissible words by their run count recovers the full degree polynomial.

Lemma 1.12 (runPolynomial zero).

$$\forall (n:\mathrm{Nat}),\mathrm{runPolynomial}n0=(\mathrm{Polynomial}.X:\mathrm{Polynomial}\mathbb{Z}{)}^{(\mathrm{if}n\le 2\mathrm{then}0\mathrm{else}n)}$$

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

A zero-run admissible word is the zero word, whose degree fixes its single polynomial weight.

References

• Truth anchor: D5/S1/Words/AssociatedMersenne/MarkedDegreeEnumeration.DegreeTuples
• Truth anchor: D5/S1/Words/AssociatedMersenne/MarkedDegreeEnumeration.degreePolynomial
• Truth anchor: D5/S1/Words/AssociatedMersenne/MarkedDegreeEnumeration.degreePolynomial_partition
• Truth anchor: D5/S1/Words/AssociatedMersenne/MarkedDegreeEnumeration.instFintypeDegreeTuples
• Truth anchor: D5/S1/Words/AssociatedMersenne/MarkedDegreeEnumeration.instFintypeRunTuples
• Truth anchor: D5/S1/Words/AssociatedMersenne/MarkedDegreeEnumeration.marked_degree_double_count
• Truth anchor: D5/S1/Words/AssociatedMersenne/MarkedDegreeEnumeration.polynomial_marked_double_count
• Truth anchor: D5/S1/Words/AssociatedMersenne/MarkedDegreeEnumeration.runCount_le
• Truth anchor: D5/S1/Words/AssociatedMersenne/MarkedDegreeEnumeration.runPolynomial
• Truth anchor: D5/S1/Words/AssociatedMersenne/MarkedDegreeEnumeration.runPolynomial_zero
• Truth anchor: D5/S1/Words/AssociatedMersenne/MarkedDegreeEnumeration.tuplePolynomial
• Truth anchor: D5/S1/Words/AssociatedMersenne/MarkedDegreeEnumeration.tuplePolynomial_eq_sum
• Dependency: D5/S1/Words/AssociatedMersenne/MultiRunDegrees