BinaryRunSupersequenceCounts

Abstract

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

Definition 1.1 (wordSum).

$$\forall (n:\mathbb{N}),(\forall (F:(\mathrm{List}\mathrm{Bool})\to (\mathbb{R})),(\mathrm{wordSum}nF=(\sum _{x:\mathrm{Fin}n\to \mathrm{Bool}}(F(\mathrm{List}.\mathrm{ofFn}x)))))$$

Formalization. D5/S3/Entropy/BinaryRunSupersequenceCounts.wordSum (✓ 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 wordSum.

Definition 1.2 (leadingWeight).

$$\begin{array}{r}\mathrm{leadingWeight}[]=(0)\\ \forall (r:\mathbb{N}),(\forall (rs:\mathrm{List}\mathbb{N}),(\mathrm{leadingWeight}(r::rs)=(\mathrm{if}r=1\mathrm{then}1+\mathrm{leadingWeight}rs\mathrm{else}r)))\end{array}$$

Formalization. D5/S3/Entropy/BinaryRunSupersequenceCounts.leadingWeight (✓ 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 leadingWeight.

Theorem 1.3 (wordSum_succ).

$$\forall (n:\mathbb{N}),(\forall (b:\mathrm{Bool}),(\forall (F:(\mathrm{List}\mathrm{Bool})\to (\mathbb{R})),(\mathrm{wordSum}(n+1)F=\mathrm{wordSum}n(\mathrm{fun}w\mapsto (F(b::w)))+\mathrm{wordSum}n(\mathrm{fun}w\mapsto (F((!b)::w))))))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/BinaryRunSupersequenceCounts.wordSum_succ (✓ 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.4 (wordSum_congr).

$$\forall (n:\mathbb{N}),(\forall (F:(\mathrm{List}\mathrm{Bool})\to (\mathbb{R})),(\forall (G:(\mathrm{List}\mathrm{Bool})\to (\mathbb{R})),((\forall x,((x.\mathrm{length}=n)\to (Fx=Gx)))\to (\mathrm{wordSum}nF=\mathrm{wordSum}nG))))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/BinaryRunSupersequenceCounts.wordSum_congr (✓ 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.5 (wordSum_add).

$$\forall (n:\mathbb{N}),(\forall (F:(\mathrm{List}\mathrm{Bool})\to (\mathbb{R})),(\forall (G:(\mathrm{List}\mathrm{Bool})\to (\mathbb{R})),(\mathrm{wordSum}n(\mathrm{fun}x\mapsto (Fx+Gx))=\mathrm{wordSum}nF+\mathrm{wordSum}nG)))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/BinaryRunSupersequenceCounts.wordSum_add (✓ 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.6 (oneWordSum).

$$\forall (w:\mathrm{List}\mathrm{Bool}),(\forall (G:(\mathbb{N})\to (\mathbb{R})),(\mathrm{oneWordSum}wG=(\mathrm{wordSum}(w.\mathrm{length}+1)(\mathrm{fun}x\mapsto (G(\mathrm{scatteredCount}wx))))))$$

Formalization. D5/S3/Entropy/BinaryRunSupersequenceCounts.oneWordSum (✓ 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 oneWordSum.

Definition 1.7 (jointWordSum).

$$\forall (w:\mathrm{List}\mathrm{Bool}),(\forall (F:(\mathbb{N})\to ((\mathbb{N})\to (\mathbb{R}))),(\mathrm{jointWordSum}wF=(\mathrm{wordSum}(w.\mathrm{length}+1)(\mathrm{fun}x\mapsto (F(\mathrm{scatteredCount}wx)(\mathrm{scatteredCount}w.\mathrm{tail}x))))))$$

Formalization. D5/S3/Entropy/BinaryRunSupersequenceCounts.jointWordSum (✓ 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 jointWordSum.

Theorem 1.8 (oneWordSum_runs).

$$\forall (b:\mathrm{Bool}),(\forall (rs:\mathrm{List}\mathbb{N}),((\forall r\in rs,(0<r))\to (\forall (G:(\mathbb{N})\to (\mathbb{R})),((G0=0)\to (\mathrm{oneWordSum}(\mathrm{runWord}brs)G=(rs.\mathrm{map}(\mathrm{fun}r\mapsto (G(r+1)))).\mathrm{sum}+((rs.\mathrm{sum}:\mathbb{R})+2-rs.\mathrm{length})\cdot G1)))))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/BinaryRunSupersequenceCounts.oneWordSum_runs (✓ 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.9 (jointWordSum_runs).

$$\forall (b:\mathrm{Bool}),(\forall (rs:\mathrm{List}\mathbb{N}),((\forall r\in rs,(0<r))\to (\forall (r:\mathbb{N}),(\forall (F:(\mathbb{N})\to ((\mathbb{N})\to (\mathbb{R}))),((\forall d,(F0d=0))\to (\mathrm{jointWordSum}(\mathrm{runWord}b((r+1)::rs))F=F(r+2)((r+2).\mathrm{choose}2)+(rs.\mathrm{map}(\mathrm{fun}t\mapsto (F(t+1)((r+1)\cdot (t+1))))).\mathrm{sum}+((r:\mathbb{R})+1+rs.\mathrm{sum}-rs.\mathrm{length})\cdot F1(r+1)+F1(r+1+\mathrm{leadingWeight}rs)))))))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/BinaryRunSupersequenceCounts.jointWordSum_runs (✓ 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 joint one-supersequence count distribution is determined by the first run length, the later run lengths, and the leading singleton chain. The function F is arbitrary subject to F 0 d = 0.

References

• Truth anchor: D5/S3/Entropy/BinaryRunSupersequenceCounts.jointWordSum
• Truth anchor: D5/S3/Entropy/BinaryRunSupersequenceCounts.jointWordSum_runs
• Truth anchor: D5/S3/Entropy/BinaryRunSupersequenceCounts.leadingWeight
• Truth anchor: D5/S3/Entropy/BinaryRunSupersequenceCounts.oneWordSum
• Truth anchor: D5/S3/Entropy/BinaryRunSupersequenceCounts.oneWordSum_runs
• Truth anchor: D5/S3/Entropy/BinaryRunSupersequenceCounts.wordSum
• Truth anchor: D5/S3/Entropy/BinaryRunSupersequenceCounts.wordSum_add
• Truth anchor: D5/S3/Entropy/BinaryRunSupersequenceCounts.wordSum_congr
• Truth anchor: D5/S3/Entropy/BinaryRunSupersequenceCounts.wordSum_succ
• Dependency: D5/S1/Words/Complexity/VivionBinomialConverseFails
• Dependency: D5/S1/Words/TwoDeletionRunDecks
• Dependency: D5/S3/Entropy/AlternatingTwoDeletionCounts