Oai119-A An Exact Finite Certificate for Hellinger Contraction on the Two-Dimensional Discrete Cube Equality, strict gaps, the information corollary, and a seven-stage audit of Family 119

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.

The single new target selected by the plan is an explicit finite Hellinger certificate at one specified dimension and correlation. Theorem thm:finite completes that target for

It covers 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 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.

Let

For $-1\le \rho \le 1$, define

The matrix $K_{\rho }$ is symmetric and stochastic. In probabilistic terms, $X$ is uniform and

where the $Z_i$ are mutually independent and independent of $X$. Both $X$ and $Y$ are uniform. Symmetry gives

These are the standard cube-noise conventions 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\}$.

To avoid the conflicting uses of $H$ in the source manuscripts, define

The convention is $0\ln 0=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

Binary entropy in bits is

We write $I_2(A;B)$ for classical mutual information in bits and $I(A;B)=\ell I_2(A;B)$ for the same quantity in nats.

Given $u:{\Omega }_n\to [-1,1]$, construct a sign $U$ with

using auxiliary randomness independent of the noise conditional on $X$. Then

For Boolean $f$, one may take $U=f(X)$, and

Proof. The conditional mean of $U$ given $X$ is $u(X)$, so its conditional entropy is $\mathbb{E}h(u)$, while its mean is $\mathbb{E}u$. This proves the first identity. Conditional expectation and the stated conditional independence give

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 (eq:MI).

No intermediate measurement, quantum observable, or decoding operation occurs in this identity.

The manuscript Sharp binary-information contraction on the discrete cube, dated 24 September 2026, asserts

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 main:ck specializes this to

The refined upper curve is strictly below the universal curve when $0<|m|<1$ and $0<|\rho |\le 1$. Its separate upgrade:production asserts a stronger, mean-dependent production bound OpenAI119I.

The manuscript Hellinger contraction with arbitrary Boolean output bias, also dated 24 September 2026, asserts

for every Boolean $f$, every dimension, and every correlation. Signed coordinates attain equality. Its cor:ck derives the ordinary Courtade–Kumar bound from this assertion OpenAI119II,OpenAI119Implication.

The Courtade–Kumar formulation in bits is

For $\rho <0$, the same formula is valid because $h_2(\epsilon )=h_2(1-\epsilon )$.

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 ABCJN. Its elementary proof is included in Section sec:implication.

The scope note lean/docs/119.md names 119-01 and describes soft contraction, the Boolean refinement, and the selected production inequality Lean119Scope. The inspected Comparator challenge files CourtadeKumar.lean and SoftChannel204.lean specify these targets. Their respective principal theorem bodies, courtadeKumarAndAttainment and fullMain, contain sorry 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.

The following audit supplies elementary identities and identifies the nontrivial universal obligations. Recording an obligation does not discharge it.

The function $\psi$ is even, continuous on $[-1,1]$, strictly increasing on $[0,1]$, and strictly convex. For $|r|<1$,

Furthermore,

and $\mathcal{I}(u)=0$ if and only if $u$ is constant.

Define $F:[0,\ell )\to [0,\infty )$ by

Then $F(0)=0$, $F^{\prime }(0)=2$, $F$ is convex, and $F(s)\ge 2s$.

Proof. The derivatives follow by differentiation. The range of $\psi$ on $[0,1]$ is $[0,\ell ]$. Jensen's inequality proves nonnegativity of $\mathcal{I}$, with equality precisely for constant $u$, by strict convexity. Its upper bound follows from $h\ge 0$.

For $r>0$, put $V=\mathrm{atanh}r$. The chain rule gives

and

because $V\ge r$. The expansion $V=r+O(r^3)$ gives $F^{\prime }(0)=2$. Convexity and the tangent at zero give $F(s)\ge 2s$.

For a soft coordinate $u(x)=a{x}_i$,

This checks the asserted equality example directly, without proving the universal upper bound.

The scalar parameter ${\psi }^{-1}(\mathcal{I}(u))$ is an effective coordinate amplitude. It is not a channel capacity and does not construct an optimizer over arbitrary summary tables.

To state the production claim precisely, let

For $|m|<1$ and $0\le I<h(m)$, define

These are the source's profiles, expressed using our entropy notation OpenAI119I,OpenAI119Reserve.

Put

Then $c_m\ge 0$, and

The infimum is attained at $u=\min \{I,c_m\}$.

Proof. Integrating the power series for $\mathrm{atanh}r$ gives

Its positive coefficients sum to $\ell$, by continuity at $r=1$. Hence $\psi (m)\le m^2\ell$, proving $c_m\ge 0$.

At fixed $u+v=I$, increasing $u$ cannot increase the objective, since its derivative is $2-F^{\prime }((I-u)/\alpha )\le 0$. The largest feasible $u$ is $\min \{I,c_m\}$. Substitution gives $2I$ when $I\le c_m$, and

otherwise. These are exactly the two branches of (eq:Bprofile).

This allocation identity is not a decomposition of a physical channel. Proving it does not prove the source's bound $\mathcal{D}(g)\ge {\hat{\mathcal{B}}}_{\mathbb{E}g}(\mathcal{I}(g))$.

For interior $a,b$, set

The source extends $c$ by zero at $(1,1)$ and $(-1,-1)$, and by $+\infty$ at every other boundary pair.

For $|m|+\delta <1$, $\delta >0$, and

its relaxed joining problem is

The infimum ranges over arbitrary joint laws on $[-1,1{]}^2$, not just laws arising from a particular finite cube.

The source's claimed optimizer has the support table

with

The mean sum determines the remaining masses. Optimality against every admissible joint law, nonnegativity of the masses, and coverage of each entropy budget are separate obligations OpenAI119Joining.

For common-output thinning, write

Adding $(1,1)$ with retained core mass $\lambda$ gives

If

the asserted payment is

under its stated core hypotheses OpenAI119Thinning.

The audit must retain the original individual child entropies in the child profiles even though the joining relaxation constrains only their average. A candidate three-atom law does not establish optimizer uniqueness or budget coverage. Moreover, a relaxed optimizer need not have the dyadic weights of a prescribed finite cube.

A joining cost is not a decoder. The posterior table printed later in this paper is not relabelled as the optimizer of (eq:joiningproblem).

For a field $g$, define the number operator

where $x^{(i)}$ flips coordinate $i$. For interior $g$, put

Let $P_t=T_{e^{-t}}$. Then

If $g_{+},g_{-}$ are the two sections in one coordinate,

Proof. For $A\subseteq \{1,\dots ,n\}$, the Walsh character ${\chi }_A(x)={\prod }_{i\in A}{x}_i$ satisfies

These characters form a basis, proving the semigroup identity.

The mean is conserved, $h^{\prime }=-\mathrm{atanh}$, and ${\partial }_t{P}_{t}g=-\mathsf{N}{P}_{t}g$. Differentiation of (eq:softinfo) gives the production identity. Separating the last-coordinate term in $\mathsf{N}$ gives (eq:productionsplit), with the factor $1/4$ in (eq:joiningcost).

If the inequality

is available for every interior field on a fixed cube, then (eq:external-soft) follows on that cube for every soft summary.

Proof. For an interior field, put $r_t={\psi }^{-1}(\mathcal{I}(P_{t}g))$. Where $r_t>0$, the chain rule and (eq:F) give

Thus $r_t\le e^{-t}{r}_0$. If information becomes zero, the field is constant by Lemma lem:scalar and remains so.

For boundary-valued inputs apply the result to $(1-\eta )u$, then let $\eta \downarrow 0$ using continuity of finite sums. Correlation zero follows by taking the constant mean. Negative correlations follow from

and invariance of uniform averages under $y\mapsto -y$.

The hypothesis of Proposition 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 OpenAI119I,ChenGohariNair.

This semigroup acts on classical functions. No matrix-algebra Lindblad evolution is specified.

Let $f_{+},f_{-}$ be Boolean sections and $d_{\pm }=T_{\rho }{f}_{\pm }$ on the remaining cube. The exact recursion is

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 OpenAI119Induction,OpenAI119II. For $g_t=P_{t}f$, the elementary derivative underlying such a continuation is

whenever the field is interior. The identity follows from $H^{\prime }(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 OpenAI119Arithmetic. Their audit requires:

1. the complete parameter domain and every subdivision;

2. positivity of any cleared denominator;

3. nonnegative sides before squaring;

4. rigorous interval endpoints and series tails;

5. coverage of seams, singular limits, and all bias regimes;

6. the correct logical passage from the scalar estimates to the dimension-free assertion.

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 sec:finite instead belongs to our entirely specified sixteen-function instance.

The implication is a classical convexity statement, not an identification of the two functionals. We prove it in Section 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.

Fix

Order the cube as

The complete noise matrix is

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

Concavity of $H$ and mean preservation imply $\mathcal{L}(f)\ge 0$.

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 $\mathcal{L}$ and $\Gamma$.

Every Boolean function on ${\Omega }_2$ belongs to exactly one of the following four classes:

1. the two constants;

2. the four signed coordinates;

3. the two signed parity functions $\pm x_1{x}_2$;

4. the eight functions with one exceptional vertex, or their complements.

A representative of the last orbit is

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.

The complete representative calculation is:

These entries follow by multiplication by (eq:fourmatrix); no dimension induction is being used.

For the biased representative, the full three-atom posterior table is

This is a posterior law for this function, not a solution of the unrelated joining optimization (eq:joiningproblem).

Let $Q=100000$. The following strict enclosures hold:

Proof. For each row of the following table, both displayed residuals are positive integers:

Hence $a^2<k{Q}^2<b^2$. Taking nonnegative square roots and dividing by $Q$ proves the result.

Define

For every Boolean function $f:{\Omega }_2\to \{-1,1\}$, with $X$ uniform and independent symmetric noise of correlation $1/2$,

Equality holds if and only if

The gaps are exactly

In particular,

and every function that is not a signed coordinate satisfies

Proof. The representative tables and evenness of $H$ give every entry in (eq:gaptable). Lemma lem:orbits transfers them to all sixteen functions.

For parity, Lemma lem:roots gives

These bounds lie strictly between $102/1000$ and $103/1000$.

For the exceptional-vertex orbit, the same root enclosures give

and

The two numerators are, respectively, $87429$ and $87467$. Therefore

Since

this proves (eq:biasedgap).

For constants,

Thus every noncoordinate class has a strictly positive gap, and the coordinate class has gap zero. This proves the inequality, the equality classification, and (eq:uniformgap).

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.

The conversion below is the classical implication of Anantharam, Bogdanov, Chakrabarti, Jayram, and Nair ABCJN (Proposition 1). It is reproduced with all normalizations fixed.

Define

Then $\phi$ is increasing and convex, and

For $0\le a\le b\le 1$,

Proof. For $0<t<1$, put $v=\sqrt{1-t^2}$. Differentiation gives

Indeed,

Continuity extends monotonicity and convexity to the endpoints. The same inequality gives ${\phi }^{\prime }(t)\ge t/\ell$; integration proves (eq:conversionlower).

Finally, $\sqrt{1-H(u{)}^2}=|u|$, and binary entropy is symmetric about $1/2$. This proves (eq:conversionidentity).

Fix one Boolean function and one symmetric-noise experiment on a uniform cube. Write

If

then

More quantitatively, if

then

Proof. Concavity of $H$ gives $0\le b\le a\le 1$. Equation (eq:MI), (eq:conversionidentity), and Jensen's inequality imply

Put $\delta =a-b$. Convexity implies that an increment of length $\delta$ increases when its interval is shifted to the right. Hence

Here $s+\eta =1-\delta \in [0,1]$. Since

the assertions follow.

At $n=2$, $\rho =1/2$, and $\epsilon =1/4$,

for every Boolean $f$. Equality holds precisely for the four signed coordinates. Every other Boolean function satisfies

For the named parity comparison,

Proof. Apply Proposition prop:HtoI to Theorem thm:finite. For a noncoordinate function, $\eta =\Gamma (f)>27/1000$. By (eq:conversionlower),

Now $s_0>4/5$, by squaring, and $\ell ={{\int }_1}^{2}dt/t<1$. Consequently the information gap is strictly greater than

For a coordinate, (eq:MI) and $T_{1/2}{x}_i=x_i/2$ give the exact value $1-h_2(1/4)$. For parity, the posterior mean is $\pm 1/4$, giving $1-h_2(3/8)$.

This is a corollary of the finite Hellinger certificate. No all-dimensional information theorem has been imported.

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.

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 (eq:fourmatrix). Each of the $64$ seeds is equiprobable, so the joint table has denominator $64$.

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.

Fix the truth table $f$, the ideal kernel (eq:fourmatrix), and the score

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.

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

Then, with probability at least $1-\alpha$,

An additional calibration-failure probability $\beta$ enlarges the failure probability to at most $\alpha +\beta$.

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-\mathbb{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

Independence, exponential Markov inequality, and optimization over $t$ give

Taking $r=\sqrt{\ln (2/\alpha )/(2N)}$, then adding the model and rounding allowances, proves (eq:coverage). The calibration assertion is a union bound. This is Hoeffding's bounded-variable argument Hoeffding.

The proof discipline is comparable to Cheung's complete-record statistical interfaces in En01-B and En01-C CheungEn01B,CheungEn01C. Their physical statistics are not identified with the present score. A confidence interval does not prove a sharp constant: Theorem thm:finite is an exact calculation, while Proposition prop:coverage concerns repeated sampling under additional hypotheses.

The Cheung references in this table are scoped comparisons drawn from the supplied passages 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 Dossier119,Oai276Context.

The external general assertions name a sharp constant and an attaining example. The present certificate additionally prints:

1. all four input points and all transition probabilities;

2. an exhaustive partition of the sixteen Boolean functions;

3. every representative truth table and noised value;

4. a signed coordinate attaining equality;

5. parity and a biased noncoordinate function with exact gaps;

6. finite integer-square certificates for the numerical bounds;

7. the information implication and its normalization in bits.

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.

Let $S$ be a uniform sign, but prepare

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

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,

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.

For this example the posterior kernel is not (eq:kernel); Bayes' rule uses the changed input law.

Keep $X$ uniform on ${\Omega }_2$, but let the two noise signs be one common sign:

Each coordinate separately still has crossover $1/4$, but the flips are not independent. Then

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-\sqrt{3}/2$.

Marginal crossover probabilities do not specify the product noise model.

For a soft $u$, the conditional entropy $\mathbb{E}h(u)$ need not vanish. Replacing $\mathcal{I}(u)$ by $h(\mathbb{E}u)$ would erase that randomization cost and change the fixed-information problem.

Arbitrary output bias means that $m=\mathbb{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.

For a Walsh character of degree $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 thm:finite. Conversely, no nominated circuit-complexity theorem proves the Hellinger inequality.

Here is an explicit non-identification, used only as a comparison. For a qubit let

and

where $X$ is the Pauli bit flip. The two CPTP maps ${\mathcal{B}}_{\epsilon }$ and ${\mathcal{B}}_{\epsilon }\circ \Delta$ agree on every diagonal input. They therefore implement the same classical binary symmetric transition on computational-basis data.

Nevertheless,

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 CheungVIIIA,CheungVIIIB,CheungEn07A. The standard measure-and-prepare characterization is given in HSR.

Similarly, $H(t)$ is a classical affinity: for the two Bernoulli laws

one has

The fact that classical affinities admit diagonal-matrix representations does not prove an inequality for arbitrary noncommuting density operators, entangled inputs, or collective POVMs.

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 $\mathsf{N}$ 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 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 CheungI,CheungVIIIB,CheungEn07A.

No Page curve, island, horizon, Hawking-radiation derivation, gravity-generated entanglement, exclusion of classical gravity, or spacetime-emergence theorem is established.