TwoDeletionChannelEntropy

Abstract

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

Theorem 1.1 (deletion_total).

$$\forall (mn:\mathbb{N})(x:\mathrm{Fin}m\to \mathrm{Bool}),\sum _{y:\mathrm{Fin}n\to \mathrm{Bool}}\mathrm{embeddings}xy=\mathrm{Nat}.\mathrm{choose}nm\cdot 2^{n-m}$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionChannelEntropy.deletion_total (✓ 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.

For every pair of natural lengths m and n and every binary word x of length m, the sum of its index-embedding counts over all binary words of length n is C(n,m) times 2^(n-m), independently of x. This is the exact general total mass; deletion_total_two and normalized_deletion_entropy consume the same declaration.

Theorem 1.2 (empty_embeddings).

$$\forall (n:\mathbb{N}),(\forall (y:(\mathrm{Fin}n)\to (\mathrm{Bool})),(\mathrm{embeddings}(\mathrm{fun}i:\mathrm{Fin}0\mapsto (\mathrm{Fin}.elim0i))y=1))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionChannelEntropy.empty_embeddings (✓ 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.3 (phi).

$$\forall (\iota :\mathrm{Type}),([\mathrm{Fintype}\iota ]\to (\forall (c:(\iota )\to (\mathbb{N})),(\mathrm{phi}(\iota :=\iota )c=(\sum _i((ci:\mathbb{R})\cdot \mathrm{Real}.\mathrm{logb}2(ci))))))$$

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

Theorem 1.4 (ofFn_complement_alternating).

$$\forall (n:\mathbb{N}),(\mathrm{List}.\mathrm{ofFn}(\mathrm{fun}i\mapsto (!(\mathrm{fun}i:\mathrm{Fin}n\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1)))i))=\mathrm{altList}\mathrm{true}n)$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionChannelEntropy.ofFn_complement_alternating (✓ 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.5 (RunDeletionCountingLowerBound).

$$\mathrm{RunDeletionCountingLowerBound}=(\forall (m:\mathbb{N})(y:(\mathrm{Fin}m)\to (\mathrm{Bool}))(b:\mathrm{Bool})(rs:\mathrm{List}\mathbb{N}),(((\forall r\in rs,(0<r)))\to ((\mathrm{List}.\mathrm{ofFn}y=\mathrm{runWord}brs)\to (\mathrm{deletionRunScore}rs\le \mathrm{phi}(\mathrm{fun}x:\mathrm{Fin}(m+2)\to \mathrm{Bool}\mapsto (\mathrm{embeddings}yx))))))$$

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

Theorem 1.6 (alternating_insertion_phi).

$$\forall (m:\mathbb{N}),(\mathrm{phi}(\mathrm{fun}x:\mathrm{Fin}m\to \mathrm{Bool}\mapsto (\mathrm{embeddings}x((\mathrm{fun}i:\mathrm{Fin}(m+2)\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1))))))=f(m+1))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionChannelEntropy.alternating_insertion_phi (✓ 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.7 (alternating_deletion_phi).

$$\forall (m:\mathbb{N}),((1\le m)\to (\mathrm{phi}(\mathrm{fun}x:\mathrm{Fin}(m+2)\to \mathrm{Bool}\mapsto (\mathrm{embeddings}((\mathrm{fun}i:\mathrm{Fin}m\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1))))x))=4\cdot (m:\mathbb{R}{)}^2+3\cdot m\cdot \mathrm{Real}.\mathrm{logb}23+((m:\mathbb{R})+1)\cdot \mathrm{Real}.\mathrm{logb}2((m:\mathbb{R})+1)))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionChannelEntropy.alternating_deletion_phi (✓ 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.8 (insertion_entropy_formula).

$$\forall (m:\mathbb{N}),(\forall (y:(\mathrm{Fin}(m+2))\to (\mathrm{Bool})),((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}((\mathrm{fun}\{m:\mathbb{N}\}(y:(\mathrm{Fin}(m+2))\to (\mathrm{Bool}))(x:(\mathrm{Fin}m)\to (\mathrm{Bool}))\mapsto ((\mathrm{embeddings}xy:\mathbb{R})/\sum _{x^{\prime }:\mathrm{Fin}m\to \mathrm{Bool}}((\mathrm{embeddings}{x}^{\prime }y:\mathbb{R}))))y)/\mathrm{Real}.\log 2)=\mathrm{Real}.\mathrm{logb}2((m+2).\mathrm{choose}m)-\mathrm{phi}(\mathrm{fun}x:\mathrm{Fin}m\to \mathrm{Bool}\mapsto (\mathrm{embeddings}xy))/(m+2).\mathrm{choose}m))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionChannelEntropy.insertion_entropy_formula (✓ 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.

For m ≥ 2, this is Lemma 3 with n = m and k = 2. The cases m = 0 and m = 1 extend the identity to the two shorter input lengths.

Theorem 1.9 (alternating_insertion_closed_form).

$$\forall (m:\mathbb{N}),((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}((\mathrm{fun}\{m:\mathbb{N}\}(y:(\mathrm{Fin}(m+2))\to (\mathrm{Bool}))(x:(\mathrm{Fin}m)\to (\mathrm{Bool}))\mapsto ((\mathrm{embeddings}xy:\mathbb{R})/\sum _{x^{\prime }:\mathrm{Fin}m\to \mathrm{Bool}}((\mathrm{embeddings}{x}^{\prime }y:\mathbb{R}))))((\mathrm{fun}i:\mathrm{Fin}(m+2)\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1)))))/\mathrm{Real}.\log 2)=\mathrm{Real}.\mathrm{logb}2((m+2).\mathrm{choose}2)-((m:\mathbb{R})+1)\cdot \mathrm{Real}.\mathrm{logb}2((m:\mathbb{R})+1)/(m+2).\mathrm{choose}2)$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionChannelEntropy.alternating_insertion_closed_form (✓ 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.10 (actual_run_insertion_lower).

$$\forall (m:\mathbb{N}),(\forall (y:(\mathrm{Fin}(m+2))\to (\mathrm{Bool})),(\forall (b:\mathrm{Bool}),(\forall (rs:\mathrm{List}\mathbb{N}),((\forall r\in rs,(0<r))\to ((\mathrm{List}.\mathrm{ofFn}y=\mathrm{runWord}brs)\to (\mathrm{runPhiInsertion}rs\le \mathrm{phi}(\mathrm{fun}x:\mathrm{Fin}m\to \mathrm{Bool}\mapsto (\mathrm{embeddings}xy))))))))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionChannelEntropy.actual_run_insertion_lower (✓ 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.11 (deletion_entropy_formula).

$$\forall (m:\mathbb{N}),(\forall (y:(\mathrm{Fin}m)\to (\mathrm{Bool})),((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}((\mathrm{fun}\{m:\mathbb{N}\}(y:(\mathrm{Fin}m)\to (\mathrm{Bool}))(x:(\mathrm{Fin}(m+2))\to (\mathrm{Bool}))\mapsto ((\mathrm{embeddings}yx:\mathbb{R})/\sum _{x^{\prime }:\mathrm{Fin}(m+2)\to \mathrm{Bool}}((\mathrm{embeddings}y{x}^{\prime }:\mathbb{R}))))y)/\mathrm{Real}.\log 2)=\mathrm{Real}.\mathrm{logb}2(4\cdot (m+2).\mathrm{choose}2)-\mathrm{phi}(\mathrm{fun}x:\mathrm{Fin}(m+2)\to \mathrm{Bool}\mapsto (\mathrm{embeddings}yx))/(4\cdot (m+2).\mathrm{choose}2)))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionChannelEntropy.deletion_entropy_formula (✓ std3). ∎

Citation. 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.12 (insertion_entropy_product_formula).

$$\forall (m:\mathbb{N}),(\forall (y:(\mathrm{Fin}(m+2))\to (\mathrm{Bool})),((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}((\mathrm{fun}\{m:\mathbb{N}\}(y:(\mathrm{Fin}(m+2))\to (\mathrm{Bool}))(x:(\mathrm{Fin}m)\to (\mathrm{Bool}))\mapsto ((\mathrm{embeddings}xy:\mathbb{R})/\sum _{x^{\prime }:\mathrm{Fin}m\to \mathrm{Bool}}((\mathrm{embeddings}{x}^{\prime }y:\mathbb{R}))))y)/\mathrm{Real}.\log 2)=\mathrm{Real}.\mathrm{logb}2((m+2).\mathrm{choose}m)-\mathrm{Real}.\mathrm{logb}2((\prod _i((((\mathrm{fun}x:\mathrm{Fin}m\to \mathrm{Bool}\mapsto (\mathrm{embeddings}xy)))i{)}^{(((\mathrm{fun}x:\mathrm{Fin}m\to \mathrm{Bool}\mapsto (\mathrm{embeddings}xy)))i)}:\mathbb{N})))/(m+2).\mathrm{choose}m))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionChannelEntropy.insertion_entropy_product_formula (✓ 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.13 (alternating_deletion_closed_form).

$$\forall (m:\mathbb{N}),((1\le m)\to ((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}((\mathrm{fun}\{m:\mathbb{N}\}(y:(\mathrm{Fin}m)\to (\mathrm{Bool}))(x:(\mathrm{Fin}(m+2))\to (\mathrm{Bool}))\mapsto ((\mathrm{embeddings}yx:\mathbb{R})/\sum _{x^{\prime }:\mathrm{Fin}(m+2)\to \mathrm{Bool}}((\mathrm{embeddings}y{x}^{\prime }:\mathbb{R}))))((\mathrm{fun}i:\mathrm{Fin}m\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1)))))/\mathrm{Real}.\log 2)=\mathrm{Real}.\mathrm{logb}2(4\cdot (m+2).\mathrm{choose}2)-(4\cdot (m:\mathbb{R}{)}^2+3\cdot m\cdot \mathrm{Real}.\mathrm{logb}23+((m:\mathbb{R})+1)\cdot \mathrm{Real}.\mathrm{logb}2((m:\mathbb{R})+1))/(4\cdot (m+2).\mathrm{choose}2)))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionChannelEntropy.alternating_deletion_closed_form (✓ 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.14 (actual_run_deletion_lower).

$$\forall (m:\mathbb{N})(y:(\mathrm{Fin}m)\to (\mathrm{Bool}))(b:\mathrm{Bool})(rs:\mathrm{List}\mathbb{N}),(((\forall r\in rs,(0<r)))\to ((\mathrm{List}.\mathrm{ofFn}y=\mathrm{runWord}brs)\to (\mathrm{deletionRunScore}rs\le \mathrm{phi}(\mathrm{fun}x:\mathrm{Fin}(m+2)\to \mathrm{Bool}\mapsto (\mathrm{embeddings}yx)))))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionChannelEntropy.actual_run_deletion_lower (✓ 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.

Every positive run profile of a received word gives a lower bound on its actual weighted embedding sum.

References

• Truth anchor: D5/S3/Entropy/TwoDeletionChannelEntropy.RunDeletionCountingLowerBound
• Truth anchor: D5/S3/Entropy/TwoDeletionChannelEntropy.actual_run_deletion_lower
• Truth anchor: D5/S3/Entropy/TwoDeletionChannelEntropy.actual_run_insertion_lower
• Truth anchor: D5/S3/Entropy/TwoDeletionChannelEntropy.alternating_deletion_closed_form
• Truth anchor: D5/S3/Entropy/TwoDeletionChannelEntropy.alternating_deletion_phi
• Truth anchor: D5/S3/Entropy/TwoDeletionChannelEntropy.alternating_insertion_closed_form
• Truth anchor: D5/S3/Entropy/TwoDeletionChannelEntropy.alternating_insertion_phi
• Truth anchor: D5/S3/Entropy/TwoDeletionChannelEntropy.deletion_entropy_formula
• Truth anchor: D5/S3/Entropy/TwoDeletionChannelEntropy.deletion_total
• Truth anchor: D5/S3/Entropy/TwoDeletionChannelEntropy.empty_embeddings
• Truth anchor: D5/S3/Entropy/TwoDeletionChannelEntropy.insertion_entropy_formula
• Truth anchor: D5/S3/Entropy/TwoDeletionChannelEntropy.insertion_entropy_product_formula
• Truth anchor: D5/S3/Entropy/TwoDeletionChannelEntropy.ofFn_complement_alternating
• Truth anchor: D5/S3/Entropy/TwoDeletionChannelEntropy.phi
• Dependency: D5/S0/Certificates/Hypergraphs/OrientationEntropyBalance
• Dependency: D5/S1/Words/Complexity/ExactDecks/Growth/ExactDeckCore
• Dependency: D5/S1/Words/Complexity/VivionBinomialConverseFails
• Dependency: D5/S1/Words/TwoDeletionRunDecks
• Dependency: D5/S3/Arith/FibonacciAtomic/Observer/CommonPredictionWordCounts
• Dependency: D5/S3/Combinatorics/Graph/DomiRankEntropyRefutation
• Dependency: D5/S3/Entropy/AlternatingTwoDeletionCounts
• Dependency: D5/S3/Entropy/BinaryRunSupersequenceCounts
• Dependency: D5/S3/Entropy/DeletionChannelEntropyOrdering
• Dependency: D5/S3/Entropy/MaxEntropy
• Dependency: D5/S3/Entropy/TwoDeletionRunEntropyBounds