RunTupleBijection

Abstract

Degree enumeration for labelled circular run-constrained words.

Definition 1.1 (tupleList).

$$\forall (t:\mathrm{List}(\mathrm{Nat}\times \mathrm{Nat})),\mathrm{tupleList}t=((t.\mathrm{flatMap}(\mathrm{fun}b\mapsto [\mathrm{List}.\mathrm{replicate}b.1\mathrm{true},\mathrm{List}.\mathrm{replicate}(b.1+1+b.2)\mathrm{false}])).\mathrm{flatten})$$

Formalization. D5/S1/Words/AssociatedMersenne/RunTupleBijection.tupleList (✓ 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 positive run is followed by its compulsory longer zero block and its additional slack.

Definition 1.2 (blockLengths).

$$\forall (w:\mathrm{List}\mathrm{Bool}),\mathrm{blockLengths}w=((w.\mathrm{splitBy}(\mathrm{fun}ab\mapsto BEq.beq\left(a,b\right))).\mathrm{map}\mathrm{List}.\mathrm{length})$$

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

Splitting at changes of Boolean value records the successive constant-block lengths.

Lemma 1.3 (tupleList length).

$$\forall (t:\mathrm{List}(\mathrm{Nat}\times \mathrm{Nat})),(\mathrm{tupleList}t).\mathrm{length}=(t.\mathrm{map}(\mathrm{fun}b\mapsto 2\cdot b.1+1+b.2)).\mathrm{sum}$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/RunTupleBijection.tupleList_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 run and zero blocks contribute two times the run length plus one plus the slack.

Definition 1.4 (decodeLengths).

$$\begin{array}{r}\mathrm{decodeLengths}[]=[]\\ \forall (rz:\mathrm{Nat})(\mathrm{rest}:\mathrm{List}\mathrm{Nat}),\mathrm{decodeLengths}(r::z::\mathrm{rest})=(r,z-(r+1))::\mathrm{decodeLengths}\mathrm{rest}\\ \forall (r:\mathrm{Nat}),\mathrm{decodeLengths}[r]=[]\end{array}$$

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

Successive one and zero block lengths determine a run length and its excess zero slack.

Definition 1.5 (extractListTuple).

$$\forall (w:\mathrm{List}\mathrm{Bool}),\mathrm{extractListTuple}w=(\mathrm{decodeLengths}(\mathrm{blockLengths}w))$$

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

Constant-block splitting followed by length decoding extracts the ordered run-and-slack tuple.

Definition 1.6 (wordOfTuple).

$$\forall (n:\mathrm{Nat}),\forall (i:\mathrm{Fin}n),\forall (t:\mathrm{List}(\mathrm{Nat}\times \mathrm{Nat})),\forall (\mathrm{hlen}:(\mathrm{tupleList}t).\mathrm{length}=n),\forall (q:\mathrm{Fin}n),\mathrm{wordOfTuple}it\mathrm{hlen}q=(\mathrm{tupleList}t)[\mathrm{offset}iq]$$

Formalization. D5/S1/Words/AssociatedMersenne/RunTupleBijection.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 defining list access uses the bound obtained from hlen and offset_lt; proof arguments do not change the returned letter.

Theorem 1.7 (linearize wordOfTuple).

$$\forall (n:\mathrm{Nat}),\forall (i:\mathrm{Fin}n),\forall (t:\mathrm{List}(\mathrm{Nat}\times \mathrm{Nat})),\forall (\mathrm{hlen}:(\mathrm{tupleList}t).\mathrm{length}=n),\mathrm{linearize}(\mathrm{wordOfTuple}it\mathrm{hlen})i=\mathrm{tupleList}t$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/RunTupleBijection.linearize_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 inverse circular offset reads the reconstructed word as its original tuple list.

Definition 1.8 (rawWord).

$$\forall (t:\mathrm{List}(\mathrm{Nat}\times \mathrm{Nat})),\mathrm{rawWord}t=((t.\mathrm{map}(\mathrm{fun}b\mapsto \mathrm{List}.\mathrm{replicate}b.1\mathrm{true}++\mathrm{List}.\mathrm{replicate}b.2\mathrm{false})).\mathrm{flatten})$$

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

Flattening alternating replicated one and zero blocks encodes the unadjusted run-and-gap lengths.

Lemma 1.9 (rawWord cons).

$$\forall (b:\mathrm{Nat}\times \mathrm{Nat}),\forall (t:\mathrm{List}(\mathrm{Nat}\times \mathrm{Nat})),\mathrm{rawWord}(b::t)=\mathrm{List}.\mathrm{replicate}b.1\mathrm{true}++\mathrm{List}.\mathrm{replicate}b.2\mathrm{false}++\mathrm{rawWord}t$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/RunTupleBijection.rawWord_cons (✓ 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 first raw pair contributes its replicated one block and zero block before the remaining pairs.

Lemma 1.10 (rawWord append).

$$\forall (t:\mathrm{List}(\mathrm{Nat}\times \mathrm{Nat})),\forall (u:\mathrm{List}(\mathrm{Nat}\times \mathrm{Nat})),\mathrm{rawWord}(t++u)=\mathrm{rawWord}t++\mathrm{rawWord}u$$

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

Flattening the block encoding transports concatenation of pair lists to concatenation of words.

Lemma 1.11 (raw encoding marked).

$$\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})),(t\ne [])\to ((\forall b\in t,0<b.1\wedge 0<b.2)\to ((\mathrm{linearize}wi=\mathrm{rawWord}t)\to (\mathrm{IsMarkedStart}wi)))$$

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

Positive first and last block lengths give a one at the origin and a zero at its predecessor.

Lemma 1.12 (first raw run start).

$$\forall (n:\mathrm{Nat}),\forall (r:\mathrm{Nat}),\forall (z:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\forall (i:\mathrm{Fin}n),\forall (\mathrm{post}:\mathrm{List}\mathrm{Bool}),(0<r)\to ((0<z)\to ((\mathrm{IsMarkedStart}wi)\to ((\mathrm{linearize}wi=\mathrm{List}.\mathrm{replicate}r\mathrm{true}++\mathrm{List}.\mathrm{replicate}z\mathrm{false}++\mathrm{post})\to (\mathrm{IsOneRunStart}wir))))$$

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

The first replicated one block and its adjacent zero blocks delimit the first run.

Lemma 1.13 (linearize get optional).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\forall (i:\mathrm{Fin}n),\forall (j:\mathrm{Nat}),(j<n)\to (\mathrm{some}((\mathrm{linearize}wi)[j])=\mathrm{some}(w(\mathrm{cycAdd}ij)))$$

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

Optional list access equals some of the indexed letter. Since j<n and linearize has length n, the displayed ordinary indexing has the same value; the two occurrences of some retain the optional equality.

Theorem 1.14 (marked admissible tuple).

$$\forall (n:\mathrm{Nat}),\forall (w:\mathrm{Fin}n\to \mathrm{Bool}),\forall (i:\mathrm{Fin}n),(\mathrm{Admissible}w)\to ((\mathrm{IsMarkedStart}wi)\to (\exists t:\mathrm{List}(\mathrm{Nat}\times \mathrm{Nat}),t\ne []\wedge (\forall b\in t,0<b.1)\wedge (t.\mathrm{map}(\mathrm{fun}b\mapsto 2\cdot b.1+1+b.2)).\mathrm{sum}=n\wedge \mathrm{tupleList}t=\mathrm{linearize}wi\wedge \mathrm{extractListTuple}(\mathrm{linearize}wi)=t))$$

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

Alternating positive blocks recover the raw pairs, and admissibility turns every excess gap into nonnegative slack.

Theorem 1.15 (raw encoding admissible).

$$\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})),(t\ne [])\to ((\forall b\in t,0<b.1\wedge b.1<b.2)\to ((\mathrm{linearize}wi=\mathrm{rawWord}t)\to (\mathrm{Admissible}w)))$$

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

Every marked run lies at a block boundary whose longer zero block fulfils the circular gap condition.

Theorem 1.16 (raw encoding admissible iff).

$$\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})),(t\ne [])\to ((\forall b\in t,0<b.1\wedge 0<b.2)\to ((\mathrm{linearize}wi=\mathrm{rawWord}t)\to (\mathrm{Admissible}w⟺\forall b\in t,b.1<b.2)))$$

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

The block-boundary run starts make admissibility equivalent to the strict inequality for each following gap.

Definition 1.17 (pairPrefix).

$$\forall (t:\mathrm{List}(\mathrm{Nat}\times \mathrm{Nat})),\forall (p:\mathrm{Nat}),\mathrm{pairPrefix}tp=((\mathrm{rawWord}(t.\mathrm{take}p)).\mathrm{length})$$

Formalization. D5/S1/Words/AssociatedMersenne/RunTupleBijection.pairPrefix (✓ 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 earlier pair lengths gives the labelled offset of a raw pair boundary.

Definition 1.18 (rawPairs).

$$\forall (t:\mathrm{List}(\mathrm{Nat}\times \mathrm{Nat})),\mathrm{rawPairs}t=(t.\mathrm{map}(\mathrm{fun}b\mapsto (b.1,b.1+1+b.2)))$$

Formalization. D5/S1/Words/AssociatedMersenne/RunTupleBijection.rawPairs (✓ 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 compulsory run length plus one to the slack converts tuples into raw run-and-gap pairs.

Lemma 1.19 (tupleList eq rawPairs).

$$\forall (t:\mathrm{List}(\mathrm{Nat}\times \mathrm{Nat})),\mathrm{tupleList}t=\mathrm{rawWord}(\mathrm{rawPairs}t)$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/RunTupleBijection.tupleList_eq_rawPairs (✓ 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 compulsory zero lengths identify the slack encoding with the raw-pair encoding.

Lemma 1.20 (tuple word admissible).

$$\forall (n:\mathrm{Nat}),\forall (i:\mathrm{Fin}n),\forall (t:\mathrm{List}(\mathrm{Nat}\times \mathrm{Nat})),\forall (\mathrm{hlen}:(\mathrm{tupleList}t).\mathrm{length}=n),(t\ne [])\to ((\forall b\in t,0<b.1)\to (\mathrm{Admissible}(\mathrm{wordOfTuple}it\mathrm{hlen})))$$

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

Every positive tuple run has its compulsory strictly longer zero block in the reconstructed word.

Lemma 1.21 (tuple word marked).

$$\forall (n:\mathrm{Nat}),\forall (i:\mathrm{Fin}n),\forall (t:\mathrm{List}(\mathrm{Nat}\times \mathrm{Nat})),\forall (\mathrm{hlen}:(\mathrm{tupleList}t).\mathrm{length}=n),(t\ne [])\to ((\forall b\in t,0<b.1)\to (\mathrm{IsMarkedStart}(\mathrm{wordOfTuple}it\mathrm{hlen})i))$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/RunTupleBijection.tuple_word_marked (✓ 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 nonempty positive tuple begins with a one and ends with a zero, marking its reconstruction origin.

Definition 1.22 (GoodTuple).

$$\forall (n:\mathrm{Nat}),\mathrm{GoodTuple}n=(\{t:\mathrm{List}(\mathrm{Nat}\times \mathrm{Nat})//t\ne []\wedge (\forall b\in t,0<b.1)\wedge (\mathrm{tupleList}t).\mathrm{length}=n\})$$

Formalization. D5/S1/Words/AssociatedMersenne/RunTupleBijection.GoodTuple (✓ 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 a nonempty positive-run tuple whose encoded length is the prescribed length.

Definition 1.23 (MarkedWords).

$$\forall (n:\mathrm{Nat}),\mathrm{MarkedWords}n=(\{p:(\mathrm{Fin}n\to \mathrm{Bool})\times \mathrm{Fin}n//\mathrm{Admissible}p.1\wedge \mathrm{IsMarkedStart}p.1p.2\})$$

Formalization. D5/S1/Words/AssociatedMersenne/RunTupleBijection.MarkedWords (✓ 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 records an admissible labelled word together with a positive marked start.

Definition 1.24 (extractMarked).

$$\begin{array}{r}\forall (n:\mathrm{Nat}),\forall (x:\mathrm{MarkedWords}n),(\mathrm{extractMarked}x).1=x.\mathrm{val}.2\\ \forall (n:\mathrm{Nat}),\forall (x:\mathrm{MarkedWords}n),(\mathrm{extractMarked}x).2.\mathrm{val}=\mathrm{extractListTuple}(\mathrm{linearize}x.\mathrm{val}.1x.\mathrm{val}.2)\end{array}$$

Formalization. D5/S1/Words/AssociatedMersenne/RunTupleBijection.extractMarked (✓ 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 first component is the labelled run mark. The second component has the displayed underlying list, with its nonemptiness, positivity and total-length proofs supplied by marked_admissible_tuple.

Definition 1.25 (reconstructMarked).

$$\forall (n:\mathrm{Nat}),\forall (x:\mathrm{Fin}n\times \mathrm{GoodTuple}n),(\mathrm{reconstructMarked}x).\mathrm{val}=(\mathrm{wordOfTuple}x.1x.2.\mathrm{val}x.2.\mathrm{property}.2.2,x.1)$$

Formalization. D5/S1/Words/AssociatedMersenne/RunTupleBijection.reconstructMarked (✓ 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 displayed value is the underlying labelled word and mark. The subtype proof is supplied by tuple_word_admissible and tuple_word_marked.

Definition 1.26 (markedTupleEquiv).

$$\begin{array}{r}\forall (n:\mathrm{Nat}),\mathrm{markedTupleEquiv}n:\mathrm{MarkedWords}n\equiv \mathrm{Fin}n\times \mathrm{GoodTuple}n\\ \forall (n:\mathrm{Nat}),(\mathrm{markedTupleEquiv}n).\mathrm{toFun}=\mathrm{extractMarked}\\ \forall (n:\mathrm{Nat}),(\mathrm{markedTupleEquiv}n).\mathrm{invFun}=\mathrm{reconstructMarked}\end{array}$$

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

Extraction and reconstruction are inverse through constant-block decoding and the marked boundary conditions.

Definition 1.27 (instFiniteGoodTuple).

$$\forall (n:\mathrm{Nat}),\mathrm{instFiniteGoodTuple}n:\mathrm{Finite}(\mathrm{GoodTuple}n)$$

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

Finiteness is constructed by Finite.of_injective, using the map that sends a good tuple to its reconstructed List.Vector Bool n and the injectivity of that map.

Definition 1.28 (instFintypeGoodTuple).

$$\forall (n:\mathrm{Nat}),\mathrm{instFintypeGoodTuple}n:\mathrm{Fintype}(\mathrm{GoodTuple}n)$$

Formalization. D5/S1/Words/AssociatedMersenne/RunTupleBijection.instFintypeGoodTuple (✓ 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 enumerating instance is Fintype.ofFinite (GoodTuple n).

Theorem 1.29 (runCount wordOfTuple).

$$\forall (n:\mathrm{Nat}),\forall (i:\mathrm{Fin}n),\forall (t:\mathrm{List}(\mathrm{Nat}\times \mathrm{Nat})),\forall (\mathrm{hlen}:(\mathrm{tupleList}t).\mathrm{length}=n),(\forall b\in t,0<b.1)\to (\mathrm{runCount}(\mathrm{wordOfTuple}it\mathrm{hlen})=t.\mathrm{length})$$

Proof. Machine-checked in Lean as D5/S1/Words/AssociatedMersenne/RunTupleBijection.runCount_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 distinct pair-prefix positions enumerate exactly the marked starts of the reconstructed word.

Lemma 1.30 (extractMarked runs).

$$\forall (n:\mathrm{Nat}),\forall (x:\mathrm{MarkedWords}n),\mathrm{runCount}x.\mathrm{val}.1=(\mathrm{extractMarked}x).2.\mathrm{val}.\mathrm{length}$$

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

Reconstruction preserves the word, and the tuple length counts its marked run starts.

Definition 1.31 (RunTuples).

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

Formalization. D5/S1/Words/AssociatedMersenne/RunTupleBijection.RunTuples (✓ 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 restricts good tuples to a prescribed number of run-and-slack pairs.

References

• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.GoodTuple
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.MarkedWords
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.RunTuples
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.blockLengths
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.decodeLengths
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.extractListTuple
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.extractMarked
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.extractMarked_runs
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.first_raw_run_start
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.instFiniteGoodTuple
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.instFintypeGoodTuple
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.linearize_get_optional
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.linearize_wordOfTuple
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.markedTupleEquiv
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.marked_admissible_tuple
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.pairPrefix
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.rawPairs
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.rawWord
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.rawWord_append
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.rawWord_cons
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.raw_encoding_admissible
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.raw_encoding_admissible_iff
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.raw_encoding_marked
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.reconstructMarked
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.runCount_wordOfTuple
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.tupleList
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.tupleList_eq_rawPairs
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.tupleList_length
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.tuple_word_admissible
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.tuple_word_marked
• Truth anchor: D5/S1/Words/AssociatedMersenne/RunTupleBijection.wordOfTuple
• Dependency: D5/S1/Words/AssociatedMersenne/CircularWords
• Dependency: D5/S1/Words/Compositions/ConstantBlocksDistinctRunSums