% Oai119-A.tex % A self-contained, single-file manuscript for pdfLaTeX. % % Suggested build commands (not executed here): % pdflatex -interaction=nonstopmode -halt-on-error Oai119-A.tex % pdflatex -interaction=nonstopmode -halt-on-error Oai119-A.tex % % Release: % An exact certificate for all 16 Boolean functions on {-1,1}^2 % at noise correlation rho = 1/2, including equality cases, % explicit strict gaps, and the corresponding Courtade--Kumar % corollary. % % The all-dimensional assertions of Family 119 remain external % claims whose proof interfaces are audited, not imported. \documentclass[11pt]{article} \usepackage[T1]{fontenc} \usepackage[utf8]{inputenc} \usepackage{lmodern} \usepackage[margin=1in]{geometry} \usepackage{amsmath,amssymb,amsthm,mathtools} \usepackage{array,booktabs,longtable,tabularx} \usepackage{enumitem} \usepackage{microtype} \usepackage{url} \usepackage[hidelinks]{hyperref} \setlength{\emergencystretch}{3em} \setlist[enumerate]{topsep=4pt,itemsep=3pt} \setlist[itemize]{topsep=4pt,itemsep=3pt} \Urlmuskip=0mu plus 1mu \allowdisplaybreaks \numberwithin{equation}{section} \newtheorem{theorem}{Theorem}[section] \newtheorem{proposition}[theorem]{Proposition} \newtheorem{lemma}[theorem]{Lemma} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} \newtheorem{claimrecord}[theorem]{External claim record} \newtheorem{specification}[theorem]{Specification} \theoremstyle{remark} \newtheorem{remark}[theorem]{Remark} \newtheorem{example}[theorem]{Example} \newcommand{\R}{\mathbb R} \newcommand{\Q}{\mathbb Q} \newcommand{\N}{\mathbb N} \newcommand{\E}{\mathbb E} \newcommand{\Prob}{\mathbb P} \newcommand{\Var}{\operatorname{Var}} \newcommand{\atanh}{\operatorname{atanh}} \newcommand{\TV}{d_{\mathrm{TV}}} \newcommand{\Isoft}{\mathcal I} \newcommand{\Info}{\operatorname{I}} \newcommand{\Num}{\mathsf N} \newcommand{\Prod}{\mathcal D} \newcommand{\Loss}{\mathcal L} \newcommand{\Gap}{\Gamma} \newcommand{\hbin}{h_2} \newcommand{\id}{\operatorname{id}} \newcommand{\Tr}{\operatorname{Tr}} \newcommand{\ket}[1]{|#1\rangle} \newcommand{\bra}[1]{\langle#1|} \newcommand{\kb}[2]{|#1\rangle\langle#2|} \newcommand{\proj}[1]{\kb{#1}{#1}} \newcommand{\NOTCLOSED}{\texttt{NOT\_CLOSED}} \title{\textbf{Oai119-A}\\ An Exact Finite Certificate for Hellinger Contraction\\ on the Two-Dimensional Discrete Cube\\[3pt] \large Equality, strict gaps, the information corollary,\\ and a seven-stage audit of Family 119} \author{Ngo Cheung} \date{14 October 2026} \begin{document} \maketitle \begin{abstract} We complete the finite-certificate task proposed for Family 119, without assuming either of its all-dimensional contraction claims. For the uniform cube \(\{-1,1\}^2\) and independent symmetric noise of correlation \(1/2\), we give the complete stochastic matrix, classify all sixteen Boolean functions, and prove the Hellinger inequality by exact algebra. Equality holds precisely for the four signed coordinates. Every other Boolean function has Hellinger gap greater than \(27/1000\). For parity the gap lies strictly between \(102/1000\) and \(103/1000\); for the nonconstant biased orbit it lies strictly between \(27/1000\) and \(28/1000\). All comparisons reduce to displayed integer-square inequalities. We prove the classical convexity argument that converts a Hellinger certificate into a Courtade--Kumar certificate. It yields, at the frozen instance, the sharp bound \(1-h_2(1/4)\), the same equality cases, and a mutual-information gap greater than \(1/50\) bit for every nonsigned-coordinate function. The rest of the manuscript freezes the distinct soft-information and Hellinger assertions, audits their proof interfaces, and separates arithmetic certification, sampling, implementation resources, and quantum recovery. The general Family 119 proofs remain unverified here. No quantum-channel, fidelity, gravitational, or spacetime conclusion is claimed. \end{abstract} \tableofcontents \section{Stage 0: objects, normalizations, and claim status} \label{sec:freeze} \subsection{The task completed here} The single new target selected by the plan is an explicit finite Hellinger certificate at one specified dimension and correlation. Theorem~\ref{thm:finite} completes that target for \[ n=2,\qquad \rho=\frac12. \] It covers \emph{every} Boolean function at this frozen instance, not merely a named coordinate and one selected comparison. The all-dimensional soft-information and Hellinger statements are recorded separately below. They are not hypotheses of Theorem~\ref{thm:finite}. Completing one finite instance does not verify either general proof. The finite calculation is elementary and is not represented as a new resolution of the original conjectures. Its contribution is a fully specified, reproducible certificate with explicit gaps and a clearly bounded dependency structure. \subsection{Uniform cube and symmetric product noise} Let \[ \Omega_n=\{-1,1\}^n,\qquad \E u=2^{-n}\sum_{x\in\Omega_n}u(x). \] For \(-1\le\rho\le1\), define \begin{equation} K_\rho(x,y) = \prod_{i=1}^n\frac{1+\rho x_i y_i}{2}, \qquad T_\rho u(y)=\sum_{x\in\Omega_n}K_\rho(y,x)u(x). \label{eq:kernel} \end{equation} The matrix \(K_\rho\) is symmetric and stochastic. In probabilistic terms, \(X\) is uniform and \[ Y_i=X_iZ_i,\qquad \Prob(Z_i=1)=\frac{1+\rho}{2}, \] where the \(Z_i\) are mutually independent and independent of \(X\). Both \(X\) and \(Y\) are uniform. Symmetry gives \[ T_\rho u(Y)=\E[u(X)\mid Y]. \] These are the standard cube-noise conventions \cite{ODonnell,CourtadeKumar2014}. A Boolean function takes values in \(\{-1,1\}\). A soft summary takes values in \([-1,1]\). A signed coordinate is \(f(x)=\sigma x_i\), with \(\sigma\in\{-1,1\}\). \subsection{Three different scalar functions} To avoid the conflicting uses of \(H\) in the source manuscripts, define \begin{align} \ell&=\ln2,\\ h(t)&= -\frac{1+t}{2}\ln\frac{1+t}{2} -\frac{1-t}{2}\ln\frac{1-t}{2}, &&-1\le t\le1,\\ \psi(t)&=\ell-h(t) = \frac{1+t}{2}\ln(1+t) +\frac{1-t}{2}\ln(1-t),\\ H(t)&=\sqrt{1-t^2}. \label{eq:profiles} \end{align} The convention is \(0\ln0=0\). Thus \(h\) is sign entropy in nats, \(\psi\) is its deficit from \(\ell\), and \(H\) is the Hellinger profile. They are not interchangeable. For a soft summary \(u\), put \begin{equation} \Isoft(u)=h(\E u)-\E h(u) =\E\psi(u)-\psi(\E u). \label{eq:softinfo} \end{equation} Binary entropy in bits is \[ \hbin(p)=-p\log_2p-(1-p)\log_2(1-p). \] We write \(\Info_2(A;B)\) for classical mutual information in bits and \(\Info(A;B)=\ell\,\Info_2(A;B)\) for the same quantity in nats. \begin{lemma}[The classical information identity] \label{lem:infoidentity} Given \(u:\Omega_n\to[-1,1]\), construct a sign \(U\) with \[ \Prob(U=b\mid X=x)=\frac{1+b\,u(x)}2, \qquad b\in\{-1,1\}, \] using auxiliary randomness independent of the noise conditional on \(X\). Then \[ \Info(U;X)=\Isoft(u), \qquad \Info(U;Y)=\Isoft(T_\rho u). \] For Boolean \(f\), one may take \(U=f(X)\), and \begin{equation} \Info_2(f(X);Y) = \hbin\!\left(\frac{1+m}{2}\right) - \E\hbin\!\left(\frac{1+T_\rho f}{2}\right), \qquad m=\E f. \label{eq:MI} \end{equation} \end{lemma} \begin{proof} The conditional mean of \(U\) given \(X\) is \(u(X)\), so its conditional entropy is \(\E h(u)\), while its mean is \(\E u\). This proves the first identity. Conditional expectation and the stated conditional independence give \[ \E[U\mid Y] = \E[u(X)\mid Y] = T_\rho u(Y). \] The same entropy calculation proves the second identity. For Boolean \(f\), \(U=f(X)\) has zero conditional entropy given \(X\), and division by \(\ell\) gives \eqref{eq:MI}. \end{proof} No intermediate measurement, quantum observable, or decoding operation occurs in this identity. \subsection{The two general assertions being audited} \begin{claimrecord}[119-01: soft contraction and Boolean refinement] \label{rec:soft} The manuscript \emph{Sharp binary-information contraction on the discrete cube}, dated 24 September 2026, asserts \begin{equation} \Isoft(T_\rho u) \le \psi\!\left(|\rho|\,\psi^{-1}(\Isoft(u))\right) \label{eq:external-soft} \end{equation} for every soft summary on every finite uniform cube. The inverse is the increasing branch from \([0,\ell]\) to \([0,1]\). Soft coordinates attain equality. For Boolean \(f\) of mean \(m\), its \texttt{main:ck} specializes this to \begin{equation} \Info(f(X);Y) \le\psi(|\rho|r_m)\le\psi(|\rho|), \qquad r_m=\psi^{-1}(h(m)). \label{eq:external-refined} \end{equation} The refined upper curve is strictly below the universal curve when \(0<|m|<1\) and \(0<|\rho|\le1\). Its separate \texttt{upgrade:production} asserts a stronger, mean-dependent production bound \cite{OpenAI119I}. \end{claimrecord} \begin{claimrecord}[119-02: arbitrary-bias Hellinger contraction] \label{rec:hellinger} The manuscript \emph{Hellinger contraction with arbitrary Boolean output bias}, also dated 24 September 2026, asserts \begin{equation} H(m)-\E H(T_\rho f)\le1-H(\rho), \qquad m=\E f, \label{eq:external-H} \end{equation} for every Boolean \(f\), every dimension, and every correlation. Signed coordinates attain equality. Its \texttt{cor:ck} derives the ordinary Courtade--Kumar bound from this assertion \cite{OpenAI119II,OpenAI119Implication}. \end{claimrecord} The Courtade--Kumar formulation in bits is \begin{equation} \Info_2(f(X);Y)\le1-\hbin(\varepsilon), \qquad \varepsilon=\frac{1-\rho}{2}. \label{eq:CK} \end{equation} For \(\rho<0\), the same formula is valid because \(\hbin(\varepsilon)=\hbin(1-\varepsilon)\). \begin{remark}[Debugging the relation between the manuscripts] The two papers concern the same noisy Boolean-summary problem, but their displayed general assertions are different. The soft-information theorem includes randomized summaries at fixed initial information. The Hellinger theorem controls a different functional and implies the ordinary Boolean information bound. We do not assert that the two displayed theorems are equivalent, nor that either general proof is a premise of the other. The implication from Hellinger to Courtade--Kumar predates these manuscripts \cite{ABCJN}. Its elementary proof is included in Section~\ref{sec:implication}. \end{remark} \subsection{Lean scope and the inspected target files} The scope note \texttt{lean/docs/119.md} names 119-01 and describes soft contraction, the Boolean refinement, and the selected production inequality \cite{Lean119Scope}. The inspected Comparator challenge files \texttt{CourtadeKumar.lean} and \texttt{SoftChannel204.lean} specify these targets. Their respective principal theorem bodies, \texttt{courtadeKumarAndAttainment} and \texttt{fullMain}, contain \texttt{sorry} \cite{Lean119CK,Lean119Soft}. Thus the inspected target files are not completed proofs of those theorem bodies. This is a statement about the inspected files, not an exhaustive inspection of every possible solution artifact. The Hellinger inequality of 119-02 is not separately specified by these targets. No Lean execution or independent formal verification is asserted here. \section{Stage 1: the five proof interfaces} \label{sec:audit} The following audit supplies elementary identities and identifies the nontrivial universal obligations. Recording an obligation does not discharge it. \subsection{Gate 1: scalar rate and effective amplitude} \begin{lemma}[Scalar profile facts] \label{lem:scalar} The function \(\psi\) is even, continuous on \([-1,1]\), strictly increasing on \([0,1]\), and strictly convex. For \(|r|<1\), \[ \psi'(r)=\atanh r, \qquad \psi''(r)=\frac1{1-r^2}. \] Furthermore, \[ 0\le\Isoft(u)\le h(\E u)\le\ell, \] and \(\Isoft(u)=0\) if and only if \(u\) is constant. Define \(F:[0,\ell)\to[0,\infty)\) by \begin{equation} F(\psi(r))=r\atanh r, \qquad 0\le r<1. \label{eq:F} \end{equation} Then \(F(0)=0\), \(F'(0)=2\), \(F\) is convex, and \(F(s)\ge2s\). \end{lemma} \begin{proof} The derivatives follow by differentiation. The range of \(\psi\) on \([0,1]\) is \([0,\ell]\). Jensen's inequality proves nonnegativity of \(\Isoft\), with equality precisely for constant \(u\), by strict convexity. Its upper bound follows from \(h\ge0\). For \(r>0\), put \(V=\atanh r\). The chain rule gives \[ F'(\psi(r)) = 1+\frac{r}{(1-r^2)V}, \] and \[ F''(\psi(r)) = \frac{(1+r^2)V-r}{(1-r^2)^2V^3}>0, \] because \(V\ge r\). The expansion \(V=r+O(r^3)\) gives \(F'(0)=2\). Convexity and the tangent at zero give \(F(s)\ge2s\). \end{proof} For a soft coordinate \(u(x)=a x_i\), \[ \Isoft(u)=\psi(|a|),\qquad T_\rho u=\rho a x_i,\qquad \Isoft(T_\rho u)=\psi(|\rho a|). \] This checks the asserted equality example directly, without proving the universal upper bound. The scalar parameter \(\psi^{-1}(\Isoft(u))\) is an effective coordinate amplitude. It is not a channel capacity and does not construct an optimizer over arbitrary summary tables. \subsection{The mean-dependent production profile} To state the production claim precisely, let \[ S(s)=F(s)-2s\quad(0\le s<\ell), \qquad S(s)=0\quad(s<0). \] For \(|m|<1\) and \(0\le I0\), and \[ 00\), the chain rule and \eqref{eq:F} give \[ r_t' = -\frac{\Prod(P_tg)}{\atanh r_t} \le-r_t. \] Thus \(r_t\le e^{-t}r_0\). If information becomes zero, the field is constant by Lemma~\ref{lem:scalar} and remains so. For boundary-valued inputs apply the result to \((1-\eta)u\), then let \(\eta\downarrow0\) using continuity of finite sums. Correlation zero follows by taking the constant mean. Negative correlations follow from \[ T_{-\rho}u(y)=T_\rho u(-y) \] and invariance of uniform averages under \(y\mapsto-y\). \end{proof} The hypothesis of Proposition~\ref{prop:conditionalflow} is not proved in this manuscript. In particular, the exact semigroup identity does not prove the nonlinear induction step. The mean-dependent joining profile is intended to supply that step \cite{OpenAI119I,ChenGohariNair}. This semigroup acts on classical functions. No matrix-algebra Lindblad evolution is specified. \subsection{Gate 4: asymmetric Hellinger induction and arithmetic} Let \(f_+,f_-\) be Boolean sections and \(d_\pm=T_\rho f_\pm\) on the remaining cube. The exact recursion is \begin{align} T_\rho f(y',1) &=\frac{1+\rho}{2}d_+(y') +\frac{1-\rho}{2}d_-(y'),\\ T_\rho f(y',-1) &=\frac{1-\rho}{2}d_+(y') +\frac{1+\rho}{2}d_-(y'). \label{eq:Hrecursion} \end{align} The means of the sections may differ. Replacing them by a balanced pair would change the problem. The 119-02 route uses asymmetric profiles before reflection, and a separately calibrated semigroup-energy continuation \cite{OpenAI119Induction,OpenAI119II}. For \(g_t=P_tf\), the elementary derivative underlying such a continuation is \begin{equation} \frac{d}{dt}\E H(g_t) = \E\!\left[\frac{g_t}{H(g_t)}\Num g_t\right] = \frac14\sum_i \E\!\left[ (g_t-g_t^{(i)}) \left( \frac{g_t}{H(g_t)} -\frac{g_t^{(i)}}{H(g_t^{(i)})} \right) \right], \label{eq:Henergy} \end{equation} whenever the field is interior. The identity follows from \(H'(r)=-r/H(r)\) and symmetrization under coordinate flips. For a noised coordinate the derivative is \(e^{-2t}/\sqrt{1-e^{-2t}}\). An estimate must preserve that calibration to preserve sharpness. The source's finite arithmetic certificates concern scalar inequalities supporting this route \cite{OpenAI119Arithmetic}. Their audit requires: \begin{enumerate} \item the complete parameter domain and every subdivision; \item positivity of any cleared denominator; \item nonnegative sides before squaring; \item rigorous interval endpoints and series tails; \item coverage of seams, singular limits, and all bias regimes; \item the correct logical passage from the scalar estimates to the dimension-free assertion. \end{enumerate} For example, nonnegative Bernstein coefficients prove the sign of a specified polynomial on a specified box because the Bernstein basis is nonnegative and sums to one. They do not identify an omitted polynomial or cover an omitted box. We do not report execution of the source's certificates. The arithmetic in Section~\ref{sec:finite} instead belongs to our entirely specified sixteen-function instance. \subsection{Gate 5: Hellinger implies information} The implication is a classical convexity statement, not an identification of the two functionals. We prove it in Section~\ref{sec:implication}, then apply it only to the finite certificate proved here. It neither makes 119-02 a premise of 119-01 nor transfers either assertion to quantum inputs. \section{Stages 3 and 6: the complete finite certificate} \label{sec:finite} \subsection{The frozen instance and its entire kernel} Fix \begin{equation} n=2,\qquad \rho_0=\frac12,\qquad \varepsilon_0=\frac14,\qquad s_0=H(\rho_0)=\frac{\sqrt3}{2},\qquad C_0=1-s_0. \label{eq:frozen} \end{equation} Order the cube as \[ v_1=(1,1),\quad v_2=(1,-1),\quad v_3=(-1,1),\quad v_4=(-1,-1). \] The complete noise matrix is \begin{equation} K_{\rho_0} = \frac1{16} \begin{pmatrix} 9&3&3&1\\ 3&9&1&3\\ 3&1&9&3\\ 1&3&3&9 \end{pmatrix}. \label{eq:fourmatrix} \end{equation} Its row and column sums are one. The joint law of \((X,Y)\) is \(K_{\rho_0}/4\). For Boolean \(f\), define its Hellinger loss and its gap from the coordinate bound by \begin{equation} \Loss(f)=H(\E f)-\E H(T_{\rho_0}f), \qquad \Gap(f)=C_0-\Loss(f). \label{eq:lossgap} \end{equation} Concavity of \(H\) and mean preservation imply \(\Loss(f)\ge0\). \subsection{Exhaustive classification of the sixteen functions} Input coordinate permutations, independent input sign changes, and output complementation preserve the mean up to sign and preserve the distribution of the noised values up to sign. They therefore preserve both \(\Loss\) and \(\Gap\). \begin{lemma}[Four exhaustive orbits] \label{lem:orbits} Every Boolean function on \(\Omega_2\) belongs to exactly one of the following four classes: \begin{enumerate} \item the two constants; \item the four signed coordinates; \item the two signed parity functions \(\pm x_1x_2\); \item the eight functions with one exceptional vertex, or their complements. \end{enumerate} A representative of the last orbit is \[ q(x)=1-2\,\mathbf1_{\{x=(1,1)\}}. \] \end{lemma} \begin{proof} Classify by the size of the positive set. Sizes zero and four give the constants. Sizes one and three give eight functions, all in the exceptional-vertex orbit. At size two there are six unordered pairs of vertices. Four pairs are edges of the square; their indicators give signed coordinates. The remaining two pairs are diagonals; they give signed parity. This accounts for \(2+4+2+8=16\) functions. \end{proof} The complete representative calculation is: \begin{center} \small \begin{tabular}{@{}lcrrrr@{}} \toprule Representative & \(m\) & \(f(v_1)\)&\(f(v_2)\)&\(f(v_3)\)&\(f(v_4)\)\\ \midrule \(1\)&\(1\)&\(1\)&\(1\)&\(1\)&\(1\)\\ \(x_1\)&\(0\)&\(1\)&\(1\)&\(-1\)&\(-1\)\\ \(x_1x_2\)&\(0\)&\(1\)&\(-1\)&\(-1\)&\(1\)\\ \(q\)&\(1/2\)&\(-1\)&\(1\)&\(1\)&\(1\)\\ \bottomrule \end{tabular} \medskip \begin{tabular}{@{}lrrrr@{}} \toprule Representative & \(T_{\rho_0}f(v_1)\)& \(T_{\rho_0}f(v_2)\)& \(T_{\rho_0}f(v_3)\)& \(T_{\rho_0}f(v_4)\)\\ \midrule \(1\)&\(1\)&\(1\)&\(1\)&\(1\)\\ \(x_1\)&\(1/2\)&\(1/2\)&\(-1/2\)&\(-1/2\)\\ \(x_1x_2\)&\(1/4\)&\(-1/4\)&\(-1/4\)&\(1/4\)\\ \(q\)&\(-1/8\)&\(5/8\)&\(5/8\)&\(7/8\)\\ \bottomrule \end{tabular} \end{center} These entries follow by multiplication by \eqref{eq:fourmatrix}; no dimension induction is being used. For the biased representative, the full three-atom posterior table is \begin{equation} \begin{array}{c|ccc} d=T_{\rho_0}q(Y)&-1/8&5/8&7/8\\ \hline \Prob(d)&1/4&1/2&1/4\\ \Prob(q(X)=1\mid Y)&7/16&13/16&15/16\\ H(d)&3\sqrt7/8&\sqrt{39}/8&\sqrt{15}/8 \end{array}. \label{eq:posterior} \end{equation} This is a posterior law for this function, not a solution of the unrelated joining optimization \eqref{eq:joiningproblem}. \subsection{Exact integer-square certificates} \begin{lemma}[Root enclosures] \label{lem:roots} Let \(Q=100000\). The following strict enclosures hold: \[ \frac{173205}{Q}<\sqrt3<\frac{173206}{Q}, \qquad \frac{264575}{Q}<\sqrt7<\frac{264576}{Q}, \] \[ \frac{387298}{Q}<\sqrt{15}<\frac{387299}{Q}, \qquad \frac{624499}{Q}<\sqrt{39}<\frac{624500}{Q}. \] \end{lemma} \begin{proof} For each row of the following table, both displayed residuals are positive integers: \[ \begin{array}{c|r|r|r|r} k&a&b&kQ^2-a^2&b^2-kQ^2\\ \hline 3&173205&173206&27975&318436\\ 7&264575&264576&69375&459776\\ 15&387298&387299&259196&515401\\ 39&624499&624500&998999&250000 \end{array}. \] Hence \(a^2\frac{27}{1000}. \label{eq:uniformgap} \end{equation} \end{theorem} \begin{proof} The representative tables and evenness of \(H\) give every entry in \eqref{eq:gaptable}. Lemma~\ref{lem:orbits} transfers them to all sixteen functions. For parity, Lemma~\ref{lem:roots} gives \[ \frac{40886}{400000} < \frac{\sqrt{15}-2\sqrt3}{4} < \frac{40889}{400000}. \] These bounds lie strictly between \(102/1000\) and \(103/1000\). For the exceptional-vertex orbit, the same root enclosures give \[ \frac{ 3(264575)+2(624499)+387298+32Q-32(173206) }{32Q} < 1+B_q-\sqrt3 \] and \[ 1+B_q-\sqrt3 < \frac{ 3(264576)+2(624500)+387299+32Q-32(173205) }{32Q}. \] The two numerators are, respectively, \(87429\) and \(87467\). Therefore \[ \frac{87429}{3200000} < \Gap(q) < \frac{87467}{3200000}. \] Since \[ 86400<87429<87467<89600, \] this proves \eqref{eq:biasedgap}. For constants, \[ \Gap(f) > 1-\frac{173206}{200000} = \frac{26794}{200000} > \frac{27}{1000}. \] Thus every noncoordinate class has a strictly positive gap, and the coordinate class has gap zero. This proves the inequality, the equality classification, and \eqref{eq:uniformgap}. \end{proof} \begin{remark}[What has been evaluated] The certificate specifies the entire input set, all admissible Boolean functions through exhaustive orbits, every kernel entry, every posterior value, and explicit integer comparisons. It does not rely on a floating-point search or an unprinted optimizer. The general three-point joining optimizer has not been evaluated here. That is not the selected next theorem: the selected next theorem is the finite Hellinger certificate, which is now proved. \end{remark} \section{The Courtade--Kumar implication as a corollary} \label{sec:implication} The conversion below is the classical implication of Anantharam, Bogdanov, Chakrabarti, Jayram, and Nair \cite[Proposition 1]{ABCJN}. It is reproduced with all normalizations fixed. \begin{lemma}[Convex entropy conversion] \label{lem:conversion} Define \[ \varphi(t)= \hbin\!\left(\frac{1-\sqrt{1-t^2}}2\right), \qquad 0\le t\le1. \] Then \(\varphi\) is increasing and convex, and \begin{equation} \hbin\!\left(\frac{1+u}{2}\right)=\varphi(H(u)) \qquad(-1\le u\le1). \label{eq:conversionidentity} \end{equation} For \(0\le a\le b\le1\), \begin{equation} \varphi(b)-\varphi(a) \ge\frac{b^2-a^2}{2\ell}. \label{eq:conversionlower} \end{equation} \end{lemma} \begin{proof} For \(0\frac1{50} \quad\text{bit}. \label{eq:strictMI} \end{equation} For the named parity comparison, \[ \Info_2(x_1x_2;Y)=1-\hbin(3/8). \] \end{corollary} \begin{proof} Apply Proposition~\ref{prop:HtoI} to Theorem~\ref{thm:finite}. For a noncoordinate function, \(\eta=\Gap(f)>27/1000\). By \eqref{eq:conversionlower}, \[ \varphi(s_0+\eta)-\varphi(s_0) \ge \frac{2s_0\eta+\eta^2}{2\ell} \ge\frac{s_0\eta}{\ell}. \] Now \(s_0>4/5\), by squaring, and \(\ell=\int_1^2dt/t<1\). Consequently the information gap is strictly greater than \[ \frac45\frac{27}{1000} = \frac{108}{5000} > \frac1{50}. \] For a coordinate, \eqref{eq:MI} and \(T_{1/2}x_i=x_i/2\) give the exact value \(1-\hbin(1/4)\). For parity, the posterior mean is \(\pm1/4\), giving \(1-\hbin(3/8)\). \end{proof} This is a corollary of the finite Hellinger certificate. No all-dimensional information theorem has been imported. \section{Stage 2: pricing only the specified objects} \label{sec:pricing} \subsection{An exact classical sampler} \begin{proposition}[A finite stochastic implementation] \label{prop:sampler} The joint law at the frozen instance can be generated using six independent fair bits and deterministic classical operations. Two bits generate \(X\) uniformly. Two further independent pairs generate the two noise signs: flip coordinate \(i\) exactly when both bits of its pair are one. \end{proposition} \begin{proof} Each flip has probability \(1/4\), and the flip events are independent of one another and of \(X\). Thus the induced transition probabilities are \(9/16\), \(3/16\), or \(1/16\), according to whether zero, one, or two coordinates differ. This is exactly \eqref{eq:fourmatrix}. Each of the \(64\) seeds is equiprobable, so the joint table has denominator \(64\). \end{proof} This is an explicit upper resource count for one classical sampler. It is not a minimum-memory theorem, an optimal circuit claim, or a Choi-rank calculation. \subsection{A complete-record statistical allowance} \begin{specification}[Declared score and repeated experiments] \label{spec:statistics} Fix the truth table \(f\), the ideal kernel \eqref{eq:fourmatrix}, and the score \[ W_f(y)=H(T_{1/2}f(y))\in[0,1]. \] Perform \(N\) independent attempted experiments. Every attempt must be scored by the predeclared rule; no success-only postselection or unaccounted stopping is allowed. The score uses the already known ideal posterior table. It is not an estimator of an unknown conditional entropy from a single observed conditional label. \end{specification} \begin{proposition}[Finite-sample coverage for the declared score] \label{prop:coverage} Suppose each actual output law is within total variation \(e\) of the specified uniform ideal law, and each recorded score approximates \(W_f\) with deterministic error at most \(\kappa\). For independent repetitions with the same actual law, put \[ \widehat\Gap = C_0-H(\E f)+\overline W_N. \] Then, with probability at least \(1-\alpha\), \begin{equation} |\widehat\Gap-\Gap(f)| \le \sqrt{\frac{\ln(2/\alpha)}{2N}}+e+\kappa. \label{eq:coverage} \end{equation} An additional calibration-failure probability \(\beta\) enlarges the failure probability to at most \(\alpha+\beta\). \end{proposition} \begin{proof} A function in \([0,1]\) changes in expectation by at most the total variation distance. Score rounding changes the sample mean by at most \(\kappa\). For completeness, for any \(W\in[0,1]\), the log moment generating function of \(W-\E W\) has value and derivative zero at zero. Its second derivative is a variance under an exponentially tilted law, at most \(1/4\). Hence \[ \ln\E e^{t(W-\E W)}\le t^2/8. \] Independence, exponential Markov inequality, and optimization over \(t\) give \[ \Prob\{|\overline W_N-\E W|>r\}\le2e^{-2Nr^2}. \] Taking \(r=\sqrt{\ln(2/\alpha)/(2N)}\), then adding the model and rounding allowances, proves \eqref{eq:coverage}. The calibration assertion is a union bound. This is Hoeffding's bounded-variable argument \cite{Hoeffding}. \end{proof} The proof discipline is comparable to Cheung's complete-record statistical interfaces in En01-B and En01-C \cite{CheungEn01B,CheungEn01C}. Their physical statistics are not identified with the present score. A confidence interval does not prove a sharp constant: Theorem~\ref{thm:finite} is an exact calculation, while Proposition~\ref{prop:coverage} concerns repeated sampling under additional hypotheses. \subsection{The comparison templates and their limits} \begin{longtable}{@{}p{.24\linewidth}p{.34\linewidth}p{.34\linewidth}@{}} \toprule Template & What can be priced or compared & What is not supplied\\ \midrule \endfirsthead \toprule Template & What can be priced or compared & What is not supplied\\ \midrule \endhead \bottomrule \endfoot En02-A, \texttt{thm:Dprime} & A specified quantum instrument's one-shot environment and register ledger. & Neither the classical kernel \(T_\rho\) nor \(\Info(f(X);Y)\).\\[5pt] En02-B, \texttt{thm:B1} & Correctness and live-memory accounting for a supplied finite decoder program. & A Boolean optimizer or a decoder from a joining law.\\[5pt] Landmark I; VIII-B & Destructive readout semantics and a record-only quantum-recovery obstruction. & Coordinate optimality. The supplied quantitative \texttt{prop:classical-recovery} is in VIII-B, version 3.\\[5pt] En07-A & Complete-complement recovery and readout-and-drop. & Hellinger contraction. Its supplied \texttt{thm:exact} is a recovery criterion, not the label of a cube-noise inequality.\\[5pt] En01-B / En01-C & Coverage for declared complete-record statistics. & A sharp inequality for all truth tables and correlations.\\[5pt] Em03-F, \texttt{thm:EB} & A particular measure-and-prepare channel and its recovery obstruction. & The cube-noise operator or its extremizers.\\[5pt] Em03-G, \texttt{thm:lower} & A positive error lower bound at each fixed finite model parameter. & A vanishing-error theorem from the lower bound alone. Growing-resource transmission is a separate result.\\[5pt] Oai272-A context & The nominated uniform secret-bit gap in its declared protocol model. & A mutual-information inequality or a verified premise of this certificate.\\[5pt] Oai265-A, \texttt{thm:separation} & Static-record, channel, and history separation. & A Boolean function or a cube-noise theorem.\\[5pt] Oai276 context & Classical transmission through a specified qubit damping channel. & The present uniform-cube summary problem.\\[5pt] Oai274 context & The nominated parity/circuit-complexity comparison. & A premise about \(T_\rho\), or a transfer of a coordinate optimizer to QAC\(^{0}\).\\ \end{longtable} The Cheung references in this table are scoped comparisons drawn from the supplied passages \cite{CheungEn02A,CheungEn02B,CheungI,CheungVIIIB, CheungEn07A,CheungEm03F,CheungEm03G,CheungOai265A}. Labels not supported by the supplied excerpts are not silently promoted to verified results. Families 272, 274, 276, and 279 remain catalogue comparisons. No factoring theorem, zero-key construction, circuit lower bound, or damping-capacity theorem is needed for the local proof \cite{Dossier119,Oai276Context}. \section{Stages 3 and 4: evaluation and hypothesis changes} \label{sec:hypotheses} \subsection{A sharp statement and its finite evaluation} The external general assertions name a sharp constant and an attaining example. The present certificate additionally prints: \begin{enumerate} \item all four input points and all transition probabilities; \item an exhaustive partition of the sixteen Boolean functions; \item every representative truth table and noised value; \item a signed coordinate attaining equality; \item parity and a biased noncoordinate function with exact gaps; \item finite integer-square certificates for the numerical bounds; \item the information implication and its normalization in bits. \end{enumerate} A three-atom posterior distribution is not automatically the three-point optimizer of the local joining problem. Neither a Lean target nor an implementation ledger supplies that missing identification. \subsection{Uniform input is an operative hypothesis} \begin{example}[Dropping uniformity changes even the coordinate value] \label{ex:nonuniform} Let \(S\) be a uniform sign, but prepare \[ X=(S,S) \] rather than a uniform point of \(\Omega_2\). Apply independent crossover-\(1/4\) noise to both coordinates, and take \(f(X)=X_1=S\). Then \[ \Info_2(S;Y_1,Y_2)>\Info_2(S;Y_1) =1-\hbin(1/4). \] Indeed, \(Y_2\) carries nonzero additional information about \(S\) conditional on \(Y_1\): both conditional values of \(S\) have positive probability, and their \(Y_2\)-laws differ. Strict concavity of binary entropy makes the information increase strict. Explicitly, \[ \Info_2(S;Y_1,Y_2) = \frac58\bigl(1-\hbin(1/10)\bigr). \] The two observations disagree with probability \(3/8\), in which case the posterior is fair; when they agree, the posterior error is \(1/10\). Thus the frozen universal constant cannot simply be retained after dropping the uniform-product-input assumption. \end{example} For this example the posterior kernel is not \eqref{eq:kernel}; Bayes' rule uses the changed input law. \subsection{Independent flips are also operative} \begin{example}[Correlated noise preserves parity perfectly] \label{ex:correlated} Keep \(X\) uniform on \(\Omega_2\), but let the two noise signs be one common sign: \[ Z_1=Z_2=Z,\qquad \E Z=\frac12. \] Each coordinate separately still has crossover \(1/4\), but the flips are not independent. Then \[ Y_1Y_2=X_1X_2Z^2=X_1X_2. \] Consequently parity has mutual information one bit with \(Y\), and its posterior mean has absolute value one. Its Hellinger loss is therefore one, not at most \(1-\sqrt3/2\). \end{example} Marginal crossover probabilities do not specify the product noise model. \subsection{Soft summaries, output bias, and asymmetric noise} For a soft \(u\), the conditional entropy \(\E h(u)\) need not vanish. Replacing \(\Isoft(u)\) by \(h(\E u)\) would erase that randomization cost and change the fixed-information problem. Arbitrary output bias means that \(m=\E f\) is unrestricted while \(X\) remains uniform. It does not mean that the input distribution is arbitrary. Asymmetric bit transitions generally destroy the symmetry \(K(x,y)=K(y,x)\), uniform stationarity, and the one-parameter Walsh multiplier \(\rho^{|A|}\). Such a model requires a new posterior kernel and a new comparison theorem. \subsection{Parity and circuit complexity} For a Walsh character of degree \(k\), \[ T_\rho\chi_A=\rho^k\chi_A,\qquad |A|=k. \] Thus parity is degree two in our finite example and degree \(n\) on the full \(n\)-variable parity family. This is a spectral calculation, not a circuit lower bound. A QAC\(^{0}\) parity obstruction concerns allowed gates, depth, size, and possibly ancillary systems. None of those parameters occurs in Theorem~\ref{thm:finite}. Conversely, no nominated circuit-complexity theorem proves the Hellinger inequality. \subsection{A classical kernel does not specify a quantum extension} Here is an explicit non-identification, used only as a comparison. For a qubit let \[ \Delta(A)=\kb00A\kb00+\kb11A\kb11, \] and \[ \mathcal B_\varepsilon(A) = (1-\varepsilon)A+\varepsilon XAX, \] where \(X\) is the Pauli bit flip. The two CPTP maps \(\mathcal B_\varepsilon\) and \(\mathcal B_\varepsilon\circ\Delta\) agree on every diagonal input. They therefore implement the same classical binary symmetric transition on computational-basis data. Nevertheless, \[ \mathcal B_\varepsilon(\proj+)=\proj+, \qquad (\mathcal B_\varepsilon\circ\Delta)(\proj+)=I_2/2. \] The output trace distance is \(1/2\). The second extension is measure-and-prepare; the classical transition table alone did not select that extension. This is the kind of distinction between records and full quantum outputs emphasized by Cheung's readout and residual comparisons \cite{CheungVIIIA,CheungVIIIB,CheungEn07A}. The standard measure-and-prepare characterization is given in \cite{HSR}. Similarly, \(H(t)\) is a classical affinity: for the two Bernoulli laws \[ p_t=\left(\frac{1+t}{2},\frac{1-t}{2}\right), \qquad p_{-t}=\left(\frac{1-t}{2},\frac{1+t}{2}\right), \] one has \[ \sum_j\sqrt{p_t(j)p_{-t}(j)}=H(t). \] The fact that classical affinities admit diagonal-matrix representations does not prove an inequality for arbitrary noncommuting density operators, entangled inputs, or collective POVMs. \subsection{Quantities that remain separate} \begin{longtable}{@{}p{.29\linewidth}p{.63\linewidth}@{}} \toprule Proposed change & Exact boundary\\ \midrule \endfirsthead \toprule Proposed change & Exact boundary\\ \midrule \endhead \bottomrule \endfoot Hellinger loss to mutual information & Requires the convexity argument in Section~\ref{sec:implication}; the functionals are not equal.\\[4pt] Classical summary to quantum recovery & Requires a quantum input/output interface and a recovery criterion. A coordinate optimizer is not a quantum decoder.\\[4pt] One-bit information to channel capacity & Requires a coding model and asymptotic error criterion. The summary problem is not a capacity optimization.\\[4pt] Information to secret key & Requires an adversarial system, access specification, and secrecy criterion. No such system is present here.\\[4pt] Finite exact certificate to general inequality & Requires all dimensions and all correlations. A finite arithmetic instance does not supply these quantifiers.\\[4pt] Sampling coverage to a sharp constant & Requires an exact mathematical upper bound; a confidence statement is not that bound.\\[4pt] Area-law record to cube contraction & Requires a specified mathematical interface. None is supplied by similarly named entropy quantities.\\ \end{longtable} \section{Stage 5: gravitational and recovery readings remain separations} \label{sec:separations} The mathematical data here are a finite set, its uniform law, a stochastic matrix, and a Boolean truth table. They specify neither a metric nor a gravitational interaction. The parameter \(t\) in \(P_t=T_{e^{-t}}\) is a classical Markov-semigroup parameter. Calling it time does not identify it with a spacetime coordinate or an evaporation process. The number operator \(\Num\) acts on functions on the cube; no physical Lindblad generator is specified. This does not deny that a classical Markov process can be embedded in a larger matrix evolution. Such an embedding is additional data, as the preceding quantum-extension example illustrates. A Page curve requires a specified time-indexed radiation state and access partition. An island or horizon requires geometric and dynamical structure. A gravity-generated-entanglement test requires a preparation, mediator model, output state, and comparison class. None occurs in the contraction experiment. Cheung's Oai265-A separates static entropy records from recovery and radiation histories, and the supplied XIV-I/J passages separate defined internal kernels from an unconstructed full characteristic composition \cite{CheungOai265A,CheungXIVI,CheungXIVJ}. Those are relevant cautions about transferring premises, not analytic inputs to our finite cube calculation. Enter, where invoked in the comparison manuscripts, remains destructive readout. A classical record does not become a reference-preserving unknown-state decoder because it contains a particularly informative bit \cite{CheungI,CheungVIIIB,CheungEn07A}. No Page curve, island, horizon, Hawking-radiation derivation, gravity-generated entanglement, exclusion of classical gravity, or spacetime-emergence theorem is established. \section{Release: the completed plan and unchanged general claims} \label{sec:release} \begin{center} \small \begin{tabularx}{\linewidth}{@{}p{.08\linewidth}X p{.31\linewidth}@{}} \toprule Stage & Completed task & Status\\ \midrule 0 & Uniform input, independent symmetric noise, the two profiles, information units, external statements, and formalization scope are distinguished. & Frozen; no external general theorem is a premise.\\[5pt] 1 & Scalar, joining, semigroup, asymmetric Hellinger, arithmetic, and implication interfaces are audited. & Elementary identities proved; universal proof obligations remain explicit.\\[5pt] 2 & A concrete sampler and finite-sample allowance are supplied. Comparison ledgers retain their own interfaces. & No decoder or resource optimum is inferred from a template.\\[5pt] 3 & The exact kernel, posterior tables, equality example, and strict numerical gaps are printed. & Evaluation supplied for the frozen instance.\\[5pt] 4 & Input law, independence, summary type, functional, coding task, and quantum interface are varied separately. & No silent hypothesis weakening.\\[5pt] 5 & Thermal, gravitational, temporal, and recovery readings are kept separate. & No standing physical problem is solved.\\[5pt] 6 & The one selected finite Hellinger theorem is proved, with the Courtade--Kumar conclusion as a corollary. & Completed by Theorem~\ref{thm:finite} and Corollary~\ref{cor:finiteCK}.\\ \bottomrule \end{tabularx} \end{center} The exact mathematical conclusion is \[ \boxed{ \begin{gathered} n=2,\qquad \rho=\frac12,\qquad H(\E f)-\E H(T_{1/2}f)\le1-\frac{\sqrt3}{2},\\[2pt] \text{equality exactly for }\pm x_1,\ \pm x_2,\\[2pt] \Gap(f)>\frac{27}{1000} \quad\text{for every other Boolean function},\\[2pt] \frac{102}{1000}<\Gap(x_1x_2)<\frac{103}{1000},\\[2pt] \Info_2(f(X);Y)\le1-\hbin(1/4),\\[2pt] \text{information gap}>\frac1{50}\text{ bit for every nonsigned-coordinate function}. \end{gathered}} \] The finite certificate now exists. The following conclusions still do not follow: \begin{itemize} \item independent verification of 119-01 or 119-02; \item a completed proof of the inspected Lean targets; \item formalization of 119-02's \texttt{thm:main} by targets that name 119-01; \item a noncommutative fidelity inequality, a quantum mutual-information inequality, or a collective-measurement optimizer; \item a Page curve or a gravity test. \end{itemize} These are logical scope boundaries. They do not assert that other researchers cannot prove a broader statement independently, or that no proof exists elsewhere. \appendix \section{Optional exact-arithmetic checker} \label{app:checker} The following optional Python code independently reconstructs the kernel and inspects all sixteen truth tables. It uses rational arithmetic and integer square roots only. It is not needed as a premise of the printed proof. No execution is asserted. \begingroup \small \begin{verbatim} from fractions import Fraction as F from itertools import product from math import isqrt vertices = [(1,1), (1,-1), (-1,1), (-1,-1)] rho = F(1,2) Q = 100000 def kernel(x, y): out = F(1) for xi, yi in zip(x, y): out *= (1 + rho*xi*yi)/2 return out K = [[kernel(x,y) for y in vertices] for x in vertices] expected = [ [9,3,3,1], [3,9,1,3], [3,1,9,3], [1,3,3,9] ] assert K == [[F(a,16) for a in row] for row in expected] assert all(sum(row, F(0)) == 1 for row in K) assert all(sum(K[i][j] for i in range(4)) == 1 for j in range(4)) def noise(f): return tuple( sum((K[y][x]*f[x] for x in range(4)), F(0)) for y in range(4) ) def sqrt_interval(z): assert z >= 0 A = z.numerator * Q*Q B = z.denominator a = isqrt(A // B) assert a*a*B <= A < (a+1)*(a+1)*B return F(a,Q), F(a+1,Q) def H_interval(t): return sqrt_interval(1-t*t) coord = set() for i in range(2): for sign in (-1,1): coord.add(tuple(sign*x[i] for x in vertices)) assert len(coord) == 4 assert noise((1,1,-1,-1)) == ( F(1,2),F(1,2),-F(1,2),-F(1,2) ) assert noise((1,-1,-1,1)) == ( F(1,4),-F(1,4),-F(1,4),F(1,4) ) assert noise((-1,1,1,1)) == ( -F(1,8),F(5,8),F(5,8),F(7,8) ) slo, shi = H_interval(rho) counts = {"constant":0, "coordinate":0, "parity":0, "exceptional":0} for f in product((-1,1), repeat=4): m = F(sum(f),4) d = noise(f) if f in coord: counts["coordinate"] += 1 assert m == 0 assert all(abs(v) == rho for v in d) continue if abs(m) == 1: counts["constant"] += 1 elif m == 0: counts["parity"] += 1 else: counts["exceptional"] += 1 hlo, hhi = H_interval(m) intervals = [H_interval(v) for v in d] blo = sum((a for a,b in intervals), F(0))/4 bhi = sum((b for a,b in intervals), F(0))/4 gap_lower = (1-shi)-hhi+blo gap_upper = (1-slo)-hlo+bhi assert gap_lower > F(27,1000) if m == 0: assert gap_lower > F(102,1000) assert gap_upper < F(103,1000) if abs(m) == F(1,2): assert gap_upper < F(28,1000) assert counts == { "constant":2, "coordinate":4, "parity":2, "exceptional":8 } root_rows = [ (3,173205,173206,27975,318436), (7,264575,264576,69375,459776), (15,387298,387299,259196,515401), (39,624499,624500,998999,250000) ] for k,a,b,left,right in root_rows: assert k*Q*Q-a*a == left > 0 assert b*b-k*Q*Q == right > 0 \end{verbatim} \endgroup The integer-root routine is sound because \[ a^2\le\left\lfloor Q^2z\right\rfloor<(a+1)^2 \] implies \(a/Q\le\sqrt z<(a+1)/Q\). The checker covers a finite list of sixteen objects. It makes no assertion about all dimensions. \section{Documentary corrections} \label{app:documentary} \begin{enumerate} \item The notation \(H\) in 119-01 denotes sign entropy, whereas \(H\) in 119-02 denotes \(\sqrt{1-t^2}\). This manuscript uses \(h\) for the former throughout. \item The supplied En07-A \texttt{thm:exact} is a complete-complement recovery criterion. Readout-and-drop is a separate statement in its interface. \item The supplied Landmark I excerpt proves a finite Born/destructive-readout characterization. The explicit quantitative \texttt{prop:classical-recovery} excerpt appears in VIII-B, version 3. \item Em03-G's supplied \texttt{thm:lower} gives a strictly positive lower bound at each fixed finite coupling. The compatibility of such bounds with growing-resource transmission is not itself an upper-bound construction. \item The large XIV--XV--XVI dossier concerns different domains, equation spaces, and distributions. Its characteristic-map and admission obligations are not steps in the proof of the finite cube certificate. \end{enumerate} \section*{Declarations} \addcontentsline{toc}{section}{Declarations} \paragraph{Authorship and identifier.} The requested identifier Oai119-A is used for this development. It does not attribute authorship to N.~Cheung or assert registration or endorsement by another series. \paragraph{Mathematical scope.} The principal result is the printed exact certificate for \(n=2,\rho=1/2\), together with its classical information corollary. Supporting scalar and probabilistic results are proved locally. The universal Family 119 assertions are not verified or assumed. \paragraph{Sources.} External manuscript assertions are identified as such. Cheung's supplied manuscripts are cited for their stated comparison interfaces, not imported as proofs of contraction. No exhaustive corpus scan is claimed. \paragraph{Formal and computational status.} No successful Lean execution, execution of the appendix, independent numerical run, successful pdfLaTeX build, referee approval, or journal acceptance is asserted. An unexecuted program is not substituted for the printed integer-square proof. \paragraph{Unchanged standing boundaries.} For the distinct programmes described in the supplied dossier, this manuscript establishes no result changing their status: \[ \boxed{ \text{O.1 remains }\NOTCLOSED,\qquad \text{the downstream XV-B admission exit is not opened},\qquad \text{XVI-N is not discharged}. } \] This does not deny the existence of technical continuation manuscripts or their separately scoped interface theorems. No inherited quantum coefficient is admitted here. \begin{thebibliography}{99} \addcontentsline{toc}{section}{References} \bibitem{CourtadeKumar2014} T.~A.~Courtade and G.~R.~Kumar. Which Boolean functions maximize mutual information on noisy inputs? \emph{IEEE Transactions on Information Theory} \textbf{60}(8) (2014), 4515--4525. doi:10.1109/TIT.2014.2326877. Historical formulation of the conjecture, not an assertion of its present verification status. \url{https://people.eecs.berkeley.edu/~courtade/pdfs/CourtadeKumar_TransITAug2014.pdf} \bibitem{ABCJN} V.~Anantharam, A.~Bogdanov, A.~Chakrabarti, T.~S.~Jayram, and C.~Nair. \emph{A conjecture regarding optimality of the dictator function under Hellinger distance}. Manuscript presented at the Information Theory and Applications Workshop, February 2017. Relevant items: Lemma 1 and Proposition 1, the classical Hellinger-to-information implication. \url{https://chandra.ie.cuhk.edu.hk/pub/papers/HC/hel-conj.pdf} \bibitem{ODonnell} R.~O'Donnell. \emph{Analysis of Boolean Functions}. Cambridge University Press, 2014. Revised author text, 2021. Uniform-cube Fourier and noise-operator conventions. \url{https://arxiv.org/abs/2105.10386} \bibitem{ChenGohariNair} Z.~Chen, A.~Gohari, and C.~Nair. \emph{A differential equation approach to the most-informative Boolean function conjecture}. 2025 IEEE International Symposium on Information Theory. Extended manuscript: arXiv:2502.10019. Cited for the local-production and semigroup methodology; no unverified auxiliary inequality is imported. \url{https://arxiv.org/abs/2502.10019} \bibitem{OpenAI119I} OpenAI. \emph{Sharp binary-information contraction on the discrete cube}. Family 119-01 manuscript, dated 24 September 2026. Relevant source labels: \texttt{main:soft}, \texttt{main:ck}, and \texttt{upgrade:production}. Recorded as external claims in this manuscript. \url{https://github.com/openai/math/blob/main/preprints/Sharp-binary-information-contraction-on-the-discrete-cube-September-24-2026/build/main.tex} \bibitem{OpenAI119Joining} OpenAI. \emph{A joining cost with one entropy budget}. Section \texttt{canonical.tex} of Family 119-01. Relevant labels: \texttt{canonical:priced} and \texttt{canonical:coverage}. \url{https://github.com/openai/math/blob/main/preprints/Sharp-binary-information-contraction-on-the-discrete-cube-September-24-2026/build/sections/canonical.tex} \bibitem{OpenAI119Reserve} OpenAI. \emph{A reserve that survives adding either common output}. Section \texttt{reserve.tex} of Family 119-01. The two-capacity allocation and mean-dependent reserve. \url{https://github.com/openai/math/blob/main/preprints/Sharp-binary-information-contraction-on-the-discrete-cube-September-24-2026/build/sections/reserve.tex} \bibitem{OpenAI119Thinning} OpenAI. \emph{Paying the information increment by thinning}. Section \texttt{thinning.tex} of Family 119-01. Relevant label: \texttt{thinning:payment}. \url{https://github.com/openai/math/blob/main/preprints/Sharp-binary-information-contraction-on-the-discrete-cube-September-24-2026/build/sections/thinning.tex} \bibitem{OpenAI119II} OpenAI. \emph{Hellinger contraction with arbitrary Boolean output bias}. Family 119-02 manuscript, dated 24 September 2026. Relevant source label: \texttt{thm:main}. The all-dimensional assertion is not independently verified here. \url{https://github.com/openai/math/blob/main/preprints/Hellinger-contraction-with-arbitrary-Boolean-output-bias-September-24-2026/build/main.tex} \bibitem{OpenAI119Induction} OpenAI. \emph{Dimension induction}. Section \texttt{induction.tex} of Family 119-02. Asymmetric-profile and section-comparison proof interface. \url{https://github.com/openai/math/blob/main/preprints/Hellinger-contraction-with-arbitrary-Boolean-output-bias-September-24-2026/build/sections/induction.tex} \bibitem{OpenAI119Arithmetic} OpenAI. \emph{Exact arithmetic conventions}. Section \texttt{arithmetic.tex} of Family 119-02. Bernstein, rational-interval, and integer-root certificate conventions; no execution is reported here. \url{https://github.com/openai/math/blob/main/preprints/Hellinger-contraction-with-arbitrary-Boolean-output-bias-September-24-2026/build/sections/arithmetic.tex} \bibitem{OpenAI119Implication} OpenAI. \emph{Completion of the proof}. Section \texttt{conclusion.tex} of Family 119-02. Relevant label: \texttt{cor:ck}. Reproduction of the classical implication of Anantharam et al.; not a premise proving the general Hellinger bound. \url{https://github.com/openai/math/blob/main/preprints/Hellinger-contraction-with-arbitrary-Boolean-output-bias-September-24-2026/build/sections/conclusion.tex} \bibitem{Lean119Scope} OpenAI. \emph{The Courtade--Kumar and Hellinger conjectures: Lean scope note}. Repository file \texttt{lean/docs/119.md}, consulted 14 October 2026. The listed accompanying paper is Family 119-01. \url{https://github.com/openai/math/blob/main/lean/docs/119.md} \bibitem{Lean119CK} OpenAI. \emph{CourtadeKumar.lean}. Repository file \texttt{lean/ComparatorChallenges/CourtadeKumar.lean}, consulted 14 October 2026. The inspected principal theorem body contains \texttt{sorry}. \url{https://github.com/openai/math/blob/main/lean/ComparatorChallenges/CourtadeKumar.lean} \bibitem{Lean119Soft} OpenAI. \emph{SoftChannel204.lean}. Repository file \texttt{lean/ComparatorChallenges/SoftChannel204.lean}, consulted 14 October 2026. The inspected \texttt{fullMain} body contains \texttt{sorry}. \url{https://github.com/openai/math/blob/main/lean/ComparatorChallenges/SoftChannel204.lean} \bibitem{Hoeffding} W.~Hoeffding. Probability inequalities for sums of bounded random variables. \emph{Journal of the American Statistical Association} \textbf{58}(301) (1963), 13--30. doi:10.1080/01621459.1963.10500830. \bibitem{HSR} M.~Horodecki, P.~W.~Shor, and M.~B.~Ruskai. Entanglement breaking channels. \emph{Reviews in Mathematical Physics} \textbf{15} (2003), 629--641. doi:10.1142/S0129055X03001709. Preprint title: \emph{General Entanglement Breaking Channels}. Cited only for the quantum-extension comparison. \url{https://arxiv.org/abs/quant-ph/0302031} \bibitem{CheungI} N.~Cheung. \emph{Landmark I}, version 2. Supplied manuscript \texttt{I.tex}. Relevant supplied label: \texttt{thm:main}. Finite Born probabilities and destructive projective residuals within the stated strategy class. Enter Calculus Companion. \bibitem{CheungVIIIA} N.~Cheung. \emph{Landmark VIII-A}, version 3. Supplied manuscript \texttt{VIII-A-v3.tex}. Relevant supplied label: \texttt{A:thm:residual}. Record agreement and complete residual agreement are different interfaces. Enter Calculus Companion. \bibitem{CheungVIIIB} N.~Cheung. \emph{Landmark VIII-B}, version 3. Supplied manuscript \texttt{VIII-B-v3.tex}. Relevant supplied label: \texttt{prop:classical-recovery}. Sharp record-only quantum-recovery obstruction. Enter Calculus Companion. \bibitem{CheungEn02A} N.~Cheung. \emph{En02-A}, version 1. Supplied manuscript \texttt{En02-A-v1.tex}. Relevant supplied label: \texttt{thm:Dprime}. One-shot environment accounting and its separation from adaptive occupancy. Enter Calculus Companion. \bibitem{CheungEn02B} N.~Cheung. \emph{En02-B}, version 1. Supplied manuscript \texttt{En02-B-v1.tex}. Relevant supplied label: \texttt{thm:B1}. Resource-certified finite decoder soundness. Enter Calculus Companion. \bibitem{CheungEn07A} N.~Cheung. \emph{En07-A}, version 1. Supplied manuscript \texttt{En07-A.tex}. Relevant supplied label: \texttt{thm:exact}. Complete-complement recovery; separately described readout-and-drop conventions. Enter Calculus Companion. \bibitem{CheungEn01B} N.~Cheung. \emph{En01-B}, version 2. Supplied manuscript \texttt{En01-B-v2.tex}. The supplied dossier records \texttt{thm:bounded} for bounded complete-record statistics. No physical diagnostic is identified with the present Hellinger score. Enter Calculus Companion. \bibitem{CheungEn01C} N.~Cheung. \emph{En01-C}, version 1. Supplied manuscript \texttt{En01-C.tex}. The supplied dossier records \texttt{thm:certificate} for clipping, complete attempted-run records, calibration, and finite-sample coverage. Enter Calculus Companion. \bibitem{CheungEm03F} N.~Cheung. \emph{Em03-F}, version 1. Supplied manuscript \texttt{Em03-F-v1.tex}. Relevant supplied labels: \texttt{thm:EB} and \texttt{thm:recovery}. A specified measure-and-prepare packet channel, not the cube-noise operator. Enter Calculus Companion. \bibitem{CheungEm03G} N.~Cheung. \emph{Em03-G}, version 1. Supplied manuscript \texttt{Em03-G-v1.tex}. Relevant supplied labels: \texttt{thm:lower}, \texttt{thm:compacttransmission}, and \texttt{prop:Fobstruction}. Finite-coupling lower bounds and growing-resource transmission are distinguished. Enter Calculus Companion. \bibitem{CheungOai265A} N.~Cheung. \emph{Oai265-A}, supplied version 1. Relevant supplied label: \texttt{thm:separation}. Static records, recovery, and radiation histories are distinct. Enter Calculus Companion. \bibitem{CheungXIVI} N.~Cheung. \emph{Landmark XIV-I}, version 1. Supplied manuscript \texttt{XIV-I.tex}. Relevant supplied labels: \texttt{thm:I2}, \texttt{thm:I3}, and \texttt{thm:release}. The internal amplitude construction and unresolved joint characteristic map are separate objects. Documentary comparison only. Enter Calculus Companion. \bibitem{CheungXIVJ} N.~Cheung. \emph{Landmark XIV-J}, version 1. Supplied manuscript \texttt{XIV-J.tex}. Relevant supplied labels: \texttt{thm:J2}, \texttt{thm:release}, and \texttt{cor:noadmission}. Supported-sector reference, unresolved complete map, and no quantum admission in the stated release. Documentary comparison only. Enter Calculus Companion. \bibitem{Oai276Context} \emph{Oai276-A: A finite certificate for a generalized amplitude-damping Holevo optimum}. Earlier development supplied in this conversation. Cited only to distinguish a damping-channel information problem from the discrete-cube problem. No attribution to N.~Cheung or independent verification of its external all-block-length claims is asserted. \bibitem{Dossier119} \emph{User-supplied Oai119-A plan and comparative source dossier}. Includes version-specific Cheung excerpts and catalogue comparisons for Families 119, 265, 272, 274, 276, and 279. Supplied retrieval identifier: \texttt{178f233f (retrieval-3)}. Not an exhaustive corpus inspection, formal verification, or transfer of model-specific premises. \end{thebibliography} \end{document}