AlternatingTwoDeletionCounts

Abstract

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

Theorem 1.1 (sum_binary_real_succ).

$$\forall (n:\mathbb{N}),(\forall (F:(((\mathrm{Fin}(n+1))\to (\mathrm{Bool})))\to (\mathbb{R})),(\forall (b:\mathrm{Bool}),((\sum _x(Fx))=(\sum _{x:\mathrm{Fin}n\to \mathrm{Bool}}(F(\mathrm{Fin}.\mathrm{cons}bx)))+\sum _{x:\mathrm{Fin}n\to \mathrm{Bool}}(F(\mathrm{Fin}.\mathrm{cons}(!b)x)))))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/AlternatingTwoDeletionCounts.sum_binary_real_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.

Definition 1.2 (altList).

$$\forall (b:\mathrm{Bool}),(\forall (n:\mathbb{N}),(\mathrm{altList}bn=(\mathrm{List}.\mathrm{ofFn}(\mathrm{fun}i:\mathrm{Fin}n\mapsto (D5.S3.\mathrm{Observer}.\mathrm{ProbabilisticClosure}.\mathrm{AdaptiveMarkerStoppingTails}.\mathrm{alternatingBit}b\mathrm{val}\left(i\right))))))$$

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

Theorem 1.3 (altList_zero).

$$\forall (b:\mathrm{Bool}),(\mathrm{altList}b0=[])$$

Proof. Machine-checked in Lean as D5/S3/Entropy/AlternatingTwoDeletionCounts.altList_zero (✓ 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 (altList_succ).

$$\forall (b:\mathrm{Bool}),(\forall (n:\mathbb{N}),(\mathrm{altList}b(n+1)=b::\mathrm{altList}(!b)n))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/AlternatingTwoDeletionCounts.altList_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.5 (count_equal_length).

$$\forall (p:\mathrm{List}\mathrm{Bool}),(\forall (q:\mathrm{List}\mathrm{Bool}),((p.\mathrm{length}=q.\mathrm{length})\to (\mathrm{scatteredCount}pq=\mathrm{if}p=q\mathrm{then}1\mathrm{else}0)))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/AlternatingTwoDeletionCounts.count_equal_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.

Theorem 1.6 (count_alt_cons_same).

$$\forall (b:\mathrm{Bool}),(\forall (m:\mathbb{N}),(\forall (q:\mathrm{List}\mathrm{Bool}),(\mathrm{scatteredCount}(\mathrm{altList}b(m+1))(b::q)=\mathrm{scatteredCount}(\mathrm{altList}b(m+1))q+\mathrm{scatteredCount}(\mathrm{altList}(!b)m)q)))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/AlternatingTwoDeletionCounts.count_alt_cons_same (✓ 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 (count_alt_cons_opposite).

$$\forall (b:\mathrm{Bool}),(\forall (m:\mathbb{N}),(\forall (q:\mathrm{List}\mathrm{Bool}),(\mathrm{scatteredCount}(\mathrm{altList}b(m+1))((!b)::q)=\mathrm{scatteredCount}(\mathrm{altList}b(m+1))q)))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/AlternatingTwoDeletionCounts.count_alt_cons_opposite (✓ 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 (altList_not).

$$\forall (b:\mathrm{Bool}),(\forall (n:\mathbb{N}),(\mathrm{altList}(!b)n=(\mathrm{altList}bn).\mathrm{map}\mathrm{Bool}.\mathrm{not}))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/AlternatingTwoDeletionCounts.altList_not (✓ 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 (ofFn_alternating).

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

Proof. Machine-checked in Lean as D5/S3/Entropy/AlternatingTwoDeletionCounts.ofFn_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.

Theorem 1.10 (count_alt_two).

$$\forall (n:\mathbb{N}),(\forall (b:\mathrm{Bool}),((\mathrm{scatteredCount}(\mathrm{altList}bn)(\mathrm{altList}b(n+2))=n+1)\wedge (\forall p:\mathrm{List}\mathrm{Bool},((p.\mathrm{length}=n)\to ((p\ne \mathrm{altList}bn)\to (\mathrm{scatteredCount}p(\mathrm{altList}b(n+2))\le 1))))))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/AlternatingTwoDeletionCounts.count_alt_two (✓ 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 (sum_one_extra_alt).

$$\forall (m:\mathbb{N}),(\forall (b:\mathrm{Bool}),(\forall (F:(\mathbb{N})\to (\mathbb{R})),((F0=0)\to ((\sum _{y:\mathrm{Fin}(m+1)\to \mathrm{Bool}}(F(\mathrm{scatteredCount}(\mathrm{altList}bm)(\mathrm{List}.\mathrm{ofFn}y))))=2\cdot F1+(m:\mathbb{R})\cdot F2))))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/AlternatingTwoDeletionCounts.sum_one_extra_alt (✓ 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.12 (sum_one_two_joint).

$$\forall (m:\mathbb{N}),((1\le m)\to (\forall (b:\mathrm{Bool}),(\forall (F:(\mathbb{N})\to ((\mathbb{N})\to (\mathbb{R}))),((\forall d,(F0d=0))\to ((\sum _{y:\mathrm{Fin}(m+2)\to \mathrm{Bool}}(F(\mathrm{scatteredCount}(\mathrm{altList}b(m+1))(\mathrm{List}.\mathrm{ofFn}y))(\mathrm{scatteredCount}(\mathrm{altList}(!b)m)(\mathrm{List}.\mathrm{ofFn}y))))=F1(m+1)+F11+F21+(m:\mathbb{R})\cdot F22)))))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/AlternatingTwoDeletionCounts.sum_one_two_joint (✓ 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/S3/Entropy/AlternatingTwoDeletionCounts.altList
• Truth anchor: D5/S3/Entropy/AlternatingTwoDeletionCounts.altList_not
• Truth anchor: D5/S3/Entropy/AlternatingTwoDeletionCounts.altList_succ
• Truth anchor: D5/S3/Entropy/AlternatingTwoDeletionCounts.altList_zero
• Truth anchor: D5/S3/Entropy/AlternatingTwoDeletionCounts.count_alt_cons_opposite
• Truth anchor: D5/S3/Entropy/AlternatingTwoDeletionCounts.count_alt_cons_same
• Truth anchor: D5/S3/Entropy/AlternatingTwoDeletionCounts.count_alt_two
• Truth anchor: D5/S3/Entropy/AlternatingTwoDeletionCounts.count_equal_length
• Truth anchor: D5/S3/Entropy/AlternatingTwoDeletionCounts.ofFn_alternating
• Truth anchor: D5/S3/Entropy/AlternatingTwoDeletionCounts.sum_binary_real_succ
• Truth anchor: D5/S3/Entropy/AlternatingTwoDeletionCounts.sum_one_extra_alt
• Truth anchor: D5/S3/Entropy/AlternatingTwoDeletionCounts.sum_one_two_joint
• Dependency: D5/S1/Words/Complexity/ExactDecks/Growth/ExactDeckCore
• Dependency: D5/S1/Words/Complexity/VivionBinomialConverseFails
• Dependency: D5/S3/Observer/ProbabilisticClosure/AdaptiveMarkerStoppingTails