TwoDeletionRunDecks

Abstract

Exact binary run counts and input entropy for two deletions and insertions.

Definition 1.1 (adjacentWeights).

$$\begin{array}{r}\mathrm{adjacentWeights}[]=([])\\ \forall (a:\mathbb{N}),(\mathrm{adjacentWeights}[a]=([]))\\ \forall (a:\mathbb{N}),(\forall (b:\mathbb{N}),(\forall (rs:\mathrm{List}\mathbb{N}),(\mathrm{adjacentWeights}(a::b::rs)=(a\cdot b::\mathrm{adjacentWeights}(b::rs)))))\end{array}$$

Formalization. D5/S1/Words/TwoDeletionRunDecks.adjacentWeights (✓ std3).

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed expression defines adjacentWeights.

Definition 1.2 (pairWeights).

$$\begin{array}{r}\mathrm{pairWeights}[]=([])\\ \forall (a:\mathbb{N}),(\forall (rs:\mathrm{List}\mathbb{N}),(\mathrm{pairWeights}(a::rs)=(rs.\mathrm{map}(\mathrm{fun}b\mapsto (a\cdot b))++\mathrm{pairWeights}rs)))\end{array}$$

Formalization. D5/S1/Words/TwoDeletionRunDecks.pairWeights (✓ std3).

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed expression defines pairWeights.

Definition 1.3 (prefixBlocks).

$$\forall (pre:\mathrm{List}\mathrm{Bool}),(\forall (bs:\mathrm{List}(\mathrm{List}\mathrm{Bool}\times \mathbb{N})),(\mathrm{prefixBlocks}prebs=(bs.\mathrm{map}(\mathrm{fun}p\mapsto ((pre++p.1,p.2))))))$$

Formalization. D5/S1/Words/TwoDeletionRunDecks.prefixBlocks (✓ std3).

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed expression defines prefixBlocks.

Definition 1.4 (deletionDeck).

$$\forall (\alpha :\mathrm{Type}),(\forall (k:\mathbb{N}),(\forall (w:\mathrm{List}\alpha ),(\mathrm{deletionDeck}(\alpha :=\alpha )kw=(\mathrm{if}k\le w.\mathrm{length}\mathrm{then}w.\mathrm{sublistsLen}(w.\mathrm{length}-k)\mathrm{else}[]))))$$

Formalization. D5/S1/Words/TwoDeletionRunDecks.deletionDeck (✓ std3).

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed expression defines deletionDeck.

Definition 1.5 (runWord).

$$\begin{array}{r}\forall (b:\mathrm{Bool}),(\mathrm{runWord}b[]=([]))\\ \forall (b:\mathrm{Bool}),(\forall (r:\mathbb{N}),(\forall (rs:\mathrm{List}\mathbb{N}),(\mathrm{runWord}b(r::rs)=(\mathrm{List}.\mathrm{replicate}rb++\mathrm{runWord}(!b)rs))))\end{array}$$

Formalization. D5/S1/Words/TwoDeletionRunDecks.runWord (✓ std3).

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed expression defines runWord.

Definition 1.6 (sameRunWeights).

$$\forall (rs:\mathrm{List}\mathbb{N}),(\mathrm{sameRunWeights}rs=((rs.\mathrm{filter}\mathrm{fun}r\mapsto (2\le r)).\mathrm{map}(\mathrm{fun}r\mapsto (r.\mathrm{choose}2))))$$

Formalization. D5/S1/Words/TwoDeletionRunDecks.sameRunWeights (✓ std3).

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed expression defines sameRunWeights.

Definition 1.7 (nonadjacentWeights).

$$\begin{array}{r}\mathrm{nonadjacentWeights}[]=([])\\ \forall (a:\mathbb{N}),(\forall (rs:\mathrm{List}\mathbb{N}),(\mathrm{nonadjacentWeights}(a::rs)=((rs.\mathrm{drop}1).\mathrm{map}(\mathrm{fun}b\mapsto (a\cdot b))++\mathrm{nonadjacentWeights}rs)))\end{array}$$

Formalization. D5/S1/Words/TwoDeletionRunDecks.nonadjacentWeights (✓ std3).

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed expression defines nonadjacentWeights.

Definition 1.8 (componentWeightsAux).

$$\begin{array}{r}\forall (acc:\mathbb{N}),(\forall (prev:\mathbb{N}),(\mathrm{componentWeightsAux}accprev[]=([acc])))\\ \forall (acc:\mathbb{N}),(\forall (prev:\mathbb{N}),(\forall (r:\mathbb{N}),(\forall (rs:\mathrm{List}\mathbb{N}),(\mathrm{componentWeightsAux}accprev(r::rs)=(\mathrm{if}prev=1\mathrm{then}\mathrm{componentWeightsAux}(acc+prev\cdot r)rrs\mathrm{else}acc::\mathrm{componentWeightsAux}(prev\cdot r)rrs)))))\end{array}$$

Formalization. D5/S1/Words/TwoDeletionRunDecks.componentWeightsAux (✓ std3).

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed expression defines componentWeightsAux.

Theorem 1.9 (blockLengths_positive).

$$\forall (w:\mathrm{List}\mathrm{Bool}),(\forall r\in \mathrm{blockLengths}w,(0<r))$$

Proof. Machine-checked in Lean as D5/S1/Words/TwoDeletionRunDecks.blockLengths_positive (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed identity or comparison relates binary embedding counts and their run profiles.

Definition 1.10 (realizeBlocks).

$$\forall (\alpha :\mathrm{Type}),(\forall (bs:\mathrm{List}(\alpha \times \mathbb{N})),(\mathrm{realizeBlocks}(\alpha :=\alpha )bs=(bs.\mathrm{flatMap}(\mathrm{fun}p\mapsto (\mathrm{List}.\mathrm{replicate}p.2p.1)))))$$

Formalization. D5/S1/Words/TwoDeletionRunDecks.realizeBlocks (✓ std3).

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed expression defines realizeBlocks.

Definition 1.11 (mergeWeightedAux).

$$\begin{array}{r}\forall (\alpha :\mathrm{Type}),(\forall (p:\alpha \times \mathbb{N}),(\forall (prev:\mathbb{N}),(\forall (\mathrm{es}:\mathrm{List}(\alpha \times \mathbb{N})),(\mathrm{mergeWeightedAux}(\alpha :=\alpha )pprev[]\mathrm{es}=([p])))))\\ \forall (\alpha :\mathrm{Type}),(\forall (p:\alpha \times \mathbb{N}),(\forall (prev:\mathbb{N}),(\forall (r:\mathbb{N}),(\forall (rs:\mathrm{List}\mathbb{N}),(\mathrm{mergeWeightedAux}(\alpha :=\alpha )pprev(r::rs)[]=([p]))))))\\ \forall (\alpha :\mathrm{Type}),(\forall (p:\alpha \times \mathbb{N}),(\forall (q:\alpha \times \mathbb{N}),(\forall (prev:\mathbb{N}),(\forall (r:\mathbb{N}),(\forall (rs:\mathrm{List}\mathbb{N}),(\forall (\mathrm{qs}:\mathrm{List}(\alpha \times \mathbb{N})),(\mathrm{mergeWeightedAux}(\alpha :=\alpha )pprev(r::rs)(q::\mathrm{qs})=(\mathrm{if}prev=1\mathrm{then}\mathrm{mergeWeightedAux}(p.1,p.2+q.2)rrs\mathrm{qs}\mathrm{else}p::\mathrm{mergeWeightedAux}qrrs\mathrm{qs}))))))))\end{array}$$

Formalization. D5/S1/Words/TwoDeletionRunDecks.mergeWeightedAux (✓ std3).

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed expression defines mergeWeightedAux.

Definition 1.12 (oneRunBlocks).

$$\begin{array}{r}\forall (b:\mathrm{Bool}),(\mathrm{oneRunBlocks}b[]=([]))\\ \forall (b:\mathrm{Bool}),(\forall (r:\mathbb{N}),(\forall (rs:\mathrm{List}\mathbb{N}),(\mathrm{oneRunBlocks}b(r::rs)=((\mathrm{List}.\mathrm{replicate}(r-1)b++\mathrm{runWord}(!b)rs,r)::((\mathrm{oneRunBlocks}(!b)rs).\mathrm{map}(\mathrm{fun}p\mapsto ((\mathrm{List}.\mathrm{replicate}rb++p.1,p.2))))))))\end{array}$$

Formalization. D5/S1/Words/TwoDeletionRunDecks.oneRunBlocks (✓ std3).

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed expression defines oneRunBlocks.

Definition 1.13 (edgeLabel).

$$\forall (b:\mathrm{Bool}),(\forall (a:\mathbb{N}),(\forall (c:\mathbb{N}),(\forall (rs:\mathrm{List}\mathbb{N}),(\mathrm{edgeLabel}bacrs=(\mathrm{List}.\mathrm{replicate}(a-1)b++\mathrm{List}.\mathrm{replicate}(c-1)(!b)++\mathrm{runWord}brs)))))$$

Formalization. D5/S1/Words/TwoDeletionRunDecks.edgeLabel (✓ std3).

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed expression defines edgeLabel.

Definition 1.14 (sameBlocks).

$$\begin{array}{r}\forall (b:\mathrm{Bool}),(\mathrm{sameBlocks}b[]=([]))\\ \forall (b:\mathrm{Bool}),(\forall (a:\mathbb{N}),(\forall (rs:\mathrm{List}\mathbb{N}),(\mathrm{sameBlocks}b(a::rs)=((\mathrm{List}.\mathrm{replicate}(a-2)b++\mathrm{runWord}(!b)rs,a.\mathrm{choose}2)::\mathrm{prefixBlocks}(\mathrm{List}.\mathrm{replicate}ab)(\mathrm{sameBlocks}(!b)rs)))))\end{array}$$

Formalization. D5/S1/Words/TwoDeletionRunDecks.sameBlocks (✓ std3).

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed expression defines sameBlocks.

Definition 1.15 (componentWeights).

$$\begin{array}{r}\mathrm{componentWeights}[]=([])\\ \forall (a:\mathbb{N}),(\mathrm{componentWeights}[a]=([]))\\ \forall (a:\mathbb{N}),(\forall (b:\mathbb{N}),(\forall (rs:\mathrm{List}\mathbb{N}),(\mathrm{componentWeights}(a::b::rs)=(\mathrm{componentWeightsAux}(a\cdot b)brs))))\end{array}$$

Formalization. D5/S1/Words/TwoDeletionRunDecks.componentWeights (✓ std3).

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed expression defines componentWeights.

Theorem 1.16 (runWord_length).

$$\forall (b:\mathrm{Bool}),(\forall (rs:\mathrm{List}\mathbb{N}),((\mathrm{runWord}brs).\mathrm{length}=rs.\mathrm{sum}))$$

Proof. Machine-checked in Lean as D5/S1/Words/TwoDeletionRunDecks.runWord_length (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed identity or comparison relates binary embedding counts and their run profiles.

Definition 1.17 (adjacentBlocks).

$$\begin{array}{r}\forall (b:\mathrm{Bool}),(\mathrm{adjacentBlocks}b[]=([]))\\ \forall (b:\mathrm{Bool}),(\forall (a:\mathbb{N}),(\mathrm{adjacentBlocks}b[a]=([])))\\ \forall (b:\mathrm{Bool}),(\forall (a:\mathbb{N}),(\forall (c:\mathbb{N}),(\forall (rs:\mathrm{List}\mathbb{N}),(\mathrm{adjacentBlocks}b(a::c::rs)=((\mathrm{edgeLabel}bacrs,a\cdot c)::\mathrm{prefixBlocks}(\mathrm{List}.\mathrm{replicate}ab)(\mathrm{adjacentBlocks}(!b)(c::rs)))))))\end{array}$$

Formalization. D5/S1/Words/TwoDeletionRunDecks.adjacentBlocks (✓ std3).

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed expression defines adjacentBlocks.

Definition 1.18 (nonadjBlocks).

$$\begin{array}{r}\forall (b:\mathrm{Bool}),(\mathrm{nonadjBlocks}b[]=([]))\\ \forall (b:\mathrm{Bool}),(\forall (a:\mathbb{N}),(\mathrm{nonadjBlocks}b[a]=([])))\\ \forall (b:\mathrm{Bool}),(\forall (a:\mathbb{N}),(\forall (c:\mathbb{N}),(\forall (rs:\mathrm{List}\mathbb{N}),(\mathrm{nonadjBlocks}b(a::c::rs)=(((\mathrm{oneRunBlocks}brs).\mathrm{map}(\mathrm{fun}p\mapsto ((\mathrm{List}.\mathrm{replicate}(a-1)b++\mathrm{List}.\mathrm{replicate}c(!b)++p.1,a\cdot p.2))))++\mathrm{prefixBlocks}(\mathrm{List}.\mathrm{replicate}ab)(\mathrm{nonadjBlocks}(!b)(c::rs)))))))\end{array}$$

Formalization. D5/S1/Words/TwoDeletionRunDecks.nonadjBlocks (✓ std3).

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed expression defines nonadjBlocks.

Theorem 1.19 (sameBlocks_weights).

$$\forall (b:\mathrm{Bool}),(\forall (rs:\mathrm{List}\mathbb{N}),((\mathrm{sameBlocks}brs).\mathrm{map}\mathrm{Prod}.\mathrm{snd}=rs.\mathrm{map}(\mathrm{fun}a\mapsto (a.\mathrm{choose}2))))$$

Proof. Machine-checked in Lean as D5/S1/Words/TwoDeletionRunDecks.sameBlocks_weights (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed identity or comparison relates binary embedding counts and their run profiles.

Definition 1.20 (collisionWeights).

$$\forall (rs:\mathrm{List}\mathbb{N}),(\mathrm{collisionWeights}rs=(\mathrm{sameRunWeights}rs++\mathrm{nonadjacentWeights}rs++\mathrm{componentWeights}rs))$$

Formalization. D5/S1/Words/TwoDeletionRunDecks.collisionWeights (✓ std3).

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed expression defines collisionWeights.

Theorem 1.21 (runWord_blockLengths).

$$\forall (w:\mathrm{List}\mathrm{Bool}),(\mathrm{runWord}(w.\mathrm{headD}\mathrm{false})(\mathrm{blockLengths}w)=w)$$

Proof. Machine-checked in Lean as D5/S1/Words/TwoDeletionRunDecks.runWord_blockLengths (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed identity or comparison relates binary embedding counts and their run profiles.

Definition 1.22 (componentBlocks).

$$\begin{array}{r}\forall (b:\mathrm{Bool}),(\mathrm{componentBlocks}b[]=([]))\\ \forall (b:\mathrm{Bool}),(\forall (a:\mathbb{N}),(\mathrm{componentBlocks}b[a]=([])))\\ \forall (b:\mathrm{Bool}),(\forall (a:\mathbb{N}),(\forall (c:\mathbb{N}),(\forall (rs:\mathrm{List}\mathbb{N}),(\mathrm{componentBlocks}b(a::c::rs)=(\mathrm{mergeWeightedAux}(\mathrm{edgeLabel}bacrs,a\cdot c)crs(\mathrm{prefixBlocks}(\mathrm{List}.\mathrm{replicate}ab)(\mathrm{adjacentBlocks}(!b)(c::rs))))))))\end{array}$$

Formalization. D5/S1/Words/TwoDeletionRunDecks.componentBlocks (✓ std3).

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed expression defines componentBlocks.

Theorem 1.23 (nonadjBlocks_weights).

$$\forall (b:\mathrm{Bool}),(\forall (rs:\mathrm{List}\mathbb{N}),((\mathrm{nonadjBlocks}brs).\mathrm{map}\mathrm{Prod}.\mathrm{snd}=\mathrm{nonadjacentWeights}rs))$$

Proof. Machine-checked in Lean as D5/S1/Words/TwoDeletionRunDecks.nonadjBlocks_weights (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed identity or comparison relates binary embedding counts and their run profiles.

Theorem 1.24 (twoDeletionDeck_eq_deletionDeck).

$$\forall (w:\mathrm{List}\mathrm{Bool}),((2\le w.\mathrm{length})\to ((w.\mathrm{sublistsLen}(w.\mathrm{length}-2))=\mathrm{deletionDeck}2w))$$

Proof. Machine-checked in Lean as D5/S1/Words/TwoDeletionRunDecks.twoDeletionDeck_eq_deletionDeck (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed identity or comparison relates binary embedding counts and their run profiles.

Theorem 1.25 (componentBlocks_weights).

$$\forall (b:\mathrm{Bool}),(\forall (rs:\mathrm{List}\mathbb{N}),((\mathrm{componentBlocks}brs).\mathrm{map}\mathrm{Prod}.\mathrm{snd}=\mathrm{componentWeights}rs))$$

Proof. Machine-checked in Lean as D5/S1/Words/TwoDeletionRunDecks.componentBlocks_weights (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed identity or comparison relates binary embedding counts and their run profiles.

Definition 1.26 (collisionBlocks).

$$\forall (b:\mathrm{Bool}),(\forall (rs:\mathrm{List}\mathbb{N}),(\mathrm{collisionBlocks}brs=(\mathrm{sameBlocks}brs++\mathrm{nonadjBlocks}brs++\mathrm{componentBlocks}brs)))$$

Formalization. D5/S1/Words/TwoDeletionRunDecks.collisionBlocks (✓ std3).

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed expression defines collisionBlocks.

Theorem 1.27 (collisionBlocks_realize).

$$\forall (b:\mathrm{Bool}),(\forall (rs:\mathrm{List}\mathbb{N}),((\forall r\in rs,(0<r))\to ((\mathrm{realizeBlocks}(\mathrm{collisionBlocks}brs)).\mathrm{Perm}(\mathrm{deletionDeck}2(\mathrm{runWord}brs)))))$$

Proof. Machine-checked in Lean as D5/S1/Words/TwoDeletionRunDecks.collisionBlocks_realize (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. S. Singhvi; O. Sabary; D. Bar-Lev; E. Yaakobi (2025). Conditional Entropies of k-Deletion/Insertion Channels. DOI: 10.1109/TIT.2025.3581849. URL: https://arxiv.org/abs/2407.10026v2.

Commentary.

The displayed identity or comparison relates binary embedding counts and their run profiles.

References

• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.adjacentBlocks
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.adjacentWeights
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.blockLengths_positive
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.collisionBlocks
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.collisionBlocks_realize
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.collisionWeights
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.componentBlocks
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.componentBlocks_weights
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.componentWeights
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.componentWeightsAux
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.deletionDeck
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.edgeLabel
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.mergeWeightedAux
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.nonadjBlocks
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.nonadjBlocks_weights
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.nonadjacentWeights
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.oneRunBlocks
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.pairWeights
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.prefixBlocks
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.realizeBlocks
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.runWord
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.runWord_blockLengths
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.runWord_length
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.sameBlocks
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.sameBlocks_weights
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.sameRunWeights
• Truth anchor: D5/S1/Words/TwoDeletionRunDecks.twoDeletionDeck_eq_deletionDeck
• Dependency: D5/S1/Words/AssociatedMersenne/RunTupleBijection