SinghviMaxInputEntropy

Abstract

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

Definition 1.1 (claim).

$$\mathrm{claim}⟺(\mathrm{let}\mathrm{deletionPosterior}:=(\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{let}\mathrm{insertionPosterior}:=(\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}))));(((\forall m:\mathbb{N},((1\le m)\to (\forall y:\mathrm{Fin}m\to \mathrm{Bool},(((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{deletionPosterior}y)/\mathrm{Real}.\log 2)\le (D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{deletionPosterior}((\mathrm{fun}i:\mathrm{Fin}m\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1)))))/\mathrm{Real}.\log 2))\wedge ((((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{deletionPosterior}y)/\mathrm{Real}.\log 2)=(D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{deletionPosterior}((\mathrm{fun}i:\mathrm{Fin}m\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1)))))/\mathrm{Real}.\log 2))⟺((y=(\mathrm{fun}i:\mathrm{Fin}m\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1))))\vee (y=\mathrm{fun}i\mapsto (!(\mathrm{fun}i:\mathrm{Fin}m\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1)))i))))))))))\wedge (((\forall m:\mathbb{N},((1\le m)\to ((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{deletionPosterior}((\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+1)\cdot \mathrm{Real}.\mathrm{logb}2(m+1))/(4\cdot (m+2).\mathrm{choose}2)))))\wedge (((\forall m:\mathbb{N},((3\le m)\to (\forall y:\mathrm{Fin}(m+2)\to \mathrm{Bool},(((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}y)/\mathrm{Real}.\log 2)\le (D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}((\mathrm{fun}i:\mathrm{Fin}(m+2)\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1)))))/\mathrm{Real}.\log 2))\wedge ((((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}y)/\mathrm{Real}.\log 2)=(D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}((\mathrm{fun}i:\mathrm{Fin}(m+2)\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1)))))/\mathrm{Real}.\log 2))⟺((y=(\mathrm{fun}i:\mathrm{Fin}(m+2)\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1))))\vee (y=\mathrm{fun}i\mapsto (!(\mathrm{fun}i:\mathrm{Fin}(m+2)\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1)))i))))))))))\wedge (((\forall m:\mathbb{N},((3\le m)\to ((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}((\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+1)\cdot \mathrm{Real}.\mathrm{logb}2(m+1)/(m+2).\mathrm{choose}2))))\wedge (((\forall y:\mathrm{Fin}2\to \mathrm{Bool},((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}(m:=0)y)/\mathrm{Real}.\log 2)=0)))\wedge (((\forall y:\mathrm{Fin}3\to \mathrm{Bool},(((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}(m:=1)y)/\mathrm{Real}.\log 2)\le (D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}((\mathrm{fun}i:\mathrm{Fin}3\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1)))))/\mathrm{Real}.\log 2))\wedge ((((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}(m:=1)y)/\mathrm{Real}.\log 2)=(D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}((\mathrm{fun}i:\mathrm{Fin}3\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1)))))/\mathrm{Real}.\log 2))⟺(\exists ij:\mathrm{Fin}3,(yi\ne yj)))))))\wedge ((\forall y:\mathrm{Fin}4\to \mathrm{Bool},(((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}(m:=2)y)/\mathrm{Real}.\log 2)\le (D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}(m:=2)![\mathrm{false},\mathrm{true},\mathrm{true},\mathrm{false}])/\mathrm{Real}.\log 2))\wedge ((((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}(m:=2)y)/\mathrm{Real}.\log 2)=(D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}(m:=2)![\mathrm{false},\mathrm{true},\mathrm{true},\mathrm{false}])/\mathrm{Real}.\log 2))⟺((y=![\mathrm{false},\mathrm{true},\mathrm{true},\mathrm{false}])\vee (y=![\mathrm{true},\mathrm{false},\mathrm{false},\mathrm{true}])))))))))))))))$$

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

Section VII-A, PDF p. 16: “Maximal Input Entropy for k = 2. While we provide a complete characterization of the sequences that minimize input entropy, the precise identification of the sequences that maximize input entropy for the 2-deletion and 2-insertion channels is still unresolved. Determining these sequences and the associated maximal entropy values remains an important open direction.” Binary words are functions Fin m to Bool, with false equal to 0. The seven clauses give both maximizing families, both maximal entropies, and the three insertion cases of received length two, three, and four. Received insertion length is m + 2 and input length is m. All logarithms are in bits.

Theorem 1.2 (result).

$$\mathrm{let}\mathrm{deletionPosterior}:=(\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{let}\mathrm{insertionPosterior}:=(\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}))));(((\forall m:\mathbb{N},((1\le m)\to (\forall y:\mathrm{Fin}m\to \mathrm{Bool},(((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{deletionPosterior}y)/\mathrm{Real}.\log 2)\le (D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{deletionPosterior}((\mathrm{fun}i:\mathrm{Fin}m\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1)))))/\mathrm{Real}.\log 2))\wedge ((((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{deletionPosterior}y)/\mathrm{Real}.\log 2)=(D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{deletionPosterior}((\mathrm{fun}i:\mathrm{Fin}m\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1)))))/\mathrm{Real}.\log 2))⟺((y=(\mathrm{fun}i:\mathrm{Fin}m\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1))))\vee (y=\mathrm{fun}i\mapsto (!(\mathrm{fun}i:\mathrm{Fin}m\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1)))i))))))))))\wedge (((\forall m:\mathbb{N},((1\le m)\to ((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{deletionPosterior}((\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+1)\cdot \mathrm{Real}.\mathrm{logb}2(m+1))/(4\cdot (m+2).\mathrm{choose}2)))))\wedge (((\forall m:\mathbb{N},((3\le m)\to (\forall y:\mathrm{Fin}(m+2)\to \mathrm{Bool},(((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}y)/\mathrm{Real}.\log 2)\le (D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}((\mathrm{fun}i:\mathrm{Fin}(m+2)\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1)))))/\mathrm{Real}.\log 2))\wedge ((((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}y)/\mathrm{Real}.\log 2)=(D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}((\mathrm{fun}i:\mathrm{Fin}(m+2)\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1)))))/\mathrm{Real}.\log 2))⟺((y=(\mathrm{fun}i:\mathrm{Fin}(m+2)\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1))))\vee (y=\mathrm{fun}i\mapsto (!(\mathrm{fun}i:\mathrm{Fin}(m+2)\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1)))i))))))))))\wedge (((\forall m:\mathbb{N},((3\le m)\to ((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}((\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+1)\cdot \mathrm{Real}.\mathrm{logb}2(m+1)/(m+2).\mathrm{choose}2))))\wedge (((\forall y:\mathrm{Fin}2\to \mathrm{Bool},((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}(m:=0)y)/\mathrm{Real}.\log 2)=0)))\wedge (((\forall y:\mathrm{Fin}3\to \mathrm{Bool},(((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}(m:=1)y)/\mathrm{Real}.\log 2)\le (D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}((\mathrm{fun}i:\mathrm{Fin}3\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1)))))/\mathrm{Real}.\log 2))\wedge ((((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}(m:=1)y)/\mathrm{Real}.\log 2)=(D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}((\mathrm{fun}i:\mathrm{Fin}3\mapsto (\mathrm{decide}(\mathrm{val}\left(i\right)\mathrm{mod}2=1)))))/\mathrm{Real}.\log 2))⟺(\exists ij:\mathrm{Fin}3,(yi\ne yj)))))))\wedge ((\forall y:\mathrm{Fin}4\to \mathrm{Bool},(((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}(m:=2)y)/\mathrm{Real}.\log 2)\le (D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}(m:=2)![\mathrm{false},\mathrm{true},\mathrm{true},\mathrm{false}])/\mathrm{Real}.\log 2))\wedge ((((D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}(m:=2)y)/\mathrm{Real}.\log 2)=(D5.S3.\mathrm{Entropy}.\mathrm{MaxEntropy}.\mathrm{shannonEntropy}(\mathrm{insertionPosterior}(m:=2)![\mathrm{false},\mathrm{true},\mathrm{true},\mathrm{false}])/\mathrm{Real}.\log 2))⟺((y=![\mathrm{false},\mathrm{true},\mathrm{true},\mathrm{false}])\vee (y=![\mathrm{true},\mathrm{false},\mathrm{false},\mathrm{true}]))))))))))))))$$

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

Resolves. Problems/singhvi-sabary-barlev-yaakobi-2024-deletion-channel-max-input-entropy (proved) by D5/S3/Entropy/SinghviMaxInputEntropy.result.

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.

Alternating words and their complements are exactly the deletion maximizers at every positive received length and the insertion maximizers from received length five onward. At length three all nonconstant words maximize, and at length four precisely 0110 and 1001 maximize. Exact joint supersequence counts give the deletion run expression; strict run estimates and Jensen inequalities give its unique minimizers. Grouping deletion masks and finite small cases give the insertion comparison.

References

• Truth anchor: D5/S3/Entropy/SinghviMaxInputEntropy.claim
• Truth anchor: D5/S3/Entropy/SinghviMaxInputEntropy.result
• Dependency: D5/S1/Words/AssociatedMersenne/RunTupleBijection
• Dependency: D5/S1/Words/Complexity/VivionBinomialConverseFails
• Dependency: D5/S1/Words/TwoDeletionRunDecks
• Dependency: D5/S3/Entropy/AlternatingTwoDeletionCounts
• Dependency: D5/S3/Entropy/DeletionChannelEntropyOrdering
• Dependency: D5/S3/Entropy/MaxEntropy
• Dependency: D5/S3/Entropy/TwoDeletionChannelEntropy
• Dependency: D5/S3/Entropy/TwoDeletionRunEntropyBounds