MultiRunDegrees

Abstract

Degree enumeration for labelled circular run-constrained words.

Theorem 1.1 (degree raw multi).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\forall (i:\mathrm{Fin}n),\forall (t:\mathrm{List}(\mathrm{Nat}\times \mathrm{Nat})),(2\le t.\mathrm{length})\to ((\forall b\in t,0<b.1\wedge b.1<b.2)\to ((\mathrm{linearize}wi=\mathrm{rawWord}t)\to (\mathrm{degree}w=\sum p:\mathrm{Fin}t.\mathrm{length},(\min t[p.\mathrm{val}].12+(t[p.\mathrm{val}].2-(t[p.\mathrm{val}].1+1)-1)+\mathrm{if}t[p.\mathrm{val}].1+1<t[p.\mathrm{val}].2\wedge (t[(p.\mathrm{val}+1)\mathrm{Nat}.\mathrm{mod}t.\mathrm{length}]).1+1<(t[(p.\mathrm{val}+1)\mathrm{Nat}.\mathrm{mod}t.\mathrm{length}]).2\mathrm{then}1\mathrm{else}0))))$$

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

Pairwise deletion endpoints, gap extensions and interior singleton insertions partition all legal flips.

Definition 1.2 (tupleDegree).

$$\forall (t:\mathrm{List}(\mathrm{Nat}\times \mathrm{Nat})),\mathrm{tupleDegree}t=(\mathrm{if}t.\mathrm{length}=1\mathrm{then}(t.\mathrm{map}(\mathrm{fun}b\mapsto \min b.12+\mathrm{if}2\le b.2\mathrm{then}b.2\mathrm{else}0)).\mathrm{sum}\mathrm{else}\sum p:\mathrm{Fin}t.\mathrm{length},(\min t[p.\mathrm{val}].12+(t[p.\mathrm{val}].2-1)+\mathrm{if}1\le t[p.\mathrm{val}].2\wedge 1\le (t[(p.\mathrm{val}+1)\mathrm{Nat}.\mathrm{mod}t.\mathrm{length}]).2\mathrm{then}1\mathrm{else}0))$$

Formalization. D5/S1/Words/AssociatedMersenne/MultiRunDegrees.tupleDegree (✓ 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 singleton case includes both circular gap endpoints meeting the same run. Natural subtraction is truncated; it is not integer subtraction.

Lemma 1.3 (degree wordOfTuple).

$$\forall (n:\mathrm{Nat}),\forall (i:\mathrm{Fin}n),\forall (t:\mathrm{GoodTuple}n),\mathrm{degree}(\mathrm{wordOfTuple}it.\mathrm{val}t.\mathrm{property}.2.2)=\mathrm{tupleDegree}t.\mathrm{val}$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/MultiRunDegrees.degree_wordOfTuple (✓ 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 reconstructed word has its tuple encoding, so the pair-local formula gives its degree.

References

• Truth anchor: D5/S1/Words/AssociatedMersenne/MultiRunDegrees.degree_raw_multi
• Truth anchor: D5/S1/Words/AssociatedMersenne/MultiRunDegrees.degree_wordOfTuple
• Truth anchor: D5/S1/Words/AssociatedMersenne/MultiRunDegrees.tupleDegree
• Dependency: D5/S1/Words/AssociatedMersenne/SingleRunDegrees