CircularWords

Abstract

Degree enumeration for labelled circular run-constrained words.

Lemma 1.1 (Split under reversal and transport).

$$\forall (\mathrm{alpha}:\mathrm{Type}),\forall (\mathrm{beta}:\mathrm{Type}),\forall (r:\mathrm{alpha}\to \mathrm{alpha}\to \mathrm{Bool}),\forall (s:\mathrm{beta}\to \mathrm{beta}\to \mathrm{Bool}),\forall (f:\mathrm{alpha}\to \mathrm{beta}),\forall (l:\mathrm{List}\mathrm{alpha}),(\forall a\in l,\forall b\in l,s(fb)(fa)=rab)\to ((l.\mathrm{reverse}.\mathrm{map}f).\mathrm{splitBy}s=(l.\mathrm{splitBy}r).\mathrm{reverse}.\mathrm{map}(\mathrm{fun}b\mapsto b.\mathrm{reverse}.\mathrm{map}f))$$

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

Reversing each block and the block order preserves internal links and separating boundaries under the transported relation.

Definition 1.2 (cycAdd).

$$\forall (n:\mathrm{Nat}),\forall (i:\mathrm{Fin}n),\forall (j:\mathrm{Nat}),\mathrm{cycAdd}ij=(\mathrm{Fin}.\mathrm{ofNat}n(i.\mathrm{val}+j))$$

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

Adding a natural offset and reducing modulo the length gives the labelled circular position.

Definition 1.3 (cycSub).

$$\forall (n:\mathrm{Nat}),\forall (i:\mathrm{Fin}n),\forall (j:\mathrm{Nat}),\mathrm{cycSub}ij=(\mathrm{Fin}.\mathrm{ofNat}n(i.\mathrm{val}+n-j))$$

Formalization. D5/S1/Words/AssociatedMersenne/CircularWords.cycSub (✓ 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 predecessor offset uses natural subtraction before reduction modulo the length.

Definition 1.4 (IsOneRunStart).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\forall (i:\mathrm{Fin}n),\forall (r:\mathrm{Nat}),\mathrm{IsOneRunStart}wir⟺(w(\mathrm{cycSub}i1)=\mathrm{false}\wedge (\forall j<r,w(\mathrm{cycAdd}ij)=\mathrm{true})\wedge w(\mathrm{cycAdd}ir)=\mathrm{false})$$

Formalization. D5/S1/Words/AssociatedMersenne/CircularWords.IsOneRunStart (✓ 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 preceding and following letters are zero and all r intermediate letters are one. This predicate permits r=0. Genuine marks use IsMarkedStart, which requires positive r.

Definition 1.5 (Admissible).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\mathrm{Admissible}w⟺((n=0\vee \exists i,wi=\mathrm{false})\wedge \forall ir,\mathrm{IsOneRunStart}wir\to \forall j\le r,w(\mathrm{cycAdd}(\mathrm{cycAdd}ir)j)=\mathrm{false})$$

Formalization. D5/S1/Words/AssociatedMersenne/CircularWords.Admissible (✓ std3).

Citation. 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, arXiv v1, pp. 3–4: “A string of 𝐁ₙ is called run-constrained-circularly if every run of 1s appearing in this string is immediately followed by a strictly longer run of 0s in a circular manner.” Positions are labelled Fin n and letters are Bool. The all-ones word is excluded for positive n; n=0 denotes the empty word.

Definition 1.6 (flip).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\forall (i:\mathrm{Fin}n),\mathrm{flip}wi=(\mathrm{Function}.\mathrm{update}wi(!wi))$$

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

Updating one Boolean letter to its negation gives the one-bit neighbour.

Definition 1.7 (degree).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\mathrm{degree}w=((\mathrm{Finset}.\mathrm{univ}.\mathrm{filter}(\mathrm{fun}i:\mathrm{Fin}n\mapsto \mathrm{Admissible}(\mathrm{CircularWords}.\mathrm{flip}wi))).\mathrm{card})$$

Formalization. D5/S1/Words/AssociatedMersenne/CircularWords.degree (✓ 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 all positions by admissibility of their one-bit neighbours counts the degree.

Definition 1.8 (N).

$$\forall (n:\mathrm{Nat}),\forall (k:\mathrm{Nat}),Nnk=((\mathrm{Finset}.\mathrm{univ}.\mathrm{filter}(\mathrm{fun}w:\mathrm{Fin}n\to \mathrm{Bool}\mapsto \mathrm{Admissible}w\wedge \mathrm{degree}w=k)).\mathrm{card})$$

Formalization. D5/S1/Words/AssociatedMersenne/CircularWords.N (✓ 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 labelled words by admissibility and degree gives the degree histogram.

Lemma 1.9 (cycAdd sub one).

$$\forall (n:\mathrm{Nat}),\forall (i:\mathrm{Fin}n),\mathrm{cycAdd}i(n-1)=\mathrm{cycSub}i1$$

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

Positivity of the length identifies the offset n minus one with the predecessor.

Lemma 1.10 (start large false).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\forall (i:\mathrm{Fin}n),\forall (r:\mathrm{Nat}),(n\le r)\to (\neg \mathrm{IsOneRunStart}wir)$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/CircularWords.start_large_false (✓ 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 run of at least the full length would make its zero predecessor a one.

Lemma 1.11 (cycAdd zero).

$$\forall (n:\mathrm{Nat}),\forall (i:\mathrm{Fin}n),\mathrm{cycAdd}i0=i$$

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

Reduction modulo the length leaves the original position unchanged at offset zero.

Lemma 1.12 (cycAdd val).

$$\forall (n:\mathrm{Nat}),\forall (i:\mathrm{Fin}n),\forall (j:\mathrm{Nat}),(\mathrm{cycAdd}ij).\mathrm{val}=(i.\mathrm{val}+j)\mathrm{Nat}.\mathrm{mod}n$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/CircularWords.cycAdd_val (✓ 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 value of circular addition is the remainder of the sum of the labelled index and offset.

Lemma 1.13 (cycAdd assoc).

$$\forall (n:\mathrm{Nat}),\forall (i:\mathrm{Fin}n),\forall (j:\mathrm{Nat}),\forall (k:\mathrm{Nat}),\mathrm{cycAdd}(\mathrm{cycAdd}ij)k=\mathrm{cycAdd}i(j+k)$$

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

Remainder arithmetic identifies successive offsets with their sum.

Lemma 1.14 (cycAdd inj).

$$\forall (n:\mathrm{Nat}),\forall (i:\mathrm{Fin}n),\forall (j:\mathrm{Nat}),\forall (k:\mathrm{Nat}),(j<n)\to ((k<n)\to (\mathrm{cycAdd}ij=\mathrm{cycAdd}ik⟺j=k))$$

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

Offsets below the length are uniquely determined by their circular positions.

Lemma 1.15 (zero admissible).

$$\forall (n:\mathrm{Nat}),\mathrm{Admissible}(\mathrm{Function}.\mathrm{const}(\mathrm{Fin}n)\mathrm{false})$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/CircularWords.zero_admissible (✓ 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 zero word has no positive run and satisfies every required zero-gap condition.

Lemma 1.16 (zero degree).

$$\forall (n:\mathrm{Nat}),\mathrm{degree}(\mathrm{Function}.\mathrm{const}(\mathrm{Fin}n)\mathrm{false})=\mathrm{if}n\le 2\mathrm{then}0\mathrm{else}n$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/CircularWords.zero_degree (✓ 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 singleton one is admissible precisely when the length exceeds two, determining every flip of the zero word.

Definition 1.17 (offset).

$$\forall (n:\mathrm{Nat}),\forall (i:\mathrm{Fin}n),\forall (q:\mathrm{Fin}n),\mathrm{offset}iq=((q.\mathrm{val}+n-i.\mathrm{val})\mathrm{Nat}.\mathrm{mod}n)$$

Formalization. D5/S1/Words/AssociatedMersenne/CircularWords.offset (✓ 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 remainder of the target index minus the starting index gives a bounded forward offset.

Lemma 1.18 (cycAdd offset).

$$\forall (n:\mathrm{Nat}),\forall (i:\mathrm{Fin}n),\forall (q:\mathrm{Fin}n),\mathrm{cycAdd}i(\mathrm{offset}iq)=q$$

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

Adding the remainder offset recovers the target labelled position.

Lemma 1.19 (offset lt).

$$\forall (n:\mathrm{Nat}),\forall (i:\mathrm{Fin}n),\forall (q:\mathrm{Fin}n),\mathrm{offset}iq<n$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/CircularWords.offset_lt (✓ 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 remainder defining an offset is strictly below the positive word length.

Lemma 1.20 (cycAdd bijective).

$$\forall (n:\mathrm{Nat}),\forall (i:\mathrm{Fin}n),\mathrm{Function}.\mathrm{Bijective}(\mathrm{fun}j:\mathrm{Fin}n\mapsto \mathrm{cycAdd}ij.\mathrm{val})$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/CircularWords.cycAdd_bijective (✓ 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 bounded offset gives an inverse to circular addition on all labelled positions.

Definition 1.21 (linearize).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\forall (i:\mathrm{Fin}n),\mathrm{linearize}wi=(\mathrm{List}.\mathrm{ofFn}(\mathrm{fun}j:\mathrm{Fin}n\mapsto w(\mathrm{cycAdd}ij.\mathrm{val})))$$

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

Reading one complete circle from the marked position gives a linear Boolean list.

Lemma 1.22 (linearize injective).

$$\forall (n:\mathrm{Nat}),\forall (i:\mathrm{Fin}n),\mathrm{Function}.\mathrm{Injective}(\mathrm{fun}w:\mathrm{Fin}n\to \mathrm{Bool}\mapsto \mathrm{linearize}wi)$$

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

Every labelled position occurs in the linear reading, so equal readings determine equal words.

Lemma 1.23 (linearize length).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\forall (i:\mathrm{Fin}n),(\mathrm{linearize}wi).\mathrm{length}=n$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/CircularWords.linearize_length (✓ 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 list of labelled positions has exactly the word length.

Lemma 1.24 (one run length unique).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\forall (i:\mathrm{Fin}n),\forall (r:\mathrm{Nat}),\forall (s:\mathrm{Nat}),(\mathrm{IsOneRunStart}wir)\to ((\mathrm{IsOneRunStart}wis)\to (r=s))$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/CircularWords.one_run_length_unique (✓ 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 zero ending a run contradicts any longer run from the same start.

Definition 1.25 (IsMarkedStart).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\forall (i:\mathrm{Fin}n),\mathrm{IsMarkedStart}wi⟺(\exists r,0<r\wedge \mathrm{IsOneRunStart}wir)$$

Formalization. D5/S1/Words/AssociatedMersenne/CircularWords.IsMarkedStart (✓ 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 mark records a one-run start with strictly positive run length.

Lemma 1.26 (marked start true).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\forall (i:\mathrm{Fin}n),(\mathrm{IsMarkedStart}wi)\to (wi=\mathrm{true})$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/CircularWords.marked_start_true (✓ 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 zero offset in a positive run forces the marked letter to be one.

Lemma 1.27 (marked start predecessor).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\forall (i:\mathrm{Fin}n),(\mathrm{IsMarkedStart}wi)\to (w(\mathrm{cycSub}i1)=\mathrm{false})$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/CircularWords.marked_start_predecessor (✓ 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 defining predecessor condition forces the letter before a mark to be zero.

Lemma 1.28 (marked start iff).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\forall (i:\mathrm{Fin}n),\mathrm{IsMarkedStart}wi⟺w(\mathrm{cycSub}i1)=\mathrm{false}\wedge wi=\mathrm{true}$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/CircularWords.marked_start_iff (✓ 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 one after a zero extends to its first following zero, giving a positive marked run.

Lemma 1.29 (cycAdd predecessor pos).

$$\forall (n:\mathrm{Nat}),\forall (i:\mathrm{Fin}n),\forall (j:\mathrm{Nat}),(0<j)\to (\mathrm{cycSub}(\mathrm{cycAdd}ij)1=\mathrm{cycAdd}i(j-1))$$

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

Moving back one position from a positive offset agrees with adding the offset minus one.

Lemma 1.30 (nonzero has marked start).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),(\exists p,wp=\mathrm{false})\to ((\exists q,wq=\mathrm{true})\to (\exists i,\mathrm{IsMarkedStart}wi))$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/CircularWords.nonzero_has_marked_start (✓ 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 least one encountered after a zero supplies a zero-to-one transition and hence a mark.

Lemma 1.31 (admissible nonzero has marked start).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),(\mathrm{Admissible}w)\to ((\exists q,wq=\mathrm{true})\to (\exists i,\mathrm{IsMarkedStart}wi))$$

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

Admissibility supplies a zero, while a nonzero word supplies the one needed for a marked transition.

Definition 1.32 (runCount).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\mathrm{runCount}w=((\mathrm{Finset}.\mathrm{univ}.\mathrm{filter}(\mathrm{IsMarkedStart}w)).\mathrm{card})$$

Formalization. D5/S1/Words/AssociatedMersenne/CircularWords.runCount (✓ 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 marked starts counts the circular runs of ones.

Definition 1.33 (DegreeRunWords).

$$\forall (n:\mathrm{Nat}),\forall (\mathrm{ell}:\mathrm{Nat}),\forall (k:\mathrm{Nat}),\mathrm{DegreeRunWords}n\mathrm{ell}k=(\{w:\mathrm{Fin}n\to \mathrm{Bool}//\mathrm{Admissible}w\wedge \mathrm{degree}w=k\wedge \mathrm{runCount}w=\mathrm{ell}\})$$

Formalization. D5/S1/Words/AssociatedMersenne/CircularWords.DegreeRunWords (✓ 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 admissibility, run count and degree for labelled words of a given length.

Definition 1.34 (MarkedDegreeRunWords).

$$\forall (n:\mathrm{Nat}),\forall (\mathrm{ell}:\mathrm{Nat}),\forall (k:\mathrm{Nat}),\mathrm{MarkedDegreeRunWords}n\mathrm{ell}k=((w:\mathrm{DegreeRunWords}n\mathrm{ell}k)\times \{i:\mathrm{Fin}n//\mathrm{IsMarkedStart}w.\mathrm{val}i\})$$

Formalization. D5/S1/Words/AssociatedMersenne/CircularWords.MarkedDegreeRunWords (✓ 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 pairs a degree-and-run-count word with one of its positive marked starts.

Definition 1.35 (instFintypeDegreeRunWords).

$$\forall (n:\mathrm{Nat}),\forall (\mathrm{ell}:\mathrm{Nat}),\forall (k:\mathrm{Nat}),\mathrm{instFintypeDegreeRunWords}n\mathrm{ell}k:\mathrm{Fintype}(\mathrm{DegreeRunWords}n\mathrm{ell}k)$$

Formalization. D5/S1/Words/AssociatedMersenne/CircularWords.instFintypeDegreeRunWords (✓ 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 Fin n → Bool satisfying Admissible, degree = k and runCount = ell.

Definition 1.36 (instFintypeMarkedDegreeRunWords).

$$\forall (n:\mathrm{Nat}),\forall (\mathrm{ell}:\mathrm{Nat}),\forall (k:\mathrm{Nat}),\mathrm{instFintypeMarkedDegreeRunWords}n\mathrm{ell}k:\mathrm{Fintype}(\mathrm{MarkedDegreeRunWords}n\mathrm{ell}k)$$

Formalization. D5/S1/Words/AssociatedMersenne/CircularWords.instFintypeMarkedDegreeRunWords (✓ 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 dependent pair of a DegreeRunWords n ell k word and a Fin n position satisfying IsMarkedStart.

Theorem 1.37 (marked double count of equiv).

$$\forall (n:\mathrm{Nat}),\forall (\mathrm{ell}:\mathrm{Nat}),\forall (k:\mathrm{Nat}),\forall (T:\mathrm{Type}),[\mathrm{Fintype}T],(\mathrm{MarkedDegreeRunWords}n\mathrm{ell}k\equiv \mathrm{Fin}n\times T)\to (\mathrm{ell}\cdot \mathrm{Fintype}.\mathrm{card}(\mathrm{DegreeRunWords}n\mathrm{ell}k)=n\cdot \mathrm{Fintype}.\mathrm{card}T)$$

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

T is a finite type in an arbitrary universe. An equivalence between labelled marked words and Fin n × T gives the displayed double count without dividing by the number of runs.

Definition 1.38 (rotateWord).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\forall (i:\mathrm{Fin}n),\mathrm{rotateWord}wi=(\mathrm{fun}j\mapsto w(\mathrm{cycAdd}ij.\mathrm{val}))$$

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

Changing the starting labelled position reads the same circular word by circular addition.

Theorem 1.39 (rotateWord admissible iff).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\forall (i:\mathrm{Fin}n),\mathrm{Admissible}(\mathrm{rotateWord}wi)⟺\mathrm{Admissible}w$$

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

Circular addition transports each run start and its following zero gap in both directions.

Lemma 1.40 (rotateWord degree).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\forall (i:\mathrm{Fin}n),\mathrm{degree}(\mathrm{rotateWord}wi)=\mathrm{degree}w$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/CircularWords.rotateWord_degree (✓ 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 bijection on positions transports legal one-bit flips and preserves their count.

Theorem 1.41 (next one gap bound).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\forall (a:\mathrm{Fin}n),\forall (r:\mathrm{Nat}),\forall (z:\mathrm{Nat}),(\mathrm{Admissible}w)\to ((\mathrm{IsOneRunStart}war)\to ((w(\mathrm{cycAdd}a(r+z))=\mathrm{true})\to (r<z)))$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/CircularWords.next_one_gap_bound (✓ 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 later one cannot occur inside the zero gap forced by admissibility of the preceding run.

Theorem 1.42 (linearize move mark).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\forall (i:\mathrm{Fin}n),\forall (p:\mathrm{Nat}),\mathrm{linearize}w(\mathrm{cycAdd}ip)=(\mathrm{linearize}wi).\mathrm{rotate}p$$

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

Moving the marked origin rotates the linear list by the corresponding bounded offset.

References

• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.Admissible
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.DegreeRunWords
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.IsMarkedStart
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.IsOneRunStart
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.MarkedDegreeRunWords
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.N
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.admissible_nonzero_has_marked_start
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.cycAdd
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.cycAdd_assoc
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.cycAdd_bijective
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.cycAdd_inj
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.cycAdd_offset
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.cycAdd_predecessor_pos
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.cycAdd_sub_one
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.cycAdd_val
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.cycAdd_zero
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.cycSub
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.degree
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.flip
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.instFintypeDegreeRunWords
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.instFintypeMarkedDegreeRunWords
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.linearize
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.linearize_injective
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.linearize_length
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.linearize_move_mark
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.marked_double_count_of_equiv
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.marked_start_iff
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.marked_start_predecessor
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.marked_start_true
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.next_one_gap_bound
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.nonzero_has_marked_start
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.offset
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.offset_lt
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.one_run_length_unique
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.rotateWord
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.rotateWord_admissible_iff
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.rotateWord_degree
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.runCount
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.split_reverse_map
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.start_large_false
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.zero_admissible
• Truth anchor: D5/S1/Words/AssociatedMersenne/CircularWords.zero_degree