Let \(M_{12,794}\) denote the requested maximum. The certified result is \[ 6{,}456{,}734{,}424\leq M_{12,794}\leq7{,}623{,}232{,}012. \] The lower endpoint is attained by the explicit initial segment in q12ns794-claim-lex-witness.

For the upper bound, put \(f=1_A\), \(\mu=794/4096\), and use the normalized Walsh coefficients \[ \widehat f(S)=2^{-12}\sum_x f(x)(-1)^{\sum_{i\in S}x_i}. \] The product kernel has Walsh eigenvalue \(4^{12-|S|}2^{|S|}\), hence \[ E(A)=8^{12}\sum_{S\subseteq[12]}2^{-|S|}\widehat f(S)^2. \] Parseval gives \(R:=\sum_{S\ne\varnothing}\widehat f(S)^2=\mu-\mu^2=655447/4194304\). If \(b(A)\) is the undirected edge boundary, then \[ D:=\sum_{S\ne\varnothing}|S|\widehat f(S)^2=\frac{b(A)}{2\cdot4096}. \] Harper's edge-isoperimetric theorem says that an initial binary segment maximizes the internal edges. At size 794 it has 3,693 internal edges, so every such \(A\) has \(b(A)\geq12\cdot794-2\cdot3693=2142\) and \(D\geq1071/4096\).

Convexity gives, for each integer \(1\leq k\leq12\), \[ 2^{-k}\leq\frac{12-k}{11}\,2^{-1}+\frac{k-1}{11}\,2^{-12}. \] Summing this inequality against the nonnegative Fourier weights and inserting the lower bound on \(D\) yields \[ E(A)\leq\frac{83{,}855{,}552{,}164}{11}=7{,}623{,}232{,}014+\frac{10}{11}. \] For even \(|A|\), the objective is divisible by four: modulo four, the diagonal contributes \(|A|\) and the paired off-diagonal terms contribute \(2\binom{|A|}{2}\), whose sum is \(|A|^2\). The largest multiple of four below the rational bound is 7,623,232,012.

The endpoints do not match. The exact maximum and the cube-automorphism orbits of its maximizers remain open in this certificate.

Index coordinates by \(i=0,\ldots,11\) and encode \(x\in\{0,1\}^{12}\) as \(\iota(x)=\sum_i2^i x_i\). The witness is \[ A_L=\{x:0\leq\iota(x)<794\}. \] Equivalently, its 4,096-bit characteristic integer is \(B_L=2^{794}-1\), where bit \(j\) records membership of the vertex with integer label \(j\). Its canonical 512-byte little-endian encoding has SHA-256 digest \[ \texttt{4f55e719c472514a6f2b2e657127780a0740471a7038205203f403f17988ba8a}. \] Direct ordered-pair summation and an independent Walsh transform both give \[ E(A_L)=6{,}456{,}734{,}424. \] The family is also the disjoint union of binary subcubes corresponding to \(794=512+256+16+8+2\). Coordinate permutations and coordinate complements preserve the objective, so the full cube-automorphism orbit of this family gives witnesses with the same value.

The family \[ H_4=\{x\in\{0,1\}^{12}:|x|\leq4\} \] has size \(\sum_{j=0}^4\binom{12}{j}=794\). Direct summation and the Walsh calculation give \[ E(H_4)=5{,}884{,}957{,}476. \] Thus \(E(A_L)-E(H_4)=571{,}776{,}948\). A vertex-isoperimetric or small-diameter preference for Hamming balls cannot settle this weighted objective. The ball has 2,784 internal cube edges and boundary 3,960, while the initial segment has 3,693 internal edges.

Harper's 1966 paper proves the binary-cube edge-isoperimetric theorem used here. Bonami's 1970 work and Beckner's 1975 paper provide the classical analytic setting for Fourier and noise inequalities on product spaces. Kündgen's 2002 paper studies minimum average Hamming distance, which is equivalent to maximizing the level-one Walsh weight. It records the broader Ahlswede-Katona problem and shows why controlling only a distance moment is a separate extremal question.

The audit searched these lines of work and exact finite noise-stability optimization. No located primary source states the maximum of \(\sum_{x,y\in A}3^{12-d_H(x,y)}\) for \(|A|=794\), and no source classifies its maximizers. This records the search outcome and makes no novelty claim.

A complete continuation can encode \(1_A\) as 4,096 binary variables with the exact cardinality equation and optimize the positive quadratic form \(x^TKx\), where \(K_{uv}=3^{12-d_H(u,v)}\). A branch-and-bound result becomes a proof when every node carries a rational dual upper bound whose maximum is at most the incumbent, with the complete node log and solver-checkable dual data preserved. A symmetry-aware alternative uses the cardinality ideal \(\sum x_u=794\), the Boolean equations \(x_u^2=x_u\), and cube-invariant semidefinite moment constraints. A rational sum-of-squares dual matching 6,456,734,424 would prove optimality. Once equality is certified, canonical labeling under the group \(C_2^{12}\rtimes S_{12}\) can enumerate the maximizing orbits.

The program constructs the initial segment and Hamming ball from their definitions. For each family it evaluates all ordered pairs directly. It then performs an unnormalized fast Walsh transform and applies the exact kernel eigenvalues \(4^{12-k}2^k\). Equality of the two answers catches distance-counting and normalization errors.

The program counts internal edges, evaluates Harper's extremal count \(\sum_{j=0}^{793}\operatorname{popcount}(j)=3693\), and carries the secant calculation with rational arithmetic. The printed upper integer incorporates the divisibility-by-four argument given in the interval claim. The verifier checks a calculation derived from Harper's theorem. It does not enumerate all subsets of size 794.