TwoDeletionRunEntropyBounds

Abstract

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

Definition 1.1 (f).

$$\forall (x:\mathbb{R}),(fx=(x\cdot \mathrm{Real}.\mathrm{logb}2x))$$

Formalization. D5/S3/Entropy/TwoDeletionRunEntropyBounds.f (✓ 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 weighted embedding term is t times its base-two logarithm; its value at zero is zero.

Theorem 1.2 (logb_three_bounds).

$$(3/2)<\mathrm{Real}.\mathrm{logb}23\wedge \mathrm{Real}.\mathrm{logb}23<(5/3)$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionRunEntropyBounds.logb_three_bounds (✓ 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 base-two logarithm of three lies strictly between three halves and five thirds.

Definition 1.3 (longRuns).

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

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

Definition 1.4 (bridgeWeightsAux).

$$\begin{array}{r}\forall (prev:\mathbb{N}),(\forall (singles:\mathbb{N}),(\mathrm{bridgeWeightsAux}prevsingles[]=([prev+singles+1])))\\ \forall (prev:\mathbb{N}),(\forall (singles:\mathbb{N}),(\forall (r:\mathbb{N}),(\forall (rs:\mathrm{List}\mathbb{N}),(\mathrm{bridgeWeightsAux}prevsingles(r::rs)=(\mathrm{if}r=1\mathrm{then}\mathrm{bridgeWeightsAux}prev(singles+1)rs\mathrm{else}(prev+r+singles+1)::\mathrm{bridgeWeightsAux}r0rs)))))\end{array}$$

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

Definition 1.5 (runDefect).

$$\forall (rs:\mathrm{List}\mathbb{N}),(\mathrm{runDefect}rs=((rs.\mathrm{map}(\mathrm{fun}r\mapsto (r-1))).\mathrm{sum}))$$

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

Theorem 1.6 (f_zero).

$$f0=0$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionRunEntropyBounds.f_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.7 (f_one).

$$f1=0$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionRunEntropyBounds.f_one (✓ 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 (f_two).

$$f2=2$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionRunEntropyBounds.f_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.9 (f_mul).

$$\forall (a:\mathbb{R}),(\forall (b:\mathbb{R}),(f(a\cdot b)=b\cdot fa+a\cdot fb))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionRunEntropyBounds.f_mul (✓ 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 (Hrun).

$$\forall (m:\mathbb{R}),(\forall (r:\mathbb{R}),(\mathrm{Hrun}mr=(f((r+1)\cdot (r+2)/2)+(2\cdot m-r)\cdot f(r+1))))$$

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

Theorem 1.11 (longRuns_bounds).

$$\forall (rs:\mathrm{List}\mathbb{N}),((\forall r\in rs,(0<r))\to (((\forall r\in \mathrm{longRuns}rs,((2\le r)\wedge (r\le rs.\mathrm{sum}))))\wedge ((\mathrm{longRuns}rs).\mathrm{sum}\le rs.\mathrm{sum})))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionRunEntropyBounds.longRuns_bounds (✓ 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 (longRuns_nonempty_of_defect).

$$\forall (rs:\mathrm{List}\mathbb{N}),((\forall r\in rs,(0<r))\to ((0<\mathrm{runDefect}rs)\to (\mathrm{longRuns}rs\ne [])))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionRunEntropyBounds.longRuns_nonempty_of_defect (✓ 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 (runDefect_eq).

$$\forall (rs:\mathrm{List}\mathbb{N}),((\forall r\in rs,(0<r))\to (\mathrm{runDefect}rs+rs.\mathrm{length}=rs.\mathrm{sum}))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionRunEntropyBounds.runDefect_eq (✓ 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.14 (runPhiInsertion).

$$\forall (rs:\mathrm{List}\mathbb{N}),(\mathrm{runPhiInsertion}rs=(((\mathrm{collisionWeights}rs).\mathrm{map}(\mathrm{fun}n:\mathbb{N}\mapsto (fn))).\mathrm{sum}))$$

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

Theorem 1.15 (same_run_phi_formula).

$$\forall (rs:\mathrm{List}\mathbb{N}),(((\mathrm{sameRunWeights}rs).\mathrm{map}(\mathrm{fun}n:\mathbb{N}\mapsto (fn))).\mathrm{sum}=(rs.\mathrm{map}(\mathrm{fun}r\mapsto (f(r.\mathrm{choose}2)))).\mathrm{sum})$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionRunEntropyBounds.same_run_phi_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.16 (bridgeWeights_constraints).

$$\forall (rs:\mathrm{List}\mathbb{N}),((\forall r\in rs,(0<r))\to (((\mathrm{bridgeWeightsAux}00rs).\mathrm{length}=(\mathrm{longRuns}rs).\mathrm{length}+1)\wedge ((\mathrm{bridgeWeightsAux}00rs).\mathrm{sum}=rs.\mathrm{sum}+(\mathrm{longRuns}rs).\mathrm{sum}+(\mathrm{longRuns}rs).\mathrm{length}+1)))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionRunEntropyBounds.bridgeWeights_constraints (✓ 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 (deletionRunScore).

$$\forall (rs:\mathrm{List}\mathbb{N}),(\mathrm{deletionRunScore}rs=(((rs.\mathrm{sum}-(\mathrm{longRuns}rs).\mathrm{sum}:\mathbb{N}):\mathbb{R})\cdot (f3+4\cdot rs.\mathrm{sum})+((\mathrm{longRuns}rs).\mathrm{map}(\mathrm{fun}r:\mathbb{N}\mapsto (\mathrm{Hrun}(rs.\mathrm{sum}:\mathbb{R})(r:\mathbb{R})))).\mathrm{sum}+((\mathrm{bridgeWeightsAux}00rs).\mathrm{map}(\mathrm{fun}r:\mathbb{N}\mapsto (fr))).\mathrm{sum}))$$

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

Theorem 1.18 (large_insertion_comparison).

$$\forall (n:\mathbb{N}),(\forall (d:\mathbb{N}),(\forall (P:\mathbb{R}),((9\le n)\to ((1\le d)\to ((2\cdot ((n:\mathbb{R})-2)\cdot d\le P)\to (((2\cdot d<n-5)\to (f(n-1:\mathbb{N})+(d:\mathbb{R})\cdot ((n:\mathbb{R})-2\cdot d-5)\le P))\to (f(n-1:\mathbb{N})<P)))))))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionRunEntropyBounds.large_insertion_comparison (✓ 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.19 (f_add_super_nat).

$$\forall (a:\mathbb{N}),(\forall (b:\mathbb{N}),(fa+fb\le f((a+b:\mathbb{N}))))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionRunEntropyBounds.f_add_super_nat (✓ 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.20 (run_fine_insertion_bound).

$$\forall (rs:\mathrm{List}\mathbb{N}),((\forall r\in rs,(0<r))\to ((3\le rs.\mathrm{length})\to (f(rs.\mathrm{sum}-1:\mathbb{N})+(\mathrm{runDefect}rs:\mathbb{R})\cdot ((rs.\mathrm{sum}:\mathbb{R})-2\cdot \mathrm{runDefect}rs-5)\le \mathrm{runPhiInsertion}rs)))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionRunEntropyBounds.run_fine_insertion_bound (✓ 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.21 (deletion_abstract_bridge_gap).

$$\forall (m:\mathbb{N}),(\forall (us:\mathrm{List}\mathbb{N}),(\forall (ws:\mathrm{List}\mathbb{N}),((2\le m)\to ((us\ne [])\to ((\forall u\in us,((2\le u)\wedge (u\le m)))\to ((us.\mathrm{sum}\le m)\to ((ws.\mathrm{length}=us.\mathrm{length}+1)\to ((m+us.\mathrm{sum}+us.\mathrm{length}+1\le ws.\mathrm{sum})\to (4\cdot (m:\mathbb{R}{)}^2+3\cdot m\cdot \mathrm{Real}.\mathrm{logb}23+f((m:\mathbb{R})+1)<((m-us.\mathrm{sum}:\mathbb{N}):\mathbb{R})\cdot (f3+4\cdot m)+(us.\mathrm{map}(\mathrm{fun}u:\mathbb{N}\mapsto (\mathrm{Hrun}(m:\mathbb{R})(u:\mathbb{R})))).\mathrm{sum}+(ws.\mathrm{map}(\mathrm{fun}n:\mathbb{N}\mapsto (fn))).\mathrm{sum})))))))))$$

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

A nonempty family of long runs and the associated bridge constraints force a strict increase above the alternating deletion score.

Theorem 1.22 (run_coarse_insertion_bound).

$$\forall (rs:\mathrm{List}\mathbb{N}),((\forall r\in rs,(0<r))\to (2\cdot ((rs.\mathrm{sum}:\mathbb{R})-2)\cdot ((rs.\mathrm{sum}:\mathbb{R})-rs.\mathrm{length})\le \mathrm{runPhiInsertion}rs))$$

Proof. Machine-checked in Lean as D5/S3/Entropy/TwoDeletionRunEntropyBounds.run_coarse_insertion_bound (✓ 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/TwoDeletionRunEntropyBounds.Hrun
• Truth anchor: D5/S3/Entropy/TwoDeletionRunEntropyBounds.bridgeWeightsAux
• Truth anchor: D5/S3/Entropy/TwoDeletionRunEntropyBounds.bridgeWeights_constraints
• Truth anchor: D5/S3/Entropy/TwoDeletionRunEntropyBounds.deletionRunScore
• Truth anchor: D5/S3/Entropy/TwoDeletionRunEntropyBounds.deletion_abstract_bridge_gap
• Truth anchor: D5/S3/Entropy/TwoDeletionRunEntropyBounds.f
• Truth anchor: D5/S3/Entropy/TwoDeletionRunEntropyBounds.f_add_super_nat
• Truth anchor: D5/S3/Entropy/TwoDeletionRunEntropyBounds.f_mul
• Truth anchor: D5/S3/Entropy/TwoDeletionRunEntropyBounds.f_one
• Truth anchor: D5/S3/Entropy/TwoDeletionRunEntropyBounds.f_two
• Truth anchor: D5/S3/Entropy/TwoDeletionRunEntropyBounds.f_zero
• Truth anchor: D5/S3/Entropy/TwoDeletionRunEntropyBounds.large_insertion_comparison
• Truth anchor: D5/S3/Entropy/TwoDeletionRunEntropyBounds.logb_three_bounds
• Truth anchor: D5/S3/Entropy/TwoDeletionRunEntropyBounds.longRuns
• Truth anchor: D5/S3/Entropy/TwoDeletionRunEntropyBounds.longRuns_bounds
• Truth anchor: D5/S3/Entropy/TwoDeletionRunEntropyBounds.longRuns_nonempty_of_defect
• Truth anchor: D5/S3/Entropy/TwoDeletionRunEntropyBounds.runDefect
• Truth anchor: D5/S3/Entropy/TwoDeletionRunEntropyBounds.runDefect_eq
• Truth anchor: D5/S3/Entropy/TwoDeletionRunEntropyBounds.runPhiInsertion
• Truth anchor: D5/S3/Entropy/TwoDeletionRunEntropyBounds.run_coarse_insertion_bound
• Truth anchor: D5/S3/Entropy/TwoDeletionRunEntropyBounds.run_fine_insertion_bound
• Truth anchor: D5/S3/Entropy/TwoDeletionRunEntropyBounds.same_run_phi_formula
• Dependency: D5/S1/Words/TwoDeletionRunDecks