Entropy

Abstract

The full bosonic attenuator and the coherent-state output-entropy question.

Balanced Fock-two determinant and entropy argument. Use the actual channel Phi and completed-space coefficient matrix C_a from the Attenuator narrative, with the evidence status stated there. The reference spectrum is lambda_star=(1/2,1/4,1/4), and its moment is b_star(q)=2^(-q)+2*4^(-q). Thus b_star(1)=1, b_star(2)=3/8, e2_star=5/16, e3_star=1/32 and S_star=(3/2) log 2, in nats. All comparisons here use this normalized reference moment. The determinant reduction below is conditional on e3>=1/32 for the same actual output for which purity<=3/8. The rank-three calculation supplies these bounds within its classified class, while the universal e3 premise remains open.

Countable Fredholm determinant. Let sigma be any positive trace-class density with countable eigenvalues lambda_i>=0 and sum_i lambda_i=1. For t>=0 define D_sigma(t)=product_i(1+t lambda_i). Since 0<=sum_i log(1+t lambda_i)<=t, the product is finite and well defined. Finite products increase to it. Expand each finite product, then use nonnegative convergence over increasing finite subsets to obtain D_sigma(t)=sum_{k>=0} e_k(sigma)t^k, with e0=1 and e_k the sum of products over increasing k-tuples. Expanding (sum_i lambda_i)^k shows k! e_k<=1, so the series converges absolutely and locally uniformly. This includes zero eigenvalues and infinite rank. Since e2=(1-Tr(sigma^2))/2, purity<=3/8 gives e2>=5/16. If also e3>=1/32, every higher e_k is nonnegative, hence D_sigma(t)>=1+t+(5/16)t^2+(1/32)t^3=(1+t/2)(1+t/4)^2=D_star(t) for every t>=0. Both premises must hold simultaneously on this sigma; separate attainable extrema do not suffice.

Moment integral with all endpoints justified. For 1<q<2 put c_q=q sin(pi(q-1))/pi>0. For x>=0, x^q=c_q integral_0^infinity (t x-log(1+t x)) t^(-q-1) dt. At x=0 both sides vanish. For x>0 substitute u=t x and integrate by parts: the integral at x=1 is (1/q) integral_0^infinity u^(1-q)/(1+u) du=pi/(q sin(pi(q-1))). The boundary terms vanish because u-log(1+u)=O(u^2) at zero and O(u) at infinity. Each integrand is nonnegative. Tonelli therefore permits summation over the countable spectrum and gives Tr(sigma^q)=c_q integral_0^infinity (t-log D_sigma(t)) t^(-q-1) dt. Moreover 0<=t-log D_sigma(t)<=min(t^2/2,t), using y-log(1+y)<=y^2/2 and sum lambda_i^2<=1. This bounds both endpoints and needs neither finite rank nor finite entropy. Determinant domination reverses the log-integral comparison and yields Tr(sigma^q)<=b_star(q) for every 1<q<2. The q=2 comparison is the separate purity premise.

Finite Sra mechanism and its scope. Suvrit Sra, Logarithmic inequalities under an elementary symmetric polynomial dominance order, https://arxiv.org/html/1509.05902v2, equation (1.1), distinguishes prec_E (equal top coefficient) from preceq_E (inequality also at the top). Proposition 2.1 and equations (2.1)-(2.2) give the finite log-integral mechanism. Theorem 2.3, equation (2.7), is stated with prec_E; its equal-trace logarithmic proof gives the weaker-order implication used here, or the finite vectors may be padded by a zero to make the top coefficients equal. Proposition 2.4 is for finite positive-definite matrices. Credit for that finite mechanism belongs to Sra. The preceding nonnegative-product and Tonelli argument supplies the needed countable noninvertible extension directly, rather than attributing an infinite trace-class theorem to those finite statements.

A common sequence gives extended entropy. Choose q_j=1+1/j for all inputs, j>=2, and put t=1/j. For 0<lambda<=1, (lambda-lambda^(1+t))/t=lambda integral_0^(-log lambda) exp(-t u) du increases to -lambda log lambda as t decreases to zero; the value for lambda=0 is zero. Monotone convergence gives S_spectral(sigma)=lim_j (1-Tr(sigma^(1+1/j)))/(1/j), including +infinity. The moment comparison gives each quotient at least (1-b_star(1+t))/t, whose limit is (3/2) log 2. Thus the conditional determinant premises imply the extended entropy bound without differentiating an infinite trace at q=1 or imposing finite entropy. An input-dependent choice of q is not the common-sequence assertion needed for a uniform pure-to-mixed moment argument.

Relation to the actual source entropy. The source defines basisEntropy as an ENNReal-valued countable diagonal sum and vonNeumannEntropy as its infimum over complete countable Hilbert bases. To identify it analytically with the extended spectral sum, take an orthonormal eigenbasis, completed in the kernel, and any other basis b_j. Its diagonal probabilities are p_j=sum_i lambda_i |<b_j,e_i>|^2. The weights in each row are a subprobability distribution if only positive eigenvalues are listed; fill the remainder with eigenvalue zero. Concavity of h(x)=-x log x on [0,1], with h(0)=0, gives h(p_j)>=sum_i |<b_j,e_i>|^2 h(lambda_i), first for finite subcollections with a tail average and then by the countable limit. Tonelli and the Parseval column sums give sum_j h(p_j)>=sum_i h(lambda_i), with extended values allowed. An eigenbasis attains equality, so the basis infimum is exactly spectral entropy. Entropy.finiteDiagonal_entropy proves the finite diagonal case; the general countable spectral/ENNReal equivalence remains an explicit formal interface obligation. Existing unitary invariance comes from transporting the whole set of Hilbert bases, as used in PhaseCovariantAttenuatorCoherentRefutation.result.

The purity premise has an all-density analytic derivation. Use chi_rho(z)=Tr(rho D(z)) and Weyl Parseval with measure d^2z/pi. For the balanced channel chi_Phi(rho)(z)=chi_rho(z/sqrt(2)) chi_|2>(z/sqrt(2)). Let tau be the difference-mode marginal after applying the actual balanced beam splitter to rho tensor rho. Since chi_rho(-z)=conj(chi_rho(z)), chi_tau(sqrt(2)z)=|chi_rho(z)|^2. Also chi_|2>(z)=exp(-|z|^2/2)L_2(|z|^2). After z=sqrt(2)w and then u=sqrt(2)w, Parseval writes purity as the pairing of chi_tau(u) with exp(-|u|^2/2)L_2(|u|^2/2)^2. The exact identity L_2(y/2)^2=(3/8)L_0(y)+(1/4)L_2(y)+(3/8)L_4(y) identifies this pairing as Tr(tau A_2), where A_2=(3/8)(|0><0|+|4><4|)+(1/4)|2><2|. Hence 0<=A_2<=(3/8)I gives Tr(Phi(rho)^2)<=3/8 for every density. Trace-class Weyl/Parseval identities and Gaussian-polynomial integrability justify this calculation without an energy assumption. This is an analytic argument requiring formalization, not a claimed frozen universal Fock-two purity theorem and not a consequence attributed to the vacuum-interference paper.

Exterior cube, minors and the exact sixth-degree residual. Set A=||a||2^2=||C_a||HS^2 and C=C_a. On the orthonormal exterior basis indexed by increasing triples, e3(C C^*)=||wedge^3 C||HS^2=sum{|I|=|J|=3}|det C[I,J]|^2=(A^3-3A||C||(S4)^4+2||C||(S6)^6)/6. There is no extra factor 3!. In a finite matrix these identities follow from singular values, Cauchy-Binet and Newton identities: writing p1=A, p2=||C||(S4)^4 and p3=||C||(S6)^6 gives 6e3=p1^3-3p1p2+2p3. For finite matrix projections converging to C in S2, the exterior products converge in Hilbert-Schmidt norm by multilinearity and the bound on their tensor products. The finite minor sums increase to the full nonnegative sum; continuity of S4 and S6 gives the displayed completed-space identities, with e3<=A^3/6. Thus ||wedge^3 C_a||_HS^2>=||a||2^6/32 is exactly equivalent to 2||C_a||(S6)^6-3||a||2^2||C_a||(S4)^4+(13/16)||a||_2^6>=0. It is sufficient for the entropy route, and is not proved here for all a in l2. Positivity alone supplies e3>=0, not the required constant.

Finite-to-completed and pure-to-mixed bridges retain the physical map. For arbitrary l2 truncations a_N, the coefficient isometry gives C_(a_N)->C_a in S2. Since ||T||(Sp)<=||T||(S2) for p>=2, the homogeneous S4/S6 expression is continuous. A finite-support theorem for that exact homogeneous inequality would therefore extend to every completed-Fock pure input; a numerical cutoff or a collection of finite examples is not such a theorem. For a fixed common q>1, suppose every normalized pure input satisfies Tr(Phi(|psi><psi|)^q)<=b_star(q). If rho=sum_k w_k |psi_k><psi_k| is its countable spectral decomposition, channel linearity and trace-norm continuity identify Phi(rho)=sum_k w_k Phi(|psi_k><psi_k|). The Schatten-q triangle inequality gives ||Phi(rho)||_Sq<=sum_k w_k ||Phi(|psi_k><psi_k|)||_Sq<=b_star(q)^(1/q), using partial sums and their trace-norm limit. Raising to q gives the mixed moment bound. The same q values must work for all pure inputs before the common sequence is used. This argument assumes neither convexity nor concavity of e3 and does not infer a mixed e3 lower bound from a pure e3 theorem.

Exact symmetric coefficients for every noncoherent rank-three pure input. In the physical compression of Attenuator set x=r^2, Z=x^2+4x+2, P=x^3+6x^2+9x+3, s=(x+1)/sqrt(2), u=x/(2sqrt(x+1)), v^2=P/(4(x+1)), T=u^2+v^2=(x^2+6x+3)/4. Directly, Tr B^2=s^2+2T=Z, det B=s v^2!=0, e2(B^2)=T^2+2s^2v^2 and e3(B^2)=s^2v^4=P^2/32. For example the second identity follows by squaring the pairwise products of the real eigenvalues mu_i: (sum_{i<j} mu_i mu_j)^2-2(sum_i mu_i)(product_i mu_i)=T^2+2s^2v^2. Divide by Z^2 and Z^3 respectively to obtain e2=5/16+(2x^2+4x+1)/(16Z^2) and e3=1/32+(2x^3+9x^2+6x+1)/(32Z^3). The numerator identities are 16(T^2+2s^2v^2)-5Z^2=2x^2+4x+1 and P^2-Z^3=2x^3+9x^2+6x+1. Both excesses are strictly positive for every finite x>=0, including x=0. These coefficients come from the actual physical C C^* and its orthogonal compression, not from a proposed spectrum.

Strict entropy and the pure equality cases. For two rank-three densities of equal trace, the scalar log-integral identity gives S(sigma)-S_star=integral_0^infinity log(D_sigma(t)/D_star(t)) dt/t^2. It may be derived first by integrating the scalar identity for each of the six eigenvalues and cancelling the equal-trace linear terms. At zero the numerator is O(t^2); at infinity it tends to the finite constant log(e3/e3_star), so the integral converges. The strictly positive e2 and e3 excesses above imply D_sigma(t)>D_star(t) for every t>0. Every noncoherent rank-three pure input therefore has S(Phi(|f><f|))>(3/2) log 2. A coherent input is a displaced vacuum input and has spectrum (1/2,1/4,1/4), so it attains equality. The limit r->infinity approaches the coherent spectrum but gives no further equality case at finite r.

Countable mixtures with output rank three. A source DensityOperator is positive trace class: its trace_one diagonal condition says that the positive square root has squared Hilbert-Schmidt norm one. The compact spectral theorem gives rho=sum_k w_k |psi_k><psi_k| with orthonormal psi_k, w_k>0 and sum_k w_k=1. Let sigma=Phi(rho) have three-dimensional support S. For any y perpendicular to S, 0=<y,sigma y>=sum_k w_k <y,Phi(|psi_k><psi_k|)y>. Each summand is nonnegative, so each vanishes. For a positive operator vanishing quadratic form means that its square root annihilates y; hence every component output is supported in S. The pure minimum-rank result makes every component rank exactly three. On this fixed finite-dimensional support entropy is continuous. Apply finite concavity to the first N weighted components and the normalized remaining tail, then let N grow: S(sigma)>=sum_k w_k S(Phi(|psi_k><psi_k|))>=S_star. If equality holds, no positive-weight term can have the strict noncoherent excess. Every spectral vector must be coherent. But distinct normalized coherent vectors have inner-product modulus exp(-|alpha-beta|^2/2)>0, whereas the psi_k are orthogonal. Only one spectral term is possible. Equality in the entire output-rank-three density class is exactly a pure coherent input. The same positive-support argument excludes output rank below three for any density.

Boundary on a possible counterexample. For an arbitrary density, group the tail of its spectral decomposition into one normalized state, apply finite entropy concavity and discard its nonnegative entropy contribution. Letting the finite subset grow gives S(Phi(rho))>=sum_k w_k S(Phi(|psi_k><psi_k|)), including extended values. This uses neither finite entropy nor a finite-dimensional output assumption. If a density violated S_star, at least one positive-weight pure spectral component would violate it. The rank-three result forces that component to have output rank at least four, possibly infinite. This is only a necessary boundary on a counterexample: it asserts neither a counterexample nor a finite-rank minimizer, and it does not reduce the open all-input problem to a finite cutoff.

Residual and compatibility with the resolvent obstruction. The remaining global obligation for this determinant route is the same-map bound e3(C_a C_a^*)>=||a||_2^6/32 for all completed-Fock vectors, or a different valid all-input entropy argument. Failure of this stronger sufficient premise would not by itself refute entropy or exclude a different common good-q sequence. For K_sigma(s)=sum_i lambda_i^2/(lambda_i+s) and L_sigma(t)=log D_sigma(t), termwise nonnegative convergence gives L_sigma’(t)=sum_i lambda_i/(1+t lambda_i)=1-K_sigma(1/t). An inequality for L does not imply an inequality for its derivative. Thus the existing physical pointwise-resolvent obstruction is compatible with determinant domination and is neither a moment nor an entropy counterexample. The earlier M1 fractional-moment gap keeps its factor q-1; this argument does not revive a pointwise-resolvent premise, assume lambda_max<=1/2, choose input-dependent q values, or use finite-cutoff extrapolation. Existing finite compound-matrix/Cauchy-Binet, Newton-identity and positive-Fredholm-product facts are reusable ingredients; they do not establish the full countable bridge or the universal physical sixth-degree inequality. No new theorem declaration, theorem Describe, Reg wrapper, freeze, deposit or ledger outcome is asserted by this exposition.

Reference moment and evidence boundary. The expression b(q)=2^(-q)+24^(-q) gives b(1)=13/24 and cannot be the moment of a trace-one density. The reference used throughout is b_star(q)=2^(-q)+2*4^(-q), with the multiplicity two explicit. This reference, the shifted root beta-conj(alpha), and the distinction between finite Sra statements and the countable argument above are part of the source-assessed result. All new arguments below have the same pending-formalization status; no new kernel theorem or named-problem resolution is claimed.

Recovering the low invariant-sector scalars from the actual channel. Write s=||a||^2, p_j=Tr((C_a C_a^)^j), and G(a)=e3(C_a C_a^)-s^3/32, so 6G=2p3-3s p2+(13/16)s^3. For a=e0+epsilon eN, put A=C_e0 and B=C_eN. A02=A20=1/2 and A11=-1/sqrt(2), all other entries zero. For real epsilon the matrix A+epsilon B is real symmetric, so p2=Tr(A+epsilon B)^4 and p3=Tr(A+epsilon B)^6. For complex epsilon the physical formula is sigma=C C^*, and these real-symmetric trace shortcuts must not be applied literally. Instead number-phase covariance from Attenuator removes the phase of epsilon, giving the same coefficients in |epsilon|^2. For N>=3, B has zero compression to indices {0,1,2}, hence ABA=0. If beta_i=B[i,N+2-i]^2, i=0,1,2, expansion of the actual creation polynomial gives beta0=(N+2)(N+1)/2^(N+3), beta1=(N+1)(N-2)^2/2^(N+3), and beta2=(N^2-5N+2)^2/2^(N+4). The quadratic coefficients U=[|epsilon|^2]p2 and W=[|epsilon|^2]p3 are U=beta0+2beta1+beta2 and W=(3/8)(beta0+beta2)+(3/2)beta1. At N=2 the extra B22=-1/2 must be retained: Tr(A^2B^2)=5/32, Tr(ABAB)=0, Tr(A^4B^2)=5/128, Tr(A^3BAB)=0 and Tr(A^2BA^2B)=1/64. Thus U2=5/8 and W2=6(5/128)+3(1/64)=9/32. The resulting (N,U,W,[|epsilon|^2]G) rows are (2,5/8,9/32,0), (3,9/16,33/128,3/128), (4,9/16,21/64,3/64), and (5,19/32,195/512,25/512), using [|epsilon|^2]G=(2W-3U+21/16)/6.

Extracting every low invariant line. The coefficient of epsilon in the physical tensor cube is S_N=sum_i x_i^N/sqrt(N!), including all three ordered-copy placements. In the center and relative coordinates of Attenuator, sum_i x_i^2=t^2+h2; sum_i x_i^3=t^3/sqrt(3)+sqrt(3)t h2+3h3; sum_i x_i^4=t^4/3+2t^2h2+4sqrt(3)t h3+h2^2/2; and sum_i x_i^5=t^5/(3sqrt(3))+10t^3h2/(3sqrt(3))+10t^2h3+5t h2^2/(2sqrt(3))+(5/2)h2h3. Factorial norms, including ||h2||^2=4, give the squared norms of the relative components at M=(0,2,3,4,5): for N=2, (1,2,0,0,0); for N=3, (1/3,2,2/3,0,0); for N=4, (1/9,4/3,8/9,2/3,0); for N=5, (1/27,20/27,20/27,10/9,10/27). Each row sums to 3. The vacuum has G=0 and the scalar lambda0=1/32. Q preserves total degree, so the second-order perturbation has no pairing with the degree-zero cube. Combining the preceding rows with the physical G coefficients successively gives delta2=0, (2/3)delta3=3/128, (8/9)delta3+(2/3)delta4=3/64, and (20/27)delta3+(10/9)delta4+(10/27)delta5=25/512, where deltaM=lambdaM-1/32. Therefore (lambda0,lambda2,lambda3,lambda4,lambda5)=(1/32,1/32,17/256,7/128,23/1024), and (delta3,delta4,delta5)=(9/256,3/128,-9/1024). These scalars apply to the invariant lines, not all vectors in each full relative sector.

An exact obstruction to the stronger operator and holomorphic-cubic SOS routes. The symmetric vector phi=(3/8)h2h3 with center vacuum has norm one and <phi,(Q-I/32)phi>=-9/1024. In unit symmetric tensor coordinates indexed in order by (5,0,0),(4,1,0),(3,2,0),(3,1,1),(2,2,1), it is (sqrt(10),-5,sqrt(2),4sqrt(2),-2sqrt(3))/9; its squared coordinate norms sum to (10+25+2+32+12)/81=1. It cannot be an actual tensor cube: if a_k is nonzero, the coefficient at (k,k,k) of a tensor3 is a_k^3 and has total degree 3k, whereas phi is homogeneous of degree five. This argument also excludes infinite-support cubes. On span{e0,…,e5}, for amplitude multi-index alpha of sum three, let m_alpha=3!/product_i alpha_i! and v_alpha(a)=sqrt(m_alpha)a^alpha. The multiplicities are 1 for a_i^3, 3 for a_i^2a_j with distinct labels, and 6 for three distinct labels. On the five listed coordinates v=(sqrt(3)a0^2a5,sqrt(6)a0a1a4,sqrt(6)a0a2a3,sqrt(3)a1^2a3,sqrt(3)a1a2^2). The Hermitian Gram matrix of G in these normalized cubic coordinates is uniquely the restriction of Q-I/32: the coefficient of conjugate(a)^alpha a^beta is sqrt(m_alpha m_beta) times the corresponding matrix entry, and these mixed monomials are linearly independent after the invertible change a=x+iy, conjugate(a)=x-iy. A representation as a sum of squared absolute values of holomorphic homogeneous cubics would make that matrix positive semidefinite, contradicting phi. This refutes that SOS representation and positivity on the larger symmetric space. It refutes neither nonnegativity on physical cubes nor a real or nonholomorphic SOS. Indeed the actual family e0+epsilon e5 has G=(25/512)|epsilon|^2+O(|epsilon|^4), positive near zero.

Exact positive swap terms. For retained-output permutations pi define T_pi as the environment expectation of the three-splitter conjugate of U_pi. The antisymmetrizer gives 6Q=I-T12-T13-T23+T123+T132, with T132=T123^*. Each term factors identically on the center and preserves relative degree. For a transposition use the pair-difference mode d=(x_i-x_j)/sqrt(2): swapping retained outputs is parity on their difference mode. In the pinned convention the one-particle splitter matrix is B=[[1,-1],[1,1]]/sqrt(2), and B^T diag(-1,1)B=[[0,1],[1,0]]. Thus the conjugated parity positively interchanges the input and environment difference modes. The pair environment |2,2> becomes (b^4-2b^2d^2+d^4)/8 in its normalized center/difference coordinates b,d; its orthogonal occupation probabilities are 3/8,1/4,3/8 at d-degrees 0,2,4. Consequently T_ij=(3/8)P_(d,0)+(1/4)P_(d,2)+(3/8)P_(d,4), with identity on other modes. The even environment would give the same term under an explicitly different environment-phase convention. In particular 0<=T_ij<=(3/8)I, also recovering the physical purity bound by the two-copy swap identity.

A uniform high-relative-degree bound with every environment block included. For fixed M>=64, let P_j project onto occupations n=0,2,4 along pair-difference axis u_j, with M-n along its orthogonal relative axis v_j. Distinct pairs have |<v_j,v_k>|=1/2. Between normalized n,m occupations each bra/ket placement pair has at least M-n-m v-to-v positions, so each overlap entry is bounded by sqrt(binomial(M,n)binomial(M,m))2^(-M+n+m)<=(M+1)^4 2^(-M+8). Taking the norm of the 3 by 3 overlap matrix gives ||P_jP_k||<=epsilon_M=768(M+1)^4 2^(-M). The Gram operator for the three range inclusions has diagonal I and off-diagonal norms at most epsilon_M; its quadratic form is bounded by (1+2epsilon_M)sum_j ||z_j||^2. Therefore ||P1+P2+P3||<=1+2epsilon_M and T12+T13+T23<=(3/8)(1+2epsilon_M)I.

Cycle compression and the tail constant. A three-cycle is a real rotation R of order three on the relative one-particle plane. Its splitter-conjugated input-input block is (I+R)/2, of norm 1/2; all other blocks are contractions. More generally, for a one-particle unitary on X direct_sum Y with input-input block norm at most r<=1, its second quantization compressed from M X-photons and d Y-photons back to those occupations has norm at most binomial(M+d,d)r^(M-d), for M>=d. The normalized symmetric embedding is the sum over N=binomial(M+d,d) orthogonal placements of the Y slots, divided by sqrt(N). Every bra/ket placement pair has at least M-d X-to-X slots, so its operator norm is at most r^(M-d). There are N^2 terms with prefactor 1/N, proving the bound even for entangled vectors in the symmetric tensor factors. Contract against each positive d-block of the relative environment using a spectral decomposition; its norm is bounded by the compression norm times that block’s trace. Summing all trace weights, with every d=0,…,6 included, gives ||T123 restricted to M||<=gamma_M=64(M+6)^6 2^(-M). No product assumption on the relative environment is used.

Exact uniform threshold and its scope. At M=64, epsilon64<2^(-26) follows from 768<2^10 and 65<2^7, while gamma64<2^(-16) follows from 70<2^7. The successive ratios ((M+2)/(M+1))^4/2 and ((M+7)/(M+6))^6/2 decrease. At 64 their base ratios 66/65 and 71/70 are both less than 11/10, and the integer inequalities 11^4<210^4 and 11^6<210^6 show both ratios are below one. Hence these bounds hold for every M>=64. The self-adjoint cycle pair is bounded below by -2gamma_M I, so q_M>=[5/8-(3/4)epsilon_M-2gamma_M]I/6>=I/12, because (3/4)2^(-26)+2^(-15)<1/8. Thus q_M-I/32>=(5/96)I on the entire relative sector for every M>=64. This controls an infinite tail; it imposes no finite photon support on the competing input and gives no sign for each middle sector.

A physical counterexample to deleting the middle sectors. Define L(a)=(9/256)||F_{a,3}||^2+(3/128)||F_{a,4}||^2-(9/1024)||F_{a,5}||^2, and let R_tail be the actual gap contribution of all M>=64. The proposed shortcut L(a)+R_tail(a)>=0 for all physical cubes is false. Take a=e0+epsilon e14. For the more general e0+epsilon eN with N>=5, the coefficient of epsilon in F_a is S_N=sum_i(c+r_i)^N/sqrt(N!), with all three placements. Its degrees M=3,4,5 are 3binom(N,3)c^(N-3)h3/sqrt(N!), (1/2)binom(N,4)c^(N-4)h2^2/sqrt(N!), and (5/2)binom(N,5)c^(N-5)h2h3/sqrt(N!). Combining these with the weighted center and relative norms gives their squared-norm coefficients w3=N(N-1)(N-2)/3^(N-1), w4=N(N-1)(N-2)(N-3)/(43^(N-2)), and w5=N(N-1)(N-2)(N-3)(N-4)/(43^(N-1)). Thus [|epsilon|^2]L=9N(N-1)(N-2)(-N^2+15N-20)/(40963^(N-1)). At N=14 the polynomial factor is -6 and this coefficient is exactly -91/(2563^9).

Existence, normalization and the vanishing tail in that physical example. The epsilon, epsilon^2 and epsilon^3 parts of F_(e0+epsilon e14) have total photon degrees 14,28,42. At fixed relative degree their center monomials have distinct degrees and are orthogonal. Therefore L=-91|epsilon|^2/(256*3^9)+O(|epsilon|^4), a finite polynomial in |epsilon|^2 with negative first coefficient. It is strictly negative for all sufficiently small nonzero epsilon. The whole tensor cube has total degree at most 42, hence F_{a,M}=0 for every M>=43, including the entire M>=64 tail. This refutes the shortcut with its actual tail and also with the nonnegative tail lower bound. Normalizing a by sqrt(1+|epsilon|^2) multiplies every degree-six gap contribution by (1+|epsilon|^2)^(-3), preserving the strict violation. No numerical search or chosen numerical epsilon is needed. In weighted differential-polynomial form it says (1/16)||P5||_3^2>(1/64)||P3||_3^2+(3/2)||P4||_3^2 for these actual Bargmann functions near epsilon=0, despite fP5=fP4’-3f’P4. It makes no assertion for every epsilon.

The same physical family has a positive full gap near zero. For A=C_e0 and B=C_e14, A^2 has diagonal (1/4,1/2,1/4) and A^4 has diagonal (1/16,1/4,1/16) on indices 0,1,2. B has total index sum 16, so its compression there is zero and ABA=0. Its physical squared entries are beta0=1615/2^17=15/8192, beta1=1512^2/2^17=135/8192, and beta2=264^2/2^17=1/16. For real epsilon the cyclic trace word classes give U=4Tr(A^2B^2)+2Tr(ABAB)=797/8192 and W=6Tr(A^4B^2)+6Tr(A^3BAB)+3Tr(A^2BA^2B)=3201/65536; ABA=0 eliminates the nonadjacent classes. At zero p2=3/8 and p3=5/32. Writing q=|epsilon|^2 and s=1+q, the coefficient of q in G is (2W-3U+21/16)/6=(6402-19128+86016)/(665536)=12215/65536. For complex epsilon use C_(D_theta a)=exp(-2i theta)D_theta C_a D_theta and sigma_(D_theta a)=D_theta sigma_a D_theta^, which remove the phase of epsilon while preserving the moments. Consequently G(e0+epsilon e14)=(12215/65536)|epsilon|^2+O(|epsilon|^4)>0 for all sufficiently small nonzero epsilon. The normalized family has the same first coefficient and the overall factor (1+q)^(-3). At quadratic order only relative degrees at most 14 occur; degrees 0,2 have zero gap and degree 1 is absent. The aggregate contribution of M=6,…,14 therefore has coefficient 12215/65536+91/(2563^9)>0, compensating the negative low-sector term. This aggregate fact assigns no sign to each middle-sector form. No global sign for this family follows.

The exact remaining same-function inequality over the full completed domain. The low-sector scalars and the norm identities of Attenuator give, for every complex l2 vector including zero, G(a)=(1/64)||P3||3^2+(3/2)||P4||3^2-(1/16)||P5||3^2+R_mid(f)+R_tail(f). Here R_mid=sum{M=6}^{63}<F{a,M},(I_center tensor(q_M-I/32))F{a,M}>, and R_tail is the same sum over every M>=64. Since sum_M ||F_{a,M}||^2=||a||^6 and 0<=Q<=I implies ||Q-I/32||<=31/32, the full gap series converges absolutely. The tail satisfies R_tail>=(5/96)sum_{M>=64}||F_{a,M}||^2. Every middle sector M=6,…,63 and its unrestricted center dependence remains present. Their matrices and individual signs are not all computed here. Even computing those finite matrices would leave a same-function compatibility problem over arbitrary entire f, not a finite input cutoff. The unresolved sufficient inequality is (1/16)||P5||_3^2<=(1/64)||P3||_3^2+(3/2)||P4||_3^2+R_mid(f)+R_tail(f), for all such f. The physical example proves that deleting R_mid is invalid. The identity fP5=fP4’-3f’P4 alone provides no integrated norm inequality that closes it. A joint estimate retaining these terms, a genuine full-G witness, or a different all-input entropy argument is still required. Neither obstruction refutes the universal physical e3 premise; even a future full-G counterexample would reject this sufficient determinant route without itself refuting entropy. The all-density balanced n=2 entropy target and the all-n/all-eta Conjecture 1 remain open.

Purity rigidity and stability on completed Fock space. Throughout this argument Phi is exactly the balanced channel with environment |2><2| identified in Attenuator, a is a unit vector in complex l2, sigma_a=Phi(|a><a|)=C_a C_a^*, d(a)=3/8-Tr(sigma_a^2), and m(a)=sup_alpha |<D(alpha)e0,a>|^2. The Bargmann normalization is ||f||^2=integral_C |f(z)|^2 exp(-|z|^2)d^2z/pi, with e_n(z)=z^n/sqrt(n!). The conclusions below hold for arbitrary completed vectors, including infinite support and infinite mean photon number. They are analytic arguments pending formalization. The purity maximum, bounded copy kernel and exact coherent equality class are literature-attested: Zixuan He, The energy cost of optical noise, version 1.0, 25 October 2026, DOI 10.5281/zenodo.23629201, Theorem 8, equations (38),(40), Appendices D,E.2,F. In that theorem n=2 gives the maximum 3/8 over every normal density and equality precisely for coherent pure inputs. The following argument includes this specialization as a prerequisite for the quantitative bounds, without claiming priority for it.

The full two-copy identity. Let R2 implement the orthogonal substitution (x1,x2)=((t+u)/sqrt(2),(t-u)/sqrt(2)), and write P_j=|e_j><e_j| on the relative mode. The positive swap calculation above, with its positive interchange in the actual splitter convention, gives B=(3/8)P_0+(1/4)P_2+(3/8)P_4 and T=R2^(I tensor B)R2. For every normal density rho, Tr(Phi(rho)^2)=Tr((rho tensor rho)T). This is an operator compression of retained-copy swap before specializing the signal; knowing only its values on identical pure tensor squares would not justify the mixed-state formula. Finite occupation identities extend by trace-norm continuity of the normal channel, tensoring and pairing with the bounded swap. Equivalently, the source square-root columns sqrt(rho)e_j give a rank-one sum equal to rho in trace norm. Thus the formula applies to the actual attenuatorOperator on off-diagonal and infinite-rank densities as well as its pure specialization. Put D=(3/8)I-B and Aop=R2^(I tensor D)R2. Then d(a)=<a tensor a,Aop(a tensor a)>, D>=0, ||Aop||=3/8, ker D=span{e0,e4}, and D>=(I-P_0-P_4)/8. The relative e2 eigenvalue is 1/8; the other nonzero eigenvalues are 3/8. He equation (40) gives the same three weights as the n=2 case of binomial(2k,k)binomial(2n-2k,n-k)/4^n.

Exact equality, with zeros included. The normalized relative e2 coefficient of R2(f tensor f) is g2(t)=(ff’‘-(f’)^2)(t/sqrt(2))/sqrt(2). Hence d(a)=0 implies ff’‘-(f’)^2=0 identically. For any nonzero entire f satisfying this identity, a zero z0 of multiplicity r>=1 would give f(z)=c(z-z0)^r+O((z-z0)^(r+1)), c!=0, and ff’‘-(f’)^2=-r c^2(z-z0)^(2r-2)+O((z-z0)^(2r-1)), a contradiction. Thus f is zero-free. The entire function f’/f has zero derivative, so f=C exp(beta z). Conversely every such exponential has relative vacuum in its tensor square. Unit norm fixes |C|=exp(-|beta|^2/2), proving d(a)=0 if and only if a is a phase multiple of D(beta)e0. More generally, for every nonzero completed Bargmann vector, g2=0 if and only if f is a scalar exponential. The derivatives here are derivatives of entire functions; neither f’ nor f’’ is required to lie in Fock space. The vector g2 itself lies there because it is a bounded orthogonal projection. This is the missing-relative-degree-two argument of He Appendix F, with an explicit zero-multiplicity proof.

The auxiliary three-copy projection estimate. Let R3 be the Gaussian-norm-preserving coordinate unitary defined by t=(x1+x2+x3)/sqrt(3), u=(x1-x2)/sqrt(2), v=(x1+x2-2x3)/sqrt(6), and let copy permutations act after transport by R3. Let P retain u-occupations 0 and 4, with every t,v coefficient, and let P_* retain joint relative vacuum in u,v with every center coefficient. For every vector Psi invariant under this transported S3 action, ||(I-P)Psi||^2>=gamma(||Psi||^2-||P_*Psi||^2), gamma=(4-sqrt(10))/8. This concerns an auxiliary projection and does not assert positivity of the exterior-cube operator K=Q-I/32. For the actual identical tensor cube Psi=R3(a tensor3), adjoining its normalized third factor leaves the two-copy defect unchanged, so d(a)>=(1/8)||(I-P)Psi||^2. No center vacuum or relative-degree cutoff is imposed.

Every finite relative sector in the projection estimate. At fixed relative total degree M, let S_M be the permutation-symmetrization projector. For M>=4 the range of P_M has orthonormal basis e0(u)eM(v), e4(u)e(M-4)(v). The transposition x1<->x2 fixes this range, while a three-cycle is rotation by 120 degrees in the relative plane. Binomial expansion of its normalized monomials gives P_M S_M P_M=(I+2C_M)/3 on that range, where C_M=(-1)^M 2^(-M)[[1,9sqrt(binomial(M,4))],[9sqrt(binomial(M,4)),s(M-4)]], s(x)=1-12x+54binomial(x,2)-108binomial(x,3)+81binomial(x,4). For M<4 the cycle compression is the scalar (-1/2)^M. M=0 is exactly the joint relative vacuum. The symmetrized scalar compressions for M=1,2,3 are 0,1/2,1/4. The largest eigenvalues of C_M for M=4,5,6 are 5/8,13/16,(4+3sqrt(10))/16, respectively. These are obtained from the displayed two by two matrices, so the largest symmetrized compression in these degrees is (4+sqrt(10))/8.

The seven remaining finite rows are displayed in the column order (M,s(M-4),strict upper bound for 2^M||C_M||). Each upper bound exceeds max(1,|s(M-4)|)+9sqrt(binomial(M,4)), so it bounds both absolute row sums before multiplication by 2^(-M). Squaring the positive integer radical comparisons verifies each row. Every listed upper bound divided by 2^M is less than 5/8.

$$\begin{array}{r}(7,19,73)\\ (8,-74,155)\\ (9,-194,302)\\ (10,-206,341)\\ (11,106,277)\\ (12,1039,1246)\\ (13,2971,3214)\end{array}$$

The complete infinite tail of the projection estimate. Write x=10+y for an integer y>=0. Exactly, s(10+y)=6361+5388y+2619binomial(y,2)+702binomial(y,3)+81binomial(y,4), and 2s(10+y)-s(11+y)=973+2769y+1917binomial(y,2)+621binomial(y,3)+81binomial(y,4)>0. Consequently s(M-4)>0 and s(M-4)/2^M decreases for M>=14. The off-diagonal ratio is (sqrt(binomial(M+1,4))/2^(M+1))/(sqrt(binomial(M,4))/2^M)=(1/2)sqrt((M+1)/(M-3))<1 there. The row-sum bound therefore gives ||C_M||<=(6361+9sqrt(1001))/16384<6649/16384<1/2 for every M>=14. Combining every case, positivity of P_M S_M P_M and its top eigenvalue give ||P_M S_M P_M||<=(4+sqrt(10))/8 for all M>=1. The operators P_M S_M P_M and S_M P_M S_M have the same norm, by the X^X/XX^ identity for X=S_M P_M. On S_M-invariant vectors this bounds ||P_M Psi||^2. Subtracting from ||Psi||^2 and summing orthogonal relative degrees proves the claimed gamma. Tensoring each sector with the whole center space and summing all its coefficients proves it on the completed invariant subspace.

The exact cubic Husimi identity. Set U(z)=exp(-|z|^2)|f(z)|^2, dnu=d^2z/pi, and m=sup U=m(a). Bounded coherent evaluation gives 0<U somewhere, U<=1, and integral U dnu=1. The joint-relative-vacuum coefficient of the transformed tensor cube is exactly f(t/sqrt(3))^3. Hence ||P_*R3(a tensor3)||^2=||f(t/sqrt(3))^3||^2=3 integral U^3 dnu. With A=(4-sqrt(10))/64 the projection estimate gives d(a)>=A(1-3 integral U^3 dnu). This is an identity for the cubic Husimi functional obtained from the auxiliary projection, rather than an identification of that functional with the exterior-cube gap G.

The external convex comparison and its normalization. Frank, Nicola and Tilli, The generalized Wehrl entropy bound in quantitative form, https://arxiv.org/html/2307.14089v3, Theorem 3 and Remark 4(c), give integral phi(U)dnu<=integral_0^1 phi(t)dt/t for a unit completed Bargmann vector and a continuous convex phi on [0,1] with phi(0)=0 and phi non-linear. Their unitary Bargmann transform uses weight exp(-pi|w|^2)dA(w); z=sqrt(pi)w gives exactly U and dnu above. Dropping the theorem’s nonnegative quantitative remainder gives the displayed comparison. For the positive maximum 0<m<=1 take phi_m(t)=t^3 on [0,m] and phi_m(t)=3m^2t-2m^3 on [m,1]. Its value and first derivative agree at m, its derivative is nondecreasing, and it is nonaffine because m>0. Since U<=m, integral phi_m(U)dnu=integral U^3 dnu. Subtracting the comparison from 1=3 integral_0^1 t^2dt yields d(a)>=A J(m), where J(m)=3 integral_m^1 (t-m)^2(t+2m)dt/t=1-9m^2+8m^3-6m^3 log m. Also (t+2m)/t>=1+2m for m<=t<=1, so J(m)>=(1+2m)(1-m)^3. No bound uniform in the external c_phi as phi varies is used. This retrieved comparison is an analytic dependency; it is neither an admitted Lean axiom nor a delivered kernel theorem.

Attainment and the correct centered stationarity. Coherent overlap is continuous and vanishes at infinity for every completed a: finite Fock polynomials have Gaussian decay and sup_alpha |<D(alpha)e0,a-p>|<=||a-p|| makes approximation uniform. Its positive supremum is attained on a compact disk, since f is not identically zero. Displace a maximizing coherent vector to e0 and choose phase to obtain a’=sqrt(m)(e0+h), h perpendicular to e0, with ||h||^2=(1-m)/m. Let g be the Bargmann function of this displaced vector a’. The function to differentiate is exp(-|beta|^2)|g(conj(beta))|^2, whose maximum is at beta=0 and g(0)=sqrt(m)>0. Its two real first derivatives force g’(0)=0, so h is also perpendicular to e1. The prime in g’(0) is an ordinary scalar derivative; the overlap is not exp(-|beta|^2)|f’(conj(beta))|^2 for the old f. No differentiability of beta->D(beta)a or domain of an unbounded annihilation operator is assumed. The completed-vector beam_displacement and partialTrace_pairDisplacement identities give Phi(D(alpha)|a><a|D(alpha)^)=D(alpha/sqrt(2))sigma_a D(alpha/sqrt(2))^, preserving d and G. Equivalently common displacement changes only the two-copy center. The same energy-free overlap attainment and centering appear in He Appendix K.4; Appendix K.5 proves a qualitative compactness conclusion for the distinct difference-vacuum overlap 2 integral U^2, not the quantitative defect estimate below.

The uniform local quadratic coefficients. For S2(h)=h tensor e0+e0 tensor h, the normalized binomial expansion of R2 S2(e_n) contains twice the even-u coefficients of R2(e_n tensor e0). Pairing occupations 0,2,4 with D gives ell_n=<S2(e_n),Aop S2(e_n)>=3/4-[(3/2)(1+binomial(n,4))+binomial(n,2)]/2^n for n>=2, with binomial(n,4)=0 when n<4. To prove ell_n>=1/8 for every n>=2, put P(n)=12(1+binomial(n,4))+8binomial(n,2). The values at n=2,…,7 are 20,36,72,152,312,600, each at most 52^n. For n>=7, Pascal’s identity gives 2P(n)-P(n+1)=12(1+binomial(n,4)-binomial(n,3))+8(binomial(n,2)-n)>=0: binomial(n,4)>=binomial(n,3) and binomial(n,2)>=n. Induction proves P(n)<=52^n. Different n have orthogonal total degrees and Aop preserves them. Boundedness and truncation therefore give ||Aop^(1/2)S2(h)||^2>=||h||^2/8 for every completed h perpendicular to e0,e1, including arbitrary complex phases and unbounded support.

The full local remainder and global constant. Aop annihilates e0 tensor e0 and ||Aop||=3/8. Expanding a’ tensor a’=m(e0 tensor e0+S2(h)+h tensor h), the reverse triangle inequality gives sqrt(d(a))>=m(r/sqrt(8)-sqrt(3/8)r^2)+, r=||h||. The entire h tensor h term is bounded by sqrt(3/8)r^2; no degree or phase is discarded. Substituting r^2=(1-m)/m gives d(a)>=(1-m)(sqrt(m)-sqrt(3(1-m)))+^2/8. Together with the convex comparison this proves the stronger global bound d(a)>=max{A J(m),(1-m)(sqrt(m)-sqrt(3(1-m)))_+^2/8}. For m<=4/5, the function (1+2m)(1-m)^2 decreases on [0,1], so it is at least 13/125, and A>1/80 because sqrt(10)<16/5. Thus d(a)>=13(1-m)/10000>=(1-m)/800. For m>=4/5, r<=1/2 and 1-sqrt(3)r>=1-sqrt(3)/2>1/8. The local bound gives d(a)>=m(1-m)/512>=(1-m)/640. Hence d(a)>=(1-m(a))/800 for every normalized completed input. The endpoints, including m=1, are included. The numerical constant 1/800 is not claimed optimal.

Distances, noncompact displacement and the sharp exponent. Maximizing phases and displacements gives inf_(alpha,theta)||a-exp(i theta)D(alpha)e0||^2=2(1-sqrt(m))<=2(1-m)<=1600d(a). The exact pure-projector trace distance is inf_alpha |||a><a|-|D(alpha)e0><D(alpha)e0|||_1=2sqrt(1-m)<=sqrt(3200d(a)). For a sequence with d->0, the centered and phased vectors therefore converge to e0, even when their maximizing displacements diverge; compactness of the coherent orbit is not asserted. For the actual physical family a_epsilon=(e0+epsilon e2)/sqrt(1+epsilon^2), 0<=epsilon<=1/sqrt(2), optimizing the angular phase gives the radial overlap exp(-x)(1+epsilon x/sqrt(2))^2, decreasing for x>=0. Thus m=1/(1+epsilon^2). The two-copy expansion gives exactly d=(epsilon^2/8+epsilon^4/32)/(1+epsilon^2)^2. For example the quadratic term is ell_2 epsilon^2=epsilon^2/8, and for e2 tensor e2 the relative-occupation-two probability is 1/4, giving its defect epsilon^4/32; their total degrees are orthogonal. With delta=1-m this is d=delta/8-3delta^2/32. Therefore no uniform bound d>=c delta^r with c>0 can hold for r<1. The exponent one of 1-m, equivalently exponent two of vector or pure-projector distance, is optimal; this does not establish optimality of the global constant.

All normal densities and two quantitative constants. Define d(rho)=3/8-Tr(Phi(rho)^2) and m(rho)=sup_alpha <D(alpha)e0,rho D(alpha)e0>. The full two-copy compression, not just its pure-square restriction, proves d(rho)>=(3/16)(1-Tr(rho^2)). Indeed R2 conjugates original copy swap to relative parity, B is supported on even relative occupations, and 0<=T<=(3/8)P_sym. Therefore Tr(Phi(rho)^2)<=(3/8)Tr((rho tensor rho)P_sym)=(3/16)(1+Tr(rho^2)). Equality d=0 forces rho pure and then the preceding equality proof makes it coherent. Conversely coherent pure inputs attain zero. For stability let lambda be the largest eigenvalue of rho, with unit eigenvector a. Positive trace-class compactness gives this attained eigenvalue, lambda>=Tr(rho^2), hence 1-lambda<=(16/3)d(rho). If lambda<1 write rho=lambda|a><a|+(1-lambda)tau. Convexity of squared Hilbert-Schmidt norm gives d(rho)>=lambda d(a)+(1-lambda)d(tau)>=lambda d(a), since d(tau)>=0. The lambda=1 case is immediate. Positivity gives m(rho)>=lambda m(a). Consequently 1-m(rho)<=(1-lambda)+lambda(1-m(a))<=(16/3+800)d(rho)=(2416/3)d(rho), or d(rho)>=(3/2416)(1-m(rho)). Finite-rank approximation in trace norm shows that the coherent symbol is continuous, vanishes at infinity and has a positive attained maximum. The pure-reference fidelity inequality then yields inf_alpha ||rho-|D(alpha)e0><D(alpha)e0|||_1<=2sqrt(1-m(rho))<=2sqrt((2416/3)d(rho)). No finite-rank or photon-moment assumption is imposed.

Spectral exclusions used for the exterior-cube consequence. For an arbitrary trace-one positive trace-class sigma put q=Tr(sigma^2). If q<=1/3, Cauchy-Schwarz gives p3>=q^2 and Newton’s identity gives e3>=(1-3q+2q^2)/6>=1/27. On [1/3,3/8] the sharp trace/purity envelope is E(q)=[10-18q-(6q-2)^(3/2)]/108, attained abstractly at (x,x,1-2x,0,…), x=(2+sqrt(6q-2))/6. To see the finite minimization, minimize e3 under p2<=q. At least three entries are positive. Moving mass between two entries strictly decreases their product times the positive remaining mass while increasing p2, so the constraint is active. Except at the endpoint 1/3 its gradients are independent. Lagrange multipliers give at most two positive values x>y. Two occurrences of y would have tangent vector (1,-1) with constrained Hessian 2(y-x)<0; hence only one y occurs. If there are k occurrences of x, then 1/(k+1)<q<1/k. The present interval forces k=2, giving E. For countable spectra retain the first n entries and replace tail mass T_n by L_n equal entries, choosing finite L_n with T_n^2/L_n no larger than the original tail squared mass; a zero tail needs no replacement. The trace stays one, p2 does not increase, and p2,p3 converge to the original moments since their tail contributions are bounded by T_n^2,T_n^3. Newton’s identity passes the finite inequality to the countable case. The envelope decreases, E(3/8)=25/864, and solving E(q)=1/32 gives q_c=(17-5sqrt(5))/16. Thus every physical a obeys e3(sigma_a)>=25/864 and q<=q_c implies e3>=1/32. The abstract optimizer need not be a physical channel output. The adjacent-uniform classical moment-boundary context is Harremoes, Joint Range of Renyi Entropies, Kybernetika 45 (2009), 901-911, Section 3 and Theorem 2, https://www.kybernetika.cz/content/2009/6/901/paper.pdf; the countable argument and constants here are derived explicitly.

The largest-eigenvalue exclusion is exact. If x is any distinguished eigenvalue of a trace-one positive trace-class sigma and tau is its remaining eigenvalue sequence, then e3(sigma)-1/32=(2x-1)(4x-1)^2/32+(x/2)(3/8-q)+e3(tau). In fact sum tau=1-x, p2(tau)=q-x^2 and e3(sigma)=x[(1-x)^2-(q-x^2)]/2+e3(tau), which factors as displayed. All series converge absolutely. In particular q<=3/8 and lambda_max(sigma)>=1/2 imply e3>=1/32. The identity itself needs neither sign hypothesis nor that x be largest. This is a sufficient exclusion, not a characterization of realizable physical spectra.

The local exterior-cube bound needed near the coherent orbit. Retain the full bounded K=Q-I/32 and G(a)=<a tensor3,K(a tensor3)> from the actual channel. For every b perpendicular to e0,e1,e2 and every complex z, put rho_loc^2=|z|^2+||b||^2. If rho_loc<=1/1024, then G(e0+z e2+b)>=(3/256)(|z|^4+||b||^2). Here is a full-operator proof using the coefficients already derived above. With S(v)=v tensor e0 tensor e0+e0 tensor v tensor e0+e0 tensor e0 tensor v, the relative eigenvalues delta0=delta2=0 and the identity center factor imply K(e0 tensor3)=0 and KS(e2)=0. A zero quadratic form of an indefinite K alone would not imply these annihilations. For N>=3 the actual moment coefficients give c_N=<S(eN),KS(eN)>=7/32-(3/8)(beta0+beta2)-beta1/2=7/32-P(N)/2^(N+7), P(N)=3N^4-22N^3+69N^2-42N+56. Thus c_N>=3/128: P(3),P(4),P(5),P(6)=200,352,696,1424 are at most 25*2^N, and at N=6+j, 2P(N)-P(N+1)=3j^4+38j^3+153j^2+198j+48>0. Orthogonal total degrees and boundedness give <S(b),KS(b)>=sum_(N>=3)c_N|b_N|^2 for arbitrary complex completed b. These are full-G input quadratic coefficients, not relative-sector eigenvalues.

The phase-sensitive degree-four square and the entire tensor remainder. Set T4=e2 tensor e2 tensor e0+e2 tensor e0 tensor e2+e0 tensor e2 tensor e2 and w=z^2. The nonzero-gap components of S(e4) and T4 are respectively sqrt(2)t h3+h2^2/(4sqrt(6)) and -sqrt(3)t h3+h2^2/8; their other relative degrees 0,2 have zero gap. Using delta3=9/256, delta4=3/128, ||t h3||^2=4/9 and ||h2^2||^2=64 gives <b4 S(e4)+w T4,K(b4 S(e4)+w T4)>=(1/64)|sqrt(2)b4-sqrt(3)w|^2+(3/2)|b4/(4sqrt(6))+w/8|^2=(3/64)|b4-w/sqrt(6)|^2+|w|^2/16. In particular the center t and the relative phase of b4,z^2 remain present. Put X=S(b)+z^2T4 and Dloc=||b||^2+|z|^4. The other total degrees and |b4|^2<=2|b4-z^2/sqrt(6)|^2+|z|^4/3 give <X,KX>>=(3/128)Dloc, and ||X||^2=3Dloc. For u=z e2+b, write exactly (e0+u) tensor3=e0 tensor3+zS(e2)+X+R. The remainder consists of the six placements of z e2,b,e0, the three placements of b,b,e0, and u tensor3. These three groups are mutually orthogonal, so ||R||^2=6|z|^2||b||^2+3||b||^4+rho_loc^6<=8rho_loc^2Dloc when rho_loc<=1. The last inequality uses rho_loc^4<=(|z|^4+2||b||^2)<=2Dloc. Self-adjointness and ||K||<=31/32<1 bound every remaining pairing, giving G(e0+u)>=[3/128-4sqrt(6)rho_loc-8rho_loc^2]Dloc. At rho_loc<=1/1024, 4sqrt(6)<10 and 10rho_loc+8rho_loc^2<=1281/131072<3/256, proving the local bound. Every middle sector and the infinite tail is included through the full K norm.

The coherent-orbit consequence for G. Put m0=2^20/(2^20+1). If m(a)>=m0, the attained maximizing displacement and phase give a’=sqrt(m)(e0+z e2+b), b perpendicular to e0,e1,e2, with |z|^2+||b||^2=(1-m)/m<=2^(-20). Covariance preserves G and its homogeneity is G(gamma a)=|gamma|^6G(a). Apply the full local bound and use |z|^4+||b||^2>=(|z|^2+||b||^2)^2, since the difference is ||b||^2(1-2|z|^2-||b||^2)>=0 in this range. It follows that G(a)>=(3/256)m(1-m)^2. The attained overlap is one exactly for coherent vectors up to phase; these have G=0 and spectrum (1/2,1/4,1/4). Thus the normalized coherent orbit is a strict local minimum of G modulo phase and displacement, on the entire Hilbert sphere without an energy constraint. This local conclusion does not settle global G or entropy.

An explicit high-purity strip and the exact necessary residual region. Let delta0=1/(2^20+1), epsilon0=delta0/10, so m0=1-delta0. If d(a)<=epsilon0, the global purity stability gives delta=1-m<=800d<=80delta0<1/1024. Therefore sqrt(m)>31/32 and sqrt(3delta)<2/32. The local purity bound gives d>=delta(29/32)^2/8>=delta/10, because (29/32)^2/8>1/10. Hence delta<=10d<=delta0, so the coherent-orbit G bound applies: q=Tr(sigma_a^2)>=3/8-1/[10(2^20+1)] implies e3(sigma_a)>=1/32, with G(a)>0 for every noncoherent a in this strip. Combining this closed strip with the spectral and largest-eigenvalue exclusions, any negative physical G(a) must simultaneously satisfy (17-5sqrt(5))/16<q<3/8-1/[10(2^20+1)], lambda_max(sigma_a)<1/2, and m(a)<2^20/(2^20+1). The remaining q interval is nonempty. These inequalities are necessary conditions only; no arbitrary prescribed spectrum or point in that region is asserted physically attainable. The complete same-function inequality above, including all M=6,…,63 and every center coefficient and infinite tail, is still open. Neither this high-purity strip nor the auxiliary S3 projection estimate proves global e3>=1/32 or the all-density entropy target S(Phi(rho))>=(3/2)log 2. The countable spectral/ENNReal bridge remains pending formalization, and the all-n/all-eta entropy conjecture remains open.

Completion and literature limits for the quantitative package. All rotations, occupation projections, symmetrizations and defect operators used here are bounded on completed Hilbert spaces. Norm-convergent finite Fock truncations have norm-convergent tensor powers; their Bargmann functions and scalar derivatives converge on compact sets, justifying the coefficient identities without placing those derivatives in Fock space. Positive trace-class decomposition and trace-norm continuity justify the density arguments, including infinite rank. The convex generalized-Wehrl comparison is the precise external analytic dependency; it still needs an exact formal bridge rather than an axiom. He Theorem 8 and Appendix F already provide the maximum/kernel/equality result, and K.4-K.5 provide the centering and qualitative comparison described above. The primary He text available for comparison is proxy-extracted PDF text; a raw-file checksum and facsimile audit are not asserted. A bounded comparison of those statements does not establish worldwide novelty for the explicit S3 gap, cubic-Husimi conversion, stability constants or strip. Cuesta, A stable quantum Darmois-Skitovich theorem, https://arxiv.org/html/1902.05298v1, Theorem 9, assumes finite moments of all orders and an approximately product full splitter output, with moment-dependent constants; it does not supply this energy-independent defect bound. Springer, Lee, Bellini and Kim, Conditions for factorizable output from a beam splitter, https://arxiv.org/html/0906.1885v1, Section III, concerns factorization of the entire output, not relative support {0,4}. Van Herstraeten, Guha and Cerf equation (45) supplies the actual Fock attenuator, equation (44) its displacement covariance, and Conjecture 1 an entropy assertion supported there by numerical exploration. None of these attributions promotes the analytic additions to kernel-verified declarations or resolves the remaining global problem.

Attainment modulo displacement and the nonlinear variational conditions (A3–A6). Continue the physical model, coefficient localization A1 and weak-profile identity A2 in the Attenuator owner. Let E(a)=e₃(σₐ), I=inf_{‖a‖=1}E(a), q(a)=Tr σₐ² for unit a, and d(a)=3/8−q(a). The theorem is: for EVERY normalized minimizing sequence aₙ, there are displacements αₙ, scalar phases ζₙ of modulus one and a strictly increasing subsequence n_k for which ζ_n_k D(−α_n_k)a_n_k converges strongly in H to a unit minimizer a. Maximizing coherent centering can be used at each term and retained at the limit: a₀=√m(a)>0 and a₁=0, where m(a)=sup_α|⟨D(α)e₀,a⟩|². The proof permits infinite input support, infinite output rank, arbitrary complex phases and infinite mean photon number. It asserts subsequential compactness after these transformations, without asserting uniqueness or convergence of the original full sequence.

The analytic inputs are the accepted D1 spectral envelope, D2 distinguished-eigenvalue identity, completed displacement covariance and coherent centering, the physical purity bound q≤3/8, and the all-sector projection inequality preceding the accepted P3 Wehrl conversion. Their exact native realizations remain pending; this exposition neither turns them into axioms nor takes over their implementation owners. For later residual conditions we also use the accepted P8 high-purity exclusion and T2 pure-output rank≤5 exclusion at the same analytic status. The present continuation preserves the existing corrected coefficient, displacement, complex-phase, center-degree and infinite-tail arguments. It supplies the new A1–A6 chain without replacing the separately owned D/P/T packages.

A3. Uniform nonvanishing for every minimizing sequence. D1 and the coherent output spectrum (1/2,1/4,1/4) give 25/864≤I≤1/32. Put q̄=93/256. For q≤1/3, D1 gives E≥(1−3q+2q²)/6≥1/27>1/32. For 1/3≤q≤q̄ it gives E≥E_sp(q̄), where E_sp(q)=[10−18q−(6q−2)³ᐟ²]/108 is decreasing on [1/3,3/8]. Its target root is q_c=(17−5√5)/16. The exact comparisons 1/3<93/256<q_c follow from 279>256 and 80√5<179, the latter from 32000<32041 after squaring. Hence E_sp(q̄)>1/32. The fixed positive margin min(1/27,E_sp(q̄))−1/32 excludes the whole q≤q̄ region eventually along any minimizing sequence, including when I=1/32. Thus q(aₙ)>q̄ and d(aₙ)<3/256 eventually.

Use the full projection estimate d(a)≥A(1−3∫Uₐ³dν), A=(4−√10)/64, Uₐ(z)=exp(−|z|²)|f(z)|², dν=d²z/π. It comes from the complete transported three-copy invariant subspace: the retained relative occupations 0,4, the joint relative-vacuum projection P_* and its gap (4−√10)/8, with ‖P_*(a⊗³)‖²=3∫Uₐ³dν. Every relative sector and every center coefficient is included. For unit a, 0≤Uₐ≤m(a) and ∫Uₐdν=1, so ∫Uₐ³dν≤m(a)². Consequently 3m(aₙ)²≥1−d(aₙ)/A>1−(3/256)/A=(4−√10)/8, and m(aₙ)>√((4−√10)/24). This uses the projection estimate itself, without identifying the degree-six output functional E with a generalized Wehrl functional.

For completeness, each nonzero a has an attained coherent maximum without an energy premise. For finite occupation polynomials, α↦⟨D(α)e₀,a⟩ is continuous and vanishes at infinity. Approximation in H is uniform in α because |⟨D(α)e₀,a−b⟩|≤‖a−b‖; hence the same C₀ property holds for all a. A nonzero Bargmann entire function has a nonzero evaluation, so the supremum is positive and attained in a compact disk. Choose ANY maximizing αₙ and a phase so bₙ=ζₙD(−αₙ)aₙ has (bₙ)₀=√m(aₙ)>0. Weyl displacement maps coherent states to coherent states up to phase and preserves m. The completed covariance follows from DisplacementCovariance.beam_displacement and partialTrace_pairDisplacement for arbitrary completed two-mode vectors: σ_D(α)a=D(α/√2)σₐD(α/√2)*. It preserves E and q; coherent_output_covariance alone is only the coherent-input special case.

Let gₙ be the Bargmann function of the displaced vector bₙ. The two real first derivatives at β=0 of exp(−|β|²)|gₙ(conjugate β)|² vanish at the maximum. Their linear parts are the real and imaginary parts of conjugate((bₙ)₀)(bₙ)₁, so (bₙ)₁=0. This uses gₙ itself, rather than the derivative of the undisplaced function; it differentiates a scalar entire overlap, not the unbounded annihilation generator or the map β↦D(β)aₙ. The unit ball of separable H is weakly sequentially compact. Passing to a subsequence, bₙ⇀a, and its vacuum coordinates converge to a₀≥((4−√10)/24)¹ᐟ⁴>0. Thus t=‖a‖² satisfies 0<t≤1, rₙ=bₙ−a⇀0, and ‖rₙ‖²→1−t. The quantifier starts with an arbitrary minimizing sequence, not a selected finite-support one.

A4. The exact cost of mass loss. Homogeneity and the definition of I give E(b)≥I‖b‖⁶ for every b≠0 by normalization, and for b=0 both sides vanish. The unnormalized physical purity estimate p₂(b)≤(3/8)‖b‖⁴ gives e₂(σ_b)≥(5/16)‖b‖⁴, including b=0. Apply A2 to bₙ=a+rₙ and take the liminf of these pointwise lower bounds. No convergence of E(rₙ) is assumed. One obtains I≥I[t³+(1−t)³]+(5/16)[t(1−t)²+(1−t)t²]=I+t(1−t)(5/16−3I). The two cross masses sum to t(1−t); the coefficient is exactly 5/16. Since I≤1/32, 5/16−3I≥7/32>0. A3 has excluded t=0, so every case 0<t<1 is impossible and t=1 is forced. This includes I=1/32 and sequences with zero remainders.

Therefore ‖rₙ‖→0. The channel estimate ‖σ_b−σₐ‖₁≤(‖b‖+‖a‖)‖b−a‖ and trace-polynomial continuity give ‖a‖=1 and E(a)=I. The supremum of coherent amplitude, √m, is 1-Lipschitz in the vector norm, so strong convergence retains a₀=√m(a)>0 real and a₁=0. This proves both attainment and the asserted every-sequence subsequence theorem, for any choices of maximizing gauges along the extracted terms. A strict overlap inequality along a sequence would in general pass only as a non-strict inequality. If I<1/32, apply the A3 argument anew to the limiting minimizer (whose q>q_c>q̄) to obtain the strict m(a)>√((4−√10)/24). No compactness of the Weyl orbit itself, finite energy estimate or full profile decomposition was assumed.

A5. Real Fréchet differentiation and the actual channel adjoint. The map Q(u,v)=C_uC_v* is bounded sesquilinear H×H→S₁, with ‖Q(u,v)‖₁≤‖u‖‖v‖. After restricting scalars to ℝ it is bounded bilinear. Trace multiplication and the ideal norm bounds express s,p₂,p₃,E as bounded real multilinear polynomials of degrees 2,4,6. Thus they have continuous real Fréchet derivatives of every order, with uniform remainder bounds on bounded sets. These are not holomorphic derivatives in complex amplitudes. They are defined for all complex h∈H, even with infinite photon moments.

For general unnormalized a, put σ=σₐ, s=‖a‖² and X=Q(h,a)+Q(a,h)=Φ(|h⟩⟨a|+|a⟩⟨h|). Differentiating Newton’s identity and using trace cyclicity gives D e₃(σ)[X]=e₂(σ)Tr X−s Tr(σX)+Tr(σ²X). The actual normal-channel trace pairing in the Attenuator owner then yields D E(a)[h]=2 Re⟨h,[e₂(σ)Id−sΦ*(σ)+Φ*(σ²)]a⟩. The factor s must remain for unnormalized a. At unit a this is 2 Re⟨h,[e₂(σ)Id−B_σ]a⟩, where B_σ=Φ*(σ−σ²). Each perturbation is self-adjoint trace class; every cyclic product has a trace-class factor and otherwise bounded factors.

At a constrained unit minimizer, the real tangent tests give [e₂(σ)Id−B_σ]a=λa with λ real. Euler homogeneity D E(a)[a]=6I fixes λ=3I for the constraint ‖a‖²=1; the phase direction supplies no additional multiplier. With q=Tr σ² and p₃=Tr σ³, e₂−3I=(1−q)/2−(1−3q+2p₃)/2=q−p₃=:μ. Hence B_σa=μa for every unit minimizer. This equation uses the same physical input a and its output σₐ.

Here B_σ is positive and compact for the actual channel. For v∈H set W_va=(⟨v|⊗Id)Va. A finite occupation vector v makes W_v a finite linear combination of the row-slice maps in A1, each compact (retaining z fixes the orientation). The contraction bound ‖W_v−W_w‖≤‖v−w‖‖V‖=‖v−w‖ and finite occupation approximation extend compactness to every v. Directly Φ*(|v⟩⟨w|)=W_vW_w, so Φ sends every finite-rank output operator to a compact operator. It is linear with ‖Φ*(K)‖≤‖K‖, since Φ*(K)=V*(K⊗Id)V. Operator-norm approximation therefore shows that Φ* sends EVERY compact output operator to a compact input operator. In particular σ and σ² are compact and so is B_σ. As a density, 0≤σ≤Id; positivity of Φ* gives B_σ≥0. The statement concerns compact outputs: Φ*(Id)=Id remains noncompact in this infinite-dimensional space.

A6. Second variation in all complex perpendicular directions. Let h∈H be arbitrary with ⟨a,h⟩=0, not restricted to real occupation coefficients. Put c=‖h‖², X=X_h=Φ(|h⟩⟨a|+|a⟩⟨h|), and Y=Φ(|h⟩⟨h|). For real t, a(t)=(a+th)/√(1+ct²) is an exact unit curve and σ(t)=(σ+tX+t²Y)/(1+ct²)=σ+tX+t²Z+O_S₁(t³), Z=Y−cσ. Here Tr X=0, Tr Y=c and Tr Z=0. For trace-one outputs E=(1−3Tr σ²+2Tr σ³)/6. The linear coefficient is −Tr[(σ−σ²)X]=−2 Re⟨h,B_σa⟩=0.

The quadratic trace coefficients are Tr X²+2Tr σZ for p₂, and 3Tr σ²Z+3Tr σX² for p₃. In the cubic expansion the three σ²Z placements and the three σX² placements have these traces by cyclicity, without commutativity. Consequently E(a(t))=I+t²[μc−⟨h,B_σh⟩−Tr[((1/2)Id−σ)X_h²]]+O(t³). The actual second derivative is TWICE the bracket. Minimality therefore gives ⟨h,B_σh⟩+Tr[((1/2)Id−σ)X_h²]≤μ‖h‖² for every complex h⊥a. It holds for h and ih, and for every complex combination in a⊥. The full real sphere tangent Re⟨a,h⟩=0 splits into a complex-perpendicular direction and ira, r∈ℝ; phase invariance supplies the same constrained-Hessian information in the latter direction. No complex-bilinear Hessian is asserted.

The top-eigenpair conclusion requires the strict gap I<1/32. D2 states that for any distinguished eigenvalue x of a trace-one positive output and its remaining eigenvalue sequence τ, E−1/32=(2x−1)(4x−1)²/32+(x/2)(3/8−q)+e₃(τ). Indeed Tr τ=1−x, Tr τ²=q−x² and E=x e₂(τ)+e₃(τ), which give the identity by substitution; all sums converge absolutely. A nonzero trace-class density has an attained largest eigenvalue. If x=λ_max(σ)≥1/2 and q≤3/8, every displayed term is nonnegative. Thus I<1/32 forces λ_max(σ)<1/2. Purity alone does not give that strict bound.

Under this gap, A=(1/2)Id−σ is bounded positive, and X_h² is positive trace class. The trace is nonnegative because Tr(A X_h²)=Tr(X_h A X_h)≥0, equivalently by the positive square-root pairing; A and X_h need not commute, and A need not be trace class. The second variation now gives ⟨h,B_σh⟩≤μ‖h‖² on a⊥. Self-adjointness and B_σa=μa make the cross blocks vanish in H=ℂa⊕a⊥, so 0≤B_σ≤μId. Also p₃≤‖σ‖q<q/2 and q>0, hence μ=q−p₃>0. Its unit eigenvector a proves ‖B_σ‖=μ. Compactness was established for the actual Φ* in A5. The stationarity and second-variation equations hold at any unit minimizer, while this proof of the top-eigenvalue conclusion keeps the negative-gap hypothesis.

The cumulative strict residual is now precise. Any negative-G unit input, and therefore any minimizer with I<1/32, must have rank σ≥6 (infinite rank is allowed, by accepted T2), q_c=(17−5√5)/16<q<3/8−1/[10(2²⁰+1)], λ_max(σ)<1/2, and √((4−√10)/24)<m(a)<m₀=2²⁰/(2²⁰+1). The upper q and m bounds use accepted P8; A3 supplies the lower m bound. At a violating minimizer these conditions accompany B_σa=μa, ‖B_σ‖=μ and the full complex second variation. Newton’s identity gives 6I=1−q−2μ, so I<1/32 is exactly μ>13/32−q/2. These are necessary conditions on one physical input, without a realizability characterization, positive uniform spectral-tail mass bound, sufficiency test or minimizer classification.

Attainment reduces the all-input target E(a)≥1/32 on the unit sphere to I=1/32, equivalently to excluding an attained physical minimizer with I<1/32. That exclusion is still open. In same-input cycle variables it is p₃≥5/32−(3/2)d. In the full relative-sector notation the missing inequality is (1/16)‖P₅‖₃²≤(1/64)‖P₃‖₃²+(3/2)‖P₄‖₃²+R_mid(f)+R_tail(f), where P₃,P₄,P₅ are the same-function differential polynomials defined earlier in these owners and ‖P‖₃²=(3/π)∫|P(c)|²exp(−3|c|²)d²c is their weighted center norm. More explicitly, R_mid=Σ_M=6,…,63⟨F_a,M,(Id_center⊗(q_M−Id/32))F_a,M⟩, and R_tail is the same sum over EVERY M≥64; F_a,M is the whole relative-degree-M component of the transformed actual f⊗³. Thus every middle sector, every center coefficient and the entire infinite tail remain. These quantities are distinct from the projection P_* in A3. No arbitrary spectrum, nonphysical symmetric tensor or positivity of the full exterior-cube operator substitutes for the same-function inequality. The new compactness proof excludes loss of mass and an unattained-infimum escape; it supplies no negative physical example and no universal E≥1/32 proof. The e₃ inequality is a sufficient entropy route, not an equivalent form of the entropy conjecture. Unrestricted balanced two-photon/all-normal entropy, the countable spectral/ENNReal entropy bridge and all-n/all-η Conjecture 1 remain open.

Literature and method. Zixuan He, The energy cost of optical noise, version 1.0 (25 October 2026), DOI 10.5281/zenodo.23629201, Theorem 8, equations (38),(40), Appendices E.2 and F already give the balanced all-normal purity maximum cₙ=4⁻ⁿbinom(2n,n), its bounded copy kernel and coherent equality for n=0 or n≥2, including the n=2 weights 3/8,1/4,3/8. Appendix F uses the missing relative degree-two coefficient ff″−(f′)² and does not impose photon moments. These prior purity/equality results are attributed to He. Appendix K.5 also proves qualitative compactness toward the coherent orbit when ν(aₙ)=2∫Uₐₙ²dν→1, by maximizing coherent centering, a nonzero weak profile, Brezis–Lieb splitting and 1≤t²+(1−t)². That is a close prior compactness mechanism. Here a minimizing sequence need only have a uniformly nonzero coherent overlap and may have positive purity defect: A2 and A4 provide its actual-output degree-six splitting and the different strict cost 5/16−3I≥7/32. The relevant He evidence is checked primary PDF text extraction, with some display-layout garbling, rather than a raw-PDF/facsimile audit.

João P. G. Ramos, Eigenfunctions, Free Boundaries, and Time-Frequency Localization, arXiv:2607.21590v2, Section 7 (https://arxiv.org/html/2607.21590v2), develops Weyl-separated Fock profiles, Pythagorean norm splitting and concentration–compactness, explicitly situated in the Lions/time-frequency literature. Proposition 7.1 has a double-limit dispersive remainder; profile extraction alone does not give norm-vanishing of a remainder. Theorem 9 proves existence for the Gaussian localization functional I_F(s)=sup_|Ω|=s∫_Ω|F(z)|²exp(−π|z|²)dA, and Theorem 10 identifies the maximizing sets as disks. This supplies relevant existing methodology and attribution. Its quadratic set-localization functional with parameter s is distinct from the physical degree-six e₃(CₐCₐ*) here; it supplies neither A2’s two e₂ cross masses nor A4’s strict cost nor the self-consistent Φ* variation. Those facts have been proved above directly.

Frank, Nicola and Tilli, The generalized Wehrl entropy bound in quantitative form, arXiv:2307.14089v3, Theorem 3 and Remark 4(c) (https://arxiv.org/html/2307.14089v3), compare convex coherent-symbol integrals with the coherent integral, including a nonnegative quantitative remainder. The substitution z=√πw matches d²z/π to their Bargmann normalization. The P3 conversion has that scope; A3 uses its preceding all-sector projection estimate and U≤m, without requiring a new FNT constant uniform in m or a Wehrl identity for the cycle term. Van Herstraeten, Guha and Cerf, Classical capacity of quantum non-Gaussian attenuator and amplifier channels, arXiv:2312.15623v2, equations (44),(45) and Conjecture 1 (https://arxiv.org/html/2312.15623v2), give the physical channel and completed displacement covariance and state coherent minimum output entropy as conjectural. Their numerical observations are not a proof. These positive source comparisons support attribution and exact scope; bounded searches establish no novelty, priority or worldwide absence claim.

The complete native contracts remain F1–F9: F1, completed occupation/Bargmann-to-S₂ vectorization, σₐ=CₐCₐ* and the unnormalized exterior/spectral Newton identities; F2, the normal S₁ channel and actual adjoint trace pairing; F3, the exact invalid-index coefficient formula, fixed-L weights and both compact restrictions; F4, S₁ coherence decay, compact tests, every cubic cross trace and both unnormalized e₂ masses; F5, the exact D1/D2, purity, all-sector projection, completed covariance and C₀-centering dependencies; F6, every-sequence nonvanishing, all mass cases, strict cost, strong convergence and preserved gauge; F7, bounded real-polynomial derivatives, multiplier 3I and full factor-two normalized second variation; F8, compact W_v and Φ* on all compact outputs, positivity and the negative-gap top eigenpair; F9, the cumulative residual and its unresolved same-input boundary. Existing supplier declarations reduce machinery work but do not discharge these exact joins. This existing-owner exposition adds no Lean declaration, theorem Describe, Reg audit, utility/admission result, freeze or ledger entry, and reports no new kernel or global entropy proof. R3: the real horizontal Hessian for the conditional R1-R3 package. Use the same actual unit negative minimizer, sigma, mu, B and A of Attenuator, under its explicitly stated A1-A6 prerequisites; all assertions in this addendum remain analytic prose pending native formalization. Let T={h:<a,h>=0}, the complex-perpendicular subspace regarded as a real Hilbert space with inner product Re<h,k>. It is the horizontal or projective tangent. The literal full real sphere tangent is S={h:Re<a,h>=0}=T direct_sum_R R(ia). Put X_h=Phi(|h><a|+|a><h|) and Q(h)=mu||h||^2-<h,Bh>-Tr(A X_h^2). The objective is to represent this actual second-variation coefficient, not a complex-bilinear substitute, on its declared real domain.

Compactness of the physical coherence map. For fixed a, R_a:h -> C_h C_a^* is bounded complex-linear H -> S1 with norm at most ||a||, by the S2 times S2 trace-ideal inequality. A2 and adjoint invariance of trace norm send each bounded weakly-null sequence to zero in S1. The Hilbert weak-sequence criterion gives compactness of R_a. There is also a direct A1 norm-approximation proof. For finite-support b choose fixed L with C_b=C_b P_L. Then R_b h=(C_h P_L)C_b^*, a compact H -> S2 map followed by bounded S2 -> S1 multiplication. Moreover ||R_a-R_b||_(H->S1)<=||a-b||. Finite-support b approximates a, and norm limits of compact operators are compact. This uses actual coefficient localization; generic coefficient symmetry or compactness of C_a alone would not establish the needed H -> S1 map.

Realification and legitimate trace products. The map h -> X_h=R_a h+(R_a h)^* is compact real-linear into self-adjoint S1 and hence into the real Hilbert space S2_R, since ||X||_2<=||X||_1. Its adjoint summand is conjugate-linear, so treating this Hessian as complex-linear would change the claim. Define M_T:T_R -> S2_R by M_T h=A^(1/2)X_h. Bounded left multiplication preserves compactness. With the real Hilbert-Schmidt inner product Re Tr(U^* V), ||M_T h||_2^2=Tr(X_h A X_h)=Tr(A X_h^2). X_h belongs to S1 and S2 and A is bounded, so these are genuine trace-class products; the S2 times S2 ideal estimate and bounded-factor cyclicity justify the equalities. No commutation of A and X_h, trace-class property of A, or cyclic permutation of unbounded products is assumed.

The tangent-domain adjoint and compression. Ba=mu a and self-adjointness make T invariant under B. The real Hilbert adjoint M_T^* has target T_R, giving H_T=mu Id_T-B restricted to T-M_T^*M_T and Q(h)=<h,H_T h>_R. This is bounded real self-adjoint and A6 gives H_T>=0. Both B restricted to T and M_T^*M_T are compact real operators. If M were first defined on all H_R, its expression on T would instead require the real orthogonal compression of M^*M; there is no assumption that unrestricted M^*M preserves T. Defining M_T on T avoids that error.

Fredholm index zero and coercivity off the whole actual kernel. Write C_T=B restricted to T+M_T^*M_T. It is compact positive real self-adjoint with 0<=C_T<=mu Id_T, and H_T=mu Id_T-C_T with mu>7/32. The eigenspace of C_T for the nonzero eigenvalue mu is finite dimensional. On its real orthogonal complement there is no mu-eigenvector; compactness prevents any other eigenvalues accumulating at the nonzero mu. Thus some c_a>0 satisfies Q(h)>=c_a||h||^2 for h real-orthogonal to ker H_T. In particular H_T has closed range and finite kernel; self-adjointness identifies its real cokernel with that kernel, so its Fredholm index is zero. Equivalently its essential spectrum is {mu}, using complexification if that convention is desired. No quantitative or input-uniform c_a is provided. The complement is that of the entire actual kernel, not just selected symmetry vectors.

Exact normalized Taylor expansion and the factor two. For h in either T or S, let c=||h||^2, Y=Phi(|h><h|), and a(t)=(a+t h)/sqrt(1+c t^2). This is a unit curve because Re<a,h>=0. Its output is exactly (sigma+tX_h+t^2Y)/(1+c t^2)=sigma+tX_h+t^2Z+O_S1(t^3), Z=Y-c sigma, and Tr X_h=0. Trace-ideal polynomial expansion gives the t^2 coefficients Tr(X_h^2)+2Tr(sigma Z) for p2 and 3Tr(sigma X_h^2)+3Tr(sigma^2 Z) for p3. The linear coefficient in E=(1-3p2+2p3)/6 is -2Re<h,Ba>=0. Substitution gives E(a(t))=I+t^2[mu c-<h,Bh>-Tr(A X_h^2)]+O(t^3)=I+t^2Q(h)+O(t^3). Therefore the actual constrained second derivative is exactly 2Q(h), and polarization gives the bilinear Hessian 2[mu Re<h,k>-Re<h,Bk>-Re Tr(X_h A X_k)]=2<h,H_T k>_R on T. Q itself is the coefficient of t^2, not the second derivative.

Full sphere, phase and other null directions. On S use M_S:S_R -> S2_R and H_S=mu Id_S-B restricted to S-M_S^*M_S. The same proof gives a nonnegative real Fredholm operator of index zero. For ia, X_(ia)=0 and B(ia)=mu ia, so ia is a phase-null vector; S=T direct_sum_R R(ia). In fact M_S kills ia and the self-adjoint decomposition gives H_S=H_T direct_sum 0. Completed displacement covariance makes E(D(beta)a) constant. R2 proves the orbit differentiable before its tangent vectors are used; after subtracting the phase component their horizontal derivatives lie in ker H_T. Nonnegativity turns a zero quadratic value into a kernel vector. These symmetry directions do not identify the whole kernel. The simple top eigenvalue and gap of B do not imply H_T>0 on all T, because M_T^*M_T can cancel that gap. No strict positivity after phase alone, Morse-Bott theorem, local/global uniqueness or minimizer classification is proved. A finite-dimensional Hessian kernel is not a finite occupation or relative-sector truncation.

All six qualifications for R1-R3. C1: C-infinity means real smoothness in alpha=(x,y), never holomorphy or an operator-norm derivative of the Weyl group itself. C2: auxiliary environmental transfer uses the repository sign D(-alpha), even though the literature uses another splitter convention. C3: the explicit rank-one Pe0 formula needs the positive a_0 gauge; the finite-seed Riesz proof treats every nonzero eigenspace without it or simplicity. C4: T is horizontal, S is the full real sphere tangent, the restricted real adjoint or explicit compression is required, and the actual Hessian is 2Q. C5: coercivity is off the entire real Hessian kernel; the B gap does not identify or remove that kernel. C6: the exact Weyl polynomial/scaling, two zero circles, transfer sign, pure Wirtinger coefficients, rising factorial, real compact correction and factor two are retained. None adds an initial support, rank or energy assumption.

The cumulative residual and the missing same-input inequality. The earlier D/P/T/A analytic packages imply that a negative minimizer would have rank(sigma)>=6, allowing infinity; (17-5sqrt(5))/16<q<3/8-1/[10(2^20+1)]; lambda_max(sigma)<1/2; and sqrt((4-sqrt(10))/24)<m(a)<2^20/(2^20+1). R1-R3 further force the simple top B eigenpair with its individual gap, every photon moment and a finite-dimensional real Hessian kernel. These are necessary conditions, not sufficient conditions for minimality or a characterization of physical realizability. They have not been shown inconsistent. The negative condition is exactly mu>13/32-q/2; the missing complementary same-input estimate is p3>=5/32-(3/2)d, d=3/8-q. Alternatively one must exclude every actual attained smooth negative minimizer satisfying the full nonlinear equation and all complex second variations, or produce a genuine physical counterexample. An arbitrary prescribed spectrum or nonphysical tensor does neither.

Every center and relative-sector obligation remains. The unresolved estimate is (1/16)||P5||_3^2<=(1/64)||P3||_3^2+(3/2)||P4||_3^2+R_mid(f)+R_tail(f), for every actual completed Bargmann input f, with the earlier weighted norms, every center coefficient, every M=6,…,63 contribution and the entire M>=64 tail. The newly proved analytic regularity supplies neither their signs nor permission to drop them; the physical middle-sector obstruction remains. No finite-energy approximation or numerical minimum settles this all-input assertion. Even a future actual e3 counterexample would refute this sufficient determinant route alone and would not automatically refute entropy. The accepted rank<=5 entropy argument is not extended to arbitrary output rank. Unrestricted balanced-Fock-two entropy, the countable spectral/ENNReal entropy bridge, the all-n/all-eta Conjecture 1 and a full description of the Hessian kernel all remain open.

The one-mode space is lp(Function.const(Nat,Complex),2) and the two-mode space is lp(Function.const(Nat,lp(Function.const(Nat,Complex),2)),2). The occupation vector at n is lp.single 2 n (Complex.ofReal 1). All state and environment supports are unrestricted. conjStarAlgEquiv is Mathlib LinearIsometryEquiv.conjStarAlgEquiv, mapping T to U composed with T and U inverse. Function names are the displayed Lean definitions or the explicitly stated Mathlib operations. Application parentheses retain grouping; NatSub is truncated natural subtraction, val is the natural value of a finite index, toReal is the natural-to-real cast and Complex.ofReal is the real-to-complex cast. Fields carrying proofs are omitted from constructor formulas; when a named proof parameter occurs in a function signature it appears as an argument of that function.

T3: entropy on every normal density with actual output rank at most five. For the same balanced channel with environment |2><2|, every normal trace-one positive input rho satisfies S(Phi(rho))>=(3/2)log 2 whenever rank Phi(rho)<=5, with equality if and only if rho is a coherent pure state. Entropy is in nats. This includes arbitrary infinite input rank, Fock support, photon moments and input entropy. The pure classification and homogeneous complex quadratic identity are T1-T2 in Attenuator. The earlier rank-three argument remains a specialization. The following proof uses a finite-dimensional actual output support, not a finite input ensemble or an occupation truncation.

The same-channel purity prerequisite and positive attribution. Zixuan He, The energy cost of optical noise, version 1.0, https://zenodo.org/records/23629201, DOI 10.5281/zenodo.23629201, Theorem 8, proves the all-normal balanced-Fock purity maximum c_n=4^(-n)binomial(2n,n), with coherent local equality for n=0 or n>=2. Section 8.1, equations (38),(40), gives the bounded copy kernel; for n=2 its relative occupation weights are 3/8,1/4,3/8 at 0,2,4. Appendix F forces purity and coherent equality using the missing relative degree-two coefficient; Appendix D supplies normal-state trace-norm completion. Thus the purity maximum, kernel and equality are established literature inputs, consistent with the source-supported copy calculation above. Theorem 8 concerns Renyi-2 and does not itself establish the present rank-restricted von Neumann entropy inference or the global entropy conjecture. No additional stability estimate is needed for the proof of T3.

Finite determinant comparison for the pure class. Let a be unit with rank sigma_a<=5. T2 makes its rank three or four. On this same actual sigma_a, He purity gives e2=(1-Tr(sigma_a^2))/2>=5/16, while T1 and completed covariance give e3>=1/32, strictly for every noncoherent a. For its finite positive eigenvalue list lambda, zeros may be appended freely, and D_sigma(t)=product_i(1+t lambda_i)=sum_k e_k t^k. Since every higher e_k is nonnegative, D_sigma(t)>=1+t+(5/16)t^2+(1/32)t^3=(1+t/2)(1+t/4)^2=D_star(t) for every t>=0. For noncoherent a the strict e3 excess makes this strict for every t>0, including the noncoherent rank-three cases. No spectrum is chosen independently of the physical input.

The finite log-integral identity, including unequal ranks and zeros. For any two finite nonnegative lists lambda,mu of equal sum one, set L(t)=sum_i log(1+t lambda_i)-sum_j log(1+t mu_j). Equal trace gives L(t)=O(t^2) at zero. At infinity L(t)=O(log t), even with different ranks, so both boundary terms in integration by parts vanish and integral_0^infinity L(t)dt/t^2=integral_0^infinity L’(t)dt/t. For a finite upper endpoint T, use lambda/[t(1+t lambda)]=lambda/t-lambda^2/(1+t lambda). Equal trace cancels the 1/t terms, giving the limit of -sum_i lambda_i log(1+T lambda_i)+sum_j mu_j log(1+T mu_j). The log T terms cancel too, and the limit is -sum_i lambda_i log lambda_i+sum_j mu_j log mu_j. A zero eigenvalue contributes zero throughout, with 0 log 0=0; invertibility and equal ranks are unnecessary. Taking mu=(1/2,1/4,1/4) proves S(sigma)-S_star=integral_0^infinity log(D_sigma(t)/D_star(t))dt/t^2. Determinant domination gives nonnegative entropy excess. Its strict continuous integrand on every t>0 for noncoherent inputs gives strict entropy excess, while coherent inputs have the reference spectrum and equality. Credit for the finite elementary-symmetric/logarithm mechanism belongs to Sra, arXiv:1509.05902v2, Proposition 2.1 and Theorem 2.3, as scoped above. The direct identity here supplies zeros, unequal ranks and strictness; it attributes no infinite trace-class or source-ENNReal bridge to that paper.

Exact source entropy on an arbitrary finite output subspace. The source vonNeumannEntropy is an ENNReal-valued infimum over all complete countable Hilbert bases, not a finite eigenvalue list by definition. For a rank-r positive trace-one operator, choose a unitary taking an orthonormal basis of its support to the first r occupation vectors and extend it across the infinite-dimensional kernel. Transporting every complete Hilbert basis by that unitary gives a bijection of the source infimum and preserves its diagonal quadratic forms and basisEntropy. This is the original basis-transport argument used inside PhaseCovariantAttenuatorCoherentRefutation.result. The diagonalized operator is Entropy.finiteDiagonal of the r eigenvalues. Entropy.finiteDiagonal_entropy then identifies the source value with ENNReal.ofReal of their Shannon entropy, including all zero directions in the kernel. Consequently T3’s exact source inequality is ENNReal.ofReal((3/2)log 2)<=Entropy.vonNeumannEntropy(Attenuator.attenuatorOperator at eta=1/2 and environment delta_2 applied to rho), with equality exactly for coherent pure rho. Here delta_2 means the ProbabilityVector of weight one at occupation 2. This is a complete analytic identification of the finite-rank case, pending its exact Lean realization; a five-by-five Shannon inequality alone would not be that source theorem. No full infinite-output spectral-entropy equivalence is required for T3.

The normal source spectral join and channel continuity. A source DensityOperator is positive bounded and has full occupation diagonal sum one. Equivalently its positive square root is Hilbert-Schmidt with squared norm one, hence rho is positive trace class. The compact spectral theorem yields rho=sum_j p_j |a_j><a_j| in trace norm, for a finite or countable orthonormal family, p_j>0 and sum_j p_j=1. This ensemble agrees with the actual source channel: the columns CFC.sqrt(rho)e_m used in outputVector have rank-one sum rho in trace norm, since the positive omitted tail has trace tending to zero. Tensor with the fixed environment |2><2|, conjugate by the completed beam unitary and take the normal partial trace. These operations are linear and trace-norm continuous (the channel contracts the trace norm on self-adjoint trace-class differences), and give exactly attenuatorOperator and its pure specializations. Therefore sigma=Phi(rho)=sum_j p_j sigma_j in trace norm, sigma_j=Phi(|a_j><a_j|), for the spectral ensemble too. This supplies the off-diagonal and infinite-rank source correspondence; it is not an assumption of finite input support or a replacement by diagonal input states.

Full common-output-support containment. Let S be the range support of sigma=Phi(rho), with dim S<=5. For every y in S-perp, trace-norm convergence gives 0=<y,sigma y>=sum_j p_j<y,sigma_j y>. Every term is nonnegative. Thus for each positive p_j the quadratic form vanishes on every such y. Positivity implies ||sigma_j^(1/2)y||^2=0, hence sigma_j y=0 on S-perp. Self-adjointness then gives range(sigma_j) contained in S. This establishes the entire operator support, including coherences, and rank sigma_j<=5 for every spectral vector. T2 and the strict pure entropy result therefore apply to every a_j. The support argument uses positivity of the full output, not only its occupation diagonal.

Countable concavity and the exact normal-density equality. All sigma_j and sigma are densities on the fixed space S; their entropies lie in [0,log(dim S)]. For the first N weights, put r_N=1-sum_{j<=N}p_j. If r_N>0 let tau_N=r_N^(-1)sum_{j>N}p_j sigma_j, a density on S. Finite entropy concavity gives S(sigma)>=sum_{j<=N}p_j S(sigma_j)+r_N S(tau_N)>=sum_{j<=N}p_j S(sigma_j); if r_N=0 the same statement is finite concavity directly. Taking the increasing limit yields S(sigma)>=sum_j p_j S(sigma_j)>=S_star. Boundedness on S ensures the sum is finite, without any assumption on the input’s entropy or energy. If S(sigma)=S_star, the sum of the nonnegative quantities p_j(S(sigma_j)-S_star) is zero. Every spectral vector is coherent up to phase by the strict pure result. Distinct normalized coherent vectors have overlap modulus exp(-|alpha-beta|^2/2)>0, and equal coherent parameters give proportional vectors. Neither can give two orthogonal spectral vectors. There is exactly one spectral term, so rho is coherent pure. Conversely every coherent pure rho has output spectrum (1/2,1/4,1/4) and attains equality. This proves T3 for all normal densities in the stated actual-output-rank class. It assumes no concavity of e3.

Mixed rank five is possible. The explanatory input rho=(|e1><e1|+|e2><e2|)/2 has diagonal output (3/8,1/16,3/16,3/16,3/16), in occupation order 0 through 4. Indeed the two pure outputs are respectively (3/8,1/8,1/8,3/8,0) and (3/8,0,1/4,0,3/8). All five averaged entries are positive and sum to one. Thus T2’s impossibility of rank five is specifically a pure-input statement, while T3 includes nonempty mixed rank-five cases. This is an explanatory example within the normal-density theorem.

Cumulative remaining region and the global obligation. T2 excludes every pure output of rank at most five. Combining it with the spectral, largest-eigenvalue, coherent-overlap and high-purity exclusions gives the necessary conditions rank sigma>=6 (infinite rank allowed), (17-5sqrt(5))/16<q<3/8-1/[10(2^20+1)], lambda_max(sigma)<1/2 and m(a)<2^20/(2^20+1) for any normalized physical input with G(a)<0. Here q=Tr(sigma^2) and m(a)=sup_alpha |<D(alpha)e0,a>|^2. The upper endpoint is strict: the high-purity implication q>=3/8-1/[10(2^20+1)] already gives G>=0, strictly for noncoherent inputs. That stability implication remains an analytic dependency pending formalization; its proof is not reproduced as part of T1-T3. These conditions establish neither attainability nor a full physical characterization or a uniform lower bound on spectral tail mass. The earlier general entropy-concavity boundary now forces an entropy-violating normal density to have an entropy-violating pure spectral component of output rank at least six, possibly infinite. No finite-rank minimizer or finite cutoff follows.

For normalized pure a, write d=3/8-q and p3=Tr(sigma^3). Newton’s identity gives 6G=2p3-5/16+3d, so the missing all-input same-channel estimate is p3>=5/32-(3/2)d. Equivalently it compares the real cycle expectation <a tensor3,T123(a tensor3)> with the swap defect (3/8)I-T12. A purity stability estimate alone supplies no adequate lower bound on that cycle. The exact full-sector identity and remaining inequality above retain every M=6,…,63 contribution, every center coefficient and the entire M>=64 tail. T1-T3 do not remove those terms or prove their remaining compatibility estimate. No physical negative-G example has been produced here, and even one would refute this sufficient e3 route without automatically refuting entropy. The unrestricted balanced two-photon entropy bound and Van Herstraeten-Guha-Cerf Conjecture 1 for every n and eta remain unresolved. All new T1-T3 arguments are analytic and pending formalization; the existing Lean theorems retain their own narrower statements.

Definition 1.1 (finiteDiagonal).

$$\forall N:\mathbb{N},(\forall p:\mathrm{Fin}\left(N\right)\to \mathbb{R},(\mathrm{finiteDiagonal}\left(N,p\right)=\sum _{k:\mathrm{Fin}\left(N\right)}(\mathrm{smul}\left(\mathrm{ComplexofReal}\left(p\left(k\right)\right),\mathrm{rankOne}\left(\mathbb{C},\mathrm{lpsingle}\left(2,\mathrm{val}\left(k\right),\mathrm{ComplexofReal}\left(1\right)\right),\mathrm{lpsingle}\left(2,\mathrm{val}\left(k\right),\mathrm{ComplexofReal}\left(1\right)\right)\right)\right))))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/Entropy.finiteDiagonal (✓ std3).

Citation. Alfred Wehrl (1978). General properties of entropy. DOI: 10.1103/RevModPhys.50.221. URL: https://doi.org/10.1103/RevModPhys.50.221.

Commentary.

The finite diagonal operator is the sum of p(k) times the occupation rank-one projector. Its definition allows arbitrary real entries; the entropy theorem supplies the bounds from zero to one.

Definition 1.2 (basisEntropy).

$$\forall T:\mathrm{ContinuousLinearMap}\left(\mathbb{C},\mathrm{lp}\left(\mathrm{Functionconst}\left(\mathbb{N},\mathbb{C}\right),2\right),\mathrm{lp}\left(\mathrm{Functionconst}\left(\mathbb{N},\mathbb{C}\right),2\right)\right),(\forall b:\mathrm{HilbertBasis}\left(\mathbb{N},\mathbb{C},\mathrm{lp}\left(\mathrm{Functionconst}\left(\mathbb{N},\mathbb{C}\right),2\right)\right),(\mathrm{basisEntropy}\left(T,b\right)=\sum _{n:\mathbb{N}}^{\prime }(\mathrm{ENNRealofReal}\left(\mathrm{negMulLog}\left(\mathrm{Re}\left(\mathrm{inner}\left(\mathbb{C},b\left(n\right),T\left(b\left(n\right)\right)\right)\right)\right)\right))))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/Entropy.basisEntropy (✓ std3).

Citation. Alfred Wehrl (1978). General properties of entropy. DOI: 10.1103/RevModPhys.50.221. URL: https://doi.org/10.1103/RevModPhys.50.221.

Commentary.

negMulLog(x)=-x log(x), with its continuous value zero at x=0. ENNReal.ofReal embeds a nonnegative real in the extended nonnegative reals; Complex.ofReal embeds a real scalar in Complex; on a density operator every diagonal probability lies in [0,1]. Natural logarithms give nats.

Definition 1.3 (vonNeumannEntropy).

$$\forall T:\mathrm{ContinuousLinearMap}\left(\mathbb{C},\mathrm{lp}\left(\mathrm{Functionconst}\left(\mathbb{N},\mathbb{C}\right),2\right),\mathrm{lp}\left(\mathrm{Functionconst}\left(\mathbb{N},\mathbb{C}\right),2\right)\right),(\mathrm{vonNeumannEntropy}\left(T\right)=\mathrm{iInf}\left((b:\mathrm{HilbertBasis}\left(\mathbb{N},\mathbb{C},\mathrm{lp}\left(\mathrm{Functionconst}\left(\mathbb{N},\mathbb{C}\right),2\right)\right))\mapsto (\mathrm{basisEntropy}\left(T,b\right))\right))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/Entropy.vonNeumannEntropy (✓ std3).

Citation. Alfred Wehrl (1978). General properties of entropy. DOI: 10.1103/RevModPhys.50.221. URL: https://doi.org/10.1103/RevModPhys.50.221.

Commentary.

The definition is the infimum over complete countable orthonormal bases of the diagonal Shannon entropy. Its equality with spectral von Neumann entropy for every density operator is literature-attested, following the eigenbasis and concavity characterization in Wehrl. The infinite-dimensional equivalence is not kernel-proved here. The kernel proves the finite diagonal spectral formula; the final refutation supplies the needed unitary invariance by transporting all Hilbert bases.

Theorem 1.4 (finiteDiagonal_entropy).

$$\forall N:\mathbb{N},(\forall p:\mathrm{Fin}\left(N\right)\to \mathbb{R},(((\forall j:\mathrm{Fin}\left(N\right),(0\le p\left(j\right)))\wedge (\forall j:\mathrm{Fin}\left(N\right),(p\left(j\right)\le 1)))\Rightarrow (\mathrm{vonNeumannEntropy}\left(\mathrm{finiteDiagonal}\left(N,p\right)\right)=\mathrm{ENNRealofReal}\left(\mathrm{shannonEntropy}\left(\mathrm{Fin}\left(N\right),p\right)\right))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/FockAttenuator/Entropy.finiteDiagonal_entropy (✓ std3). ∎

Citation. Alfred Wehrl (1978). General properties of entropy. DOI: 10.1103/RevModPhys.50.221. URL: https://doi.org/10.1103/RevModPhys.50.221.

Commentary.

Concavity of -x log(x), the subprobability row bound and the Parseval column sums give the lower bound in every complete basis. The occupation basis attains it. shannonEntropy is the frozen finite Shannon functional, sum_j negMulLog(p_j). The result does not require the finite entries to sum to one.

Complete analytical writeback R6, reconciled R7, and the local radius refinement

The following results use the same actual balanced Fock-two channel and all completed Hilbert domains fixed in the Attenuator narrative. They are analytic prose pending native formalization. They quantify over the full center coordinate, infinite sums, arbitrary complex phases and displacements, and the actual output moments; they do not replace C_aC_a* by a prescribed spectrum or globally dephase the environment.

WHOLE R6: all-degree radial compression, Gaussian sign, intrinsic F3, and a closed Gaussian tube

Put t=(x_1+x_2+x_3)/sqrt(3), u=(x_1-x_2)/sqrt(2), v=(x_1+x_2-2x_3)/sqrt(6), h_2=u^2+v^2, phi_k=h_2^k/(2^k k!), and Rad=closed span{phi_k:k>=0}. For every F=sum_{k>=0} b_k(t)phi_k with arbitrary completed center vectors and sum ||b_k||^2<infinity,

<F,(Q-Id/32)F>=(3/128)||b_2||^2+(7/384)sum_{k>=3}||b_k||^2.

This is a quadratic-form compression on H_center tensor Rad. It does not assert that Rad is invariant under q_rel and it does not turn relative Rayleigh values into output eigenvalues.

For every unit pure Gaussian Bargmann input f(z)=exp(alpha z^2/2+beta z+gamma), r=|alpha|<1, the actual same-input trace satisfies

G(a)>=r^4(9-2r^2)/384,

and therefore p3>=5/32-(3/2)(3/8-q)+r^4(9-2r^2)/128. Equality in this proved Gaussian class occurs exactly at r=0, the coherent vectors up to phase. For a nonzero unnormalized input, E(a)>=||a||^6[1/32+r^4(9-2r^2)/384].

For every nonzero completed Bargmann input the following are equivalent: f has no zero on C; f=exp(alpha z^2/2+beta z+gamma) with |alpha|<1; P3 uses the third derivative expression (f^2 f3-3ff1f2+2f1^3)/2 is identically zero; and the complete relative-degree-three projected vector F_(a,3) is zero. The zero-free/Gaussian classification is classical and is attributed below; the channel-specific sign and full F3 identity are the R6 content. A unit input with G<0 must have a Bargmann zero and nonzero F_(a,3).

Let Gauss be all unit pure Gaussian vectors, including phase and displacement, delta0=1/(2^20+1), and rhoG=7delta0^2/18432. Every unit completed physical a with inf_{b in Gauss}||a-b||<=rhoG satisfies G(a)>=0, whether or not the infimum is attained. Thus G(a)<0 implies distance(a,Gauss)>rhoG. This tube uses P8 as an analytical premise and is not a global nonradial sign theorem.

R6 proof

Step 1: Radial normalization, symmetry and Rayleigh reduction.

The complex coordinate change z_+=(u+i v)/sqrt(2), z_-=(u-i v)/sqrt(2) is unitary. Since h2=2z_+z_-, phi_k=z_+^k z_-^k/k! is exactly the normalized occupation |k,k>. Thus ||h2^k||^2=4^k(k!)^2, and distinct k are orthogonal.

Every real orthogonal transformation of the relative plane preserves h2. In particular copy permutations fix phi_k. The three conjugate transposition expectations therefore agree; call their common value tau_k. For gamma_k=<phi_k,T123 phi_k> and ell_k=<phi_k,q_rel phi_k>, the exact antisymmetrizer gives ell_k=(1-3tau_k+2 Re gamma_k)/6.

Different k have different relative degree. Degree preservation and the identity center factor remove their matrix elements for arbitrary completed b_k(t), regardless of overlaps between the center vectors. No entire-sector eigenvalue or output eigenvalue is being computed: ell_k is the declared relative Rayleigh value.

Step 2: All swap probabilities and monotonicity.

Expansion of h2^k gives probability p_j=binom(2j,j)binom(2k-2j,k-j)/4^k for pair-difference occupation 2j, 0<=j<=k. This follows directly from the normalized coefficient binom(k,j)sqrt((2j)!(2k-2j)!)/(2^k k!).

Pairing p_0,p_1,p_2 with the actual swap weights gives tau_0=3/8, tau_1=5/16 and tau_2=11/32. For k>=2, writing A_k=binom(2k,k)/4^k gives tau_k=A_k[3/8+k/(4(2k-1))+9k(k-1)/(16(2k-1)(2k-3))]. In particular tau_3=15/64.

A_(k+1)/A_k=(2k+1)/(2k+2)<1. The second rational factor decreases. For the third, k(k-1)/((2k-1)(2k-3))-(k+1)k/((2k+1)(2k-1))=2k/((2k-1)(2k-3)(2k+1))>0 for k>=2. All factors are positive. Hence tau_k strictly decreases for k>=2, and tau_k<=15/64 for EVERY k>=3. The k=0,1 cases were handled separately, so no invalid denominator is used.

Step 3: Complete environmental state, coefficients and the precise off-diagonal selection rule.

The inverse coordinate formulas give x1 x2 x3=[t^3-3t z_+z_- -i(z_+^3-z_-^3)]/(3sqrt(3)). Therefore the normalized environmental triple e2 tensor3 equals that numerator squared divided by 54sqrt(2). The squared denominator is 5832.

The numerator expands to t^6-6t^4z_+z_- -2it^3z_+^3+2it^3z_-^3+9t^2z_+^2z_-^2+6it z_+^4z_- -6it z_+z_-^4-z_+^6+2z_+^3z_-^3-z_-^6. For occupation (s,p,q), its normalized coefficient is the table’s numerator coefficient times sqrt(s!p!q!)/(54sqrt(2)); squaring gives every probability below. Their sum is (10+12+2+2+9+12+12+10+10+2)/81=1.

The retained cycle is identity on the retained center; conjugating by the center splitter consequently gives identity on BOTH input/environment centers. Orthogonality removes environmental entries with unequal s. In circular relative coordinates the conjugated cycle splits into two independent input/environment two-mode unitaries. They separately conserve N_input,+ + N_env,+ and N_input,- + N_env,-. Between input bra and ket |k,k>, an environmental entry |p,q><p’,q’| therefore contributes only when p=p’ and q=q’. This proves removal of the remaining environmental off-diagonal entries in THIS diagonal matrix element. It does not diagonalize the environmental state or justify deleting its coherences for other input bra/ket pairs.

Step 4: Actual splitter phases and all-k cycle formula.

For the source one-particle splitter B=[[1,-1],[1,1]]/sqrt(2), B^T diag(exp(i theta),1) B=exp(i theta/2)[[cos(theta/2),-i sin(theta/2)],[-i sin(theta/2),cos(theta/2)]]. A relative retained three-cycle has theta=+/-2pi/3, hence cos(theta/2)=1/2. Reversing the cycle or interchanging the circular labels conjugates the intermediate phases and leaves every table phase unchanged.

The coefficient returning |k,j> to itself is obtained by choosing l exchanged particles from each creation polynomial. Since the same occupations occur in bra and ket, normalization cancels. This yields exp(i theta(k+j)/2)2^(-(k+j))H_j(k), H_j(k)=sum_{l=0}^{min(j,k)}(-3)^l binom(j,l)binom(k,l). The ratio -3 is the square of the off-diagonal/diagonal entry, including its sign.

For environmental (p,q) the two-mode product is exp(i pi(p-q)/3)4^(-k)2^(-(p+q))H_p(k)H_q(k). Its phase is -1 precisely on (3,0),(0,3),(4,1),(1,4), including all relative environmental degree-three and degree-five rows. The degree-six endpoint rows have phase +1.

Summing all ten rows gives gamma_k=4^(-k)/81[10+3H_1^2-H_3/2+9H_2^2/16-3H_1H_4/4+5H_6/16+H_3^2/32]. Thus gamma_k is real for every integer k>=0. The fixed upper environmental occupation six is the exact state support; there is no input-degree cutoff.

Step 5: Exact polynomial identity, all-degree sign and completed compression.

Direct expansion of the defining finite binomial sums gives H_1=1-3k; H_2=(9k^2-21k+2)/2; H_3=(-9k^3+54k^2-63k+2)/2; H_4=(27k^4-306k^3+945k^2-762k+8)/8; H_6=(81k^6-2187k^5+20655k^4-83745k^3+142344k^2-78588k+80)/80. These are polynomial identities for all k>=0 because the falling-factorial terms vanish when their index exceeds k, including the small k cases.

Let B_k=320+96H_1^2-16H_3+18H_2^2-24H_1H_4+10H_6+H_3^2. Independently collecting its coefficients gives 8B_k=(243,-2187,8991,-35073,93798,-63828,3240) in descending powers k^6,…,1. This is exactly 81 times (3,-27,111,-433,1158,-788,40). Consequently B_k=(81/8)C(k), and substitution into the preceding cycle expression gives gamma_k=C(k)/(256*4^k), C(k)=3k^6-27k^5+111k^4-433k^3+1158k^2-788k+40.

The exact small values are C(0)=40, C(1)=64, C(2)=736, C(3)=1024. Independently shifting the polynomial gives C(x+4)=3x^6+45x^5+291x^4+863x^3+858x^2-20x+760. At integer x=0 this is 760>0. At every integer x>=1, 858x^2-20x>=838x>=0 and every other displayed term is nonnegative, including the positive constant. This proves C(k)>0 for every natural degree k; it is a finite base-case plus polynomial proof, not sample-based sign evidence.

Thus gamma_0=5/32, gamma_1=1/16, gamma_2=23/128, and the exact swap values give ell_0=ell_1=1/32 and ell_2=7/128. For every k>=3, ell_k-1/32=(13/16-3tau_k+2gamma_k)/6>=7/384; in fact it is strictly greater since gamma_k>0. The k=2 gap is 3/128.

For finite radial sums with arbitrary center vectors the quadratic form is exactly sum_k(ell_k-1/32)||b_k||^2. Boundedness of Q and orthogonal Hilbert convergence extend this identity and its lower bound to every l2 sum. Equivalently the compression P_Rad q_rel P_Rad is diagonal in phi_k. No assertion that q_rel maps Rad to Rad is used, and no radial-angular cross term for a general nonradial input is discarded.

Step 6: Full physical Gaussian class and its exact infinite cube.

For arbitrary complex alpha,beta with r=|alpha|<1, choose delta=(beta+alpha conjugate(beta))/(1-r^2). Then delta-alpha conjugate(delta)=beta. In the source convention D(-delta)f(z)=exp(-|delta|^2/2-delta z)f(z+conjugate(delta)); its linear exponent is beta+alpha conjugate(delta)-delta=0. A number rotation makes alpha=r. Covariance preserves the actual output moments, and scalar phase is immaterial.

The normalized representative is a_r(z)=(1-r^2)^(1/4)exp(rz^2/2). Indeed its squared unnormalized norm is sum_{n>=0}binom(2n,n)(r^2/4)^n=(1-r^2)^(-1/2). The coordinate unitary preserves sum_i x_i^2=t^2+h2. Hence the transformed SAME physical cube is exactly a_r(t) sqrt(1-r^2) exp(rh2/2)=a_r(t) sqrt(1-r^2) sum_{k>=0}r^k phi_k. The full center vector a_r(t) has norm one. The relative squared weights are (1-r^2)r^(2k), sum to one, and are nonzero at all k when r>0.

Applying the completed compression yields G(a_r)>=(3/128)(1-r^2)r^4+(7/384)(1-r^2)sum_{k>=3}r^(2k)=r^4(9-2r^2)/384. This keeps the entire center and every middle/high even relative degree. No finite output-rank or energy assumption is used. At r=0 the actual coherent output has spectrum (1/2,1/4,1/4), giving G=0; at every r>0 the displayed lower bound is positive (and the inequality against it is also strict by the positive tail weights and strict Step 5 bound).

Completed displacement and number-phase covariance return every original complex squeezing angle, beta and gamma compatible with unit normalization. Degree-six homogeneity gives the unnormalized statement. Finally p3-5/32+(3/2)d=3G gives precisely the claimed strengthened trace inequality, with denominator 128 in the added term.

Step 7: Classical zero-free classification and the actual full F3 equivalence.

A nonzero zero-free entire f on the simply connected plane has an entire logarithm g. Completed coherent evaluation gives Re g(z)=log|f(z)|<=log||a||+|z|^2/2. Borel-Caratheodory on disks of radii R and 2R bounds sup_{|z|<=R}|g(z)-g(0)| by O(1+R^2). Cauchy’s estimates imply g^(j)(0)=0 for every j>=3 as R tends to infinity. Thus g=gamma+beta z+alpha z^2/2.

After a rotation making alpha=r>=0, the squared Bargmann integrand has exponent -(1-r)x^2-(1+r)y^2+2 Re(beta)x-2 Im(beta)y+constant. For r>1 its x quadratic grows. For r=1 the x integral is an exponential of a linear function, which diverges whether the slope vanishes or not. For r<1 both quadratic forms decay and any beta is integrable. Thus the precise boundary is |alpha|<1, and conversely every such exponential quadratic is zero-free and belongs to H.

On a zero-free disk P3=f^3(log f)’‘’/2. At ANY zero z0 of multiplicity m>=1, write f(z)=c(z-z0)^m+O((z-z0)^(m+1)), c!=0. The coefficient in P3 at power 3m-3 is c^3[m(m-1)(m-2)-3m^2(m-1)+2m^3]/2=m c^3, nonzero. This includes m=1 and m=2, with the vanishing falling-factorial terms handled directly. Hence P3 identically zero forbids every zero, and then forces g’‘’=0; the converse is immediate for exponential quadratics.

The inherited full completed projection is F_(a,3)=P3(t/sqrt(3))h3, h3=(3u^2v-v^3)/(3sqrt(6)), with ||h3||^2=4/9. Its whole center norm is ||P3||3^2=(3/pi) integral |P3(c)|^2 exp(-3|c|^2)d^2c, so ||F(a,3)||^2=(4/9)||P3||3^2. Bounded projections and bounded center evaluation show F(a,3)=0 iff P3 is identically zero. Individual scalar derivatives need not lie in H. The completed identity, with all center coefficients, is essential; a coefficient evaluated only at center vacuum would be insufficient.

The zero-free/Gaussian equivalence is established classical mathematics, explicitly stated by Chabaud-Markham-Grosshans and attributed there to Lutkenhaus-Barnett. The direct logarithm proof above independently supplies the precise Fock/integrability hypotheses. R6 adds the channel-specific sign and intrinsic use of F3, not a new classification priority claim.

Step 8: Entire uniform closed tube, both squeezing ranges and a nonattained infimum.

For unit a,b, tensor telescoping gives ||a tensor3-b tensor3||<=3||a-b||. Since ||Q||<=1, the difference of its quadratic forms is at most 2||a tensor3-b tensor3||, and the two subtractions 1/32 agree. Hence |G(a)-G(b)|<=6||a-b||. Also sqrt(m) is 1-Lipschitz and lies in [0,1], so |m(a)-m(b)|<=2||a-b||.

For the centered real Gaussian b=a_r, its coherent-overlap square at z is sqrt(1-r^2)exp(-|z|^2+r Re z^2). This is maximized at zero since r<1. Displacement, phase and rotation preserve m, so EVERY unit Gaussian has m(b)=sqrt(1-r^2).

If r^2<=delta0/2, m(b)>=1-r^2>=m0+delta0/2. Thus at distance at most rhoG, m(a)>=m0+delta0/2-2rhoG>m0, and P8 gives G(a)>=0, strictly unless a is coherent. The strict margin holds because 2rhoG=7delta0^2/9216<delta0/2.

If r^2>=delta0/2, Step 6 gives G(b)>=7r^4/384>=7delta0^2/1536. Since 6rhoG=7delta0^2/3072, Lipschitz continuity gives G(a)>=7delta0^2/3072>0. The split covers all r<1, including arbitrarily large physical squeezing.

For d=inf_{b in Gauss}||a-b||<=rhoG, choose b_n with ||a-b_n|| tending to d; no minimizer in Gauss is assumed. One of the two ranges contains an infinite subsequence. In the small range pass m(a)>=m0+delta0/2-2||a-b_n|| to the limit. In the large range pass G(a)>=7delta0^2/1536-6||a-b_n|| to the limit. The same strict margins survive at d=rhoG. Therefore the ENTIRE closed tube is excluded without compactness of the Gaussian orbit, an energy premise, or a new sign assumption.

R6 F0–F7 and exact ten-row environment selection rule

R6 F0–F7 native interfaces

F0. Join the actual completed occupation/Bargmann model, C_a, Phi, V tensor3, antisymmetrizer Q, center/relative unitary, conserved-degree blocks, positive transposition kernel and completed arbitrary-input displacement/number-phase covariance. Preserve sigma_a=C_a C_a*, trace-class moments, the identical input in every factor and source normalization.

Native boundary: The immutable Scribe confirms the analytical contract and provenance. It is not a new Lean theorem inventory, build or axiom receipt. A coherent-only covariance theorem is too weak.

F1. Supply the circular relative-mode unitary, normalized occupations phi_k, their orthonormality and permutation invariance, degree-orthogonal matrix elements, and tensoring with every completed center vector. Formulate P_Rad q_rel P_Rad or its quadratic form without asserting Rad invariant.

Native boundary: A finite radial span or center-vacuum lemma is a useful intermediate only; the delivered theorem must quantify over the full Hilbert tensor subspace.

F2. Prove the six-photon polynomial and all ten normalized occupation coefficients; derive the source splitter-conjugated cycle and all-k creation-polynomial diagonal amplitude. Establish the two separate conserved occupations to remove environmental coherences solely for the declared diagonal input matrix element.

Native boundary: Replacing the relative environment by a diagonal state globally would change the problem and would lose legitimate nonradial cross terms. Retain odd relative degrees three and five with their phases.

F3. Prove the all-k binomial H_j formulas, the exact degree-six identity, shifted positivity for all natural k, swap probabilities and rational monotonicity, and the exact low Rayleigh values. Combine them with the antisymmetrizer identity and legitimate real/conjugate trace conventions.

Native boundary: The displayed exact algebra is independently checked mathematics. Formal arithmetic/binomial/order proofs still need kernel checking on the authorized machine. Neither computed samples nor an invented positivity axiom can supply the all-k theorem.

F4. Extend the bounded degree-diagonal quadratic form to all l2 sums with completed center vectors; prove Gaussian normalization, the exact physical cube factorization and its infinite geometric weights. Apply arbitrary complex displacement/phase covariance and degree-six homogeneity.

Native boundary: No invariant-subspace supplier, energy restriction, I<1/32 premise, IFT or Lojasiewicz theorem is needed. A theorem only for finite squeezed-state truncations is insufficient.

F5. For the full intrinsic conclusion supply a lawful entire logarithm plus Borel-Caratheodory and Cauchy estimates, or an exactly matching proved zero-free Fock classification. Prove the |alpha|=1 divergence boundary, the zero-multiplicity coefficient for every m, and reuse the actual bounded completed F3/P3 identity with its weighted center norm.

Native boundary: Current native availability is unassessed, not claimed absent. Literature cannot be admitted as a Lean axiom. This conclusion may be independent of the radial proof in dependency order, but remains required for a complete R6 delivery.

F6. Reuse P8 through its original owner; prove the 6-Lipschitz G estimate, 2-Lipschitz m estimate, exact Gaussian coherent maximum, both squeezing ranges, constants and the approximating-sequence argument at an unattained infimum.

Native boundary: No compactness of Gauss or differentiability of a maximizing center is required. All unit completed a in the closed tube are included. The P8 analytical statement is a dependency, not a fresh native receipt.

F7. Existing authorized same owners retain source search, faithful D5/Blueprint echo, utility and proof-shape obligations, Reg attempt or honest linked-issue exception, scoped kernel/axiom evidence, deposit, independent repository assessment, required checks and lifecycle custody. Preserve all P/T/A/R scopes and global abstentions.

Native boundary: No active owner, native worktree, supplier inventory, CI, publication or merge was inspected or certified. This mathematical assessment is not a repository vote and creates no new implementation owner.

The six-photon environment numerator in circular relative coordinates is

t^6-6t^4 z_+z_- -2i t^3z_+^3+2i t^3z_-^3+9t^2z_+^2z_-^2+6it z_+^4z_- -6it z_+z_-^4-z_+^6+2z_+^3z_-^3-z_-^6,

normalized by 54sqrt(2). The ten rows (s,p,q; numerator coefficient; probability; cycle phase) are:

| (s,p,q) | coefficient | probability | phase | |—|—:|—:|—:| | (6,0,0) | 1 | 10/81 | +1 | | (4,1,1) | -6 | 4/27 | +1 | | (3,3,0) | -2i | 2/81 | -1 | | (3,0,3) | 2i | 2/81 | -1 | | (2,2,2) | 9 | 1/9 | +1 | | (1,4,1) | 6i | 4/27 | -1 | | (1,1,4) | -6i | 4/27 | -1 | | (0,6,0) | -1 | 10/81 | +1 | | (0,0,6) | -1 | 10/81 | +1 | | (0,3,3) | 2 | 2/81 | +1 |

The probabilities sum to one. The cycle is identity on the retained center, and circular input/environment occupations are separately conserved. Therefore an environmental matrix element contributes to this diagonal matrix element only when p=p’ and q=q’. This removes off-diagonal environmental entries only for the declared |k,k> input matrix element; it does not diagonalize the environmental state for other input bra/ket pairs. The odd degree-three and degree-five rows retain their negative phases.“

R6 global residuals

The unrestricted physical sign remains open. The full obligation is (1/16)||P5||_3^2 <= (1/64)||P3||_3^2+(3/2)||P4||_3^2+R_mid(f)+R_tail(f), with ||P||_3^2=(3/pi) integral |P(c)|^2 exp(-3|c|^2)d^2c, every M=6,…,63 term, every M>=64 term, and every center coefficient. The invariant relative M=5 vector (3/8)h2h3 has gap -9/1024 on the whole symmetric tensor space but is not a physical tensor cube. The actual e0+epsilon e14 family prevents deleting R_mid even with the full tail, while its actual G is positive near zero. No cutoff, assumed radial invariance, holomorphic-cubic SOS, or arbitrary spectrum replaces the physical problem. A negative minimizer still has rank(sigma)>=6 allowing infinity, (17-5sqrt(5))/16<q<3/8-1/[10(2^20+1)], ||sigma||<1/2, and sqrt((4-sqrt(10))/24)<m(a)<2^20/(2^20+1); R5 additionally supplies uniform sixth-eigenvalue and tail mass near the bottom. These are necessary conditions only.

WHOLE R7: all N>=3, all amplitudes, a closed completed tube, and exact-family finite-rank entropy

For every integer N>=3, A,B,alpha in C, let a=D(alpha)(A e0+B eN). The actual output trace obeys the homogeneous estimate

G(a)>=[18|A|^4|B|^2+15|A|^2|B|^4+14|B|^6]/768.

This includes A=0, B=0, zero, arbitrary phases, and every displacement. For a unit input w=|B|^2, the same actual output satisfies G(a)>=w(18-21w+17w^2)/768>=w/128 and

p3>=5/32-(3/2)(3/8-q)+w(18-21w+17w^2)/256.

Equality G=0 in this exact family occurs precisely for B=0, the coherent class. N=1,2 retain their separate accepted T1 scope. No all-input sign follows.

Let Vnum={D(alpha)(A e0+B eN): N>=3, |A|^2+|B|^2=1}, delta0=1/(2^20+1), rhoV=delta0/3072. Every unit completed input with inf_{b in Vnum}||a-b||<=rhoV has G(a)>=0, and equality in this closed tube is exactly coherent up to phase. The infimum need not be attained; perturbations in the tube may have arbitrary infinite support and infinite mean photon number.

For every unit member of Vnum, the actual finite-rank output satisfies S(sigma)>=(3/2)log 2 in nats, strictly when B!=0, with equality exactly for coherent inputs. This is an analytical finite-spectrum comparison on the exact family. The source ENNReal vonNeumannEntropy identification still needs the existing finite-rank unitary/basis-transport join and retains the infinite zero kernel. No entropy theorem for the whole tube, all inputs, all mixtures, or a countable spectral bridge is claimed.

R7 proof

R7 Step 1.

The balanced e2 channel is the fixed actual map sigma_a=C_a C_a*. Displacement conjugates sigma by D(alpha/sqrt(2)); scalar and number phase reduce A!=0 to e0+t eN with t>=0 for this one-number family. Degree-six homogeneity restores EVERY complex A,B,alpha. A=0, B=0 and zero are retained. No many-coefficient phase reduction is inferred.

R7 Step 2.

H=C_e0 has H02=H20=1/2 and H11=-1/sqrt(2); J=C_eN is real symmetric and supported on i+j=N+2. For EVERY N>=3 its low {0,1,2} compression is zero, hence HJH=0. J^2 is diagonal with beta0=(N+2)(N+1)/2^(N+3), beta1=(N+1)(N-2)^2/2^(N+3), beta2=(N^2-5N+2)^2/2^(N+4). For x=beta0+beta2, b=beta1, the three disjoint partner indices and total mass give x+b<=1/2. Preserve the accepted P8 FULL-G coefficient c_N=7/32-3x/8-b/2=7/32-P(N)/2^(N+7)>=3/128. Here P(N)=3N^4-22N^3+69N^2-42N+56; its N=3,4,5,6 bases satisfy P(N)<=25*2^N and, at N=6+j, 2P(N)-P(N+1)=3j^4+38j^3+153j^2+198j+48>0. This coefficient and induction belong to P8, not new R7 novelty.

R7 Step 3.

For the actual two-copy input eN tensor eN, the difference-occupation 2j probability is binom(2j,j)binom(2N-2j,N-j)/4^N. The physical swap weights give q_N=Tr J^4=A_N[3/8+N/(4(2N-1))+9N(N-1)/(16(2N-1)(2N-3))], A_N=binom(2N,N)/4^N, N>=2. A_(N+1)/A_N=(2N+1)/(2N+2)<1; N/(2N-1) decreases and the difference of N(N-1)/((2N-1)(2N-3)) at N and N+1 is 2N/((2N-1)(2N-3)(2N+1))>0. Therefore q_N<=q_3=15/64 for ALL N>=3. The exact beta1 bases are b3=1/16,b4=5/32,b5=27/128,b6=7/32; for N>=6 its decreasing recurrence is equivalent to N^3-6N^2+3N+6>=0, whose N=6+j expansion is j^3+12j^2+39j+24>0. Thus b<=7/32 and U=x+2b<=23/32<3/4. These are all-N analytical identities, not sampling or an arbitrary-spectrum substitution.

R7 Step 4.

Only for the lawful real representative, C=H+tJ is self-adjoint and the SAME actual output is C^2. Covariance makes the moment polynomials even. With y=t^2 and v_N=Tr J^6>=0, p2=3/8+U y+q_N y^2 and p3=5/32+W y+V y^2+v_N y^3. U=4Tr(H^2J^2)=x+2b; W=6Tr(H^4J^2)=3x/8+3b/2; V=6Tr(H^2J^4)+3Tr(HJ^2HJ^2)=3(beta0^2+beta2^2+beta0 beta2)/2+9b^2/2. The fourth-power two-J classes have multiplicities 4,2, with HJHJ vanishing. The sixth-power two-J classes have multiplicities 6,6,3 and traces H^4J^2,H^3JHJ,H^2JH^2J; HJH=0 kills the last two. The four-J classes likewise have multiplicities 6,6,3 and traces H^2J^4,HJHJ^3,HJ^2HJ^2; only the middle vanishes. H^2 has diagonal (1/4,1/2,1/4), H^4 has diagonal (1/16,1/4,1/16), and Tr(HJ^2HJ^2)=(beta0 beta2+b^2)/2 is retained and generally NONZERO. No complex-input replacement of CC* by C^2 occurs.

R7 Step 5.

Newton gives exactly 6G=2p3-3(1+y)p2+(13/16)(1+y)^3=kappa2y+kappa4y^2+kappa6*y^3, with kappa2=2W-3U+21/16=6c_N>=18/128, kappa4=2V-3(U+q_N)+39/16, kappa6=2v_N-3q_N+13/16. Since beta0 beta2<=x^2/4, V>=9x^2/8+9b^2/2>=(9/16)U^2; the latter difference is (9/16)(x-2b)^2. Hence kappa4>=(9/8)U^2-3U+111/64>=15/128 on 0<=U<=3/4. Finally kappa6>=13/16-45/64=7/64=14/128. No discarded sector or assumed middle-sector sign enters.

R7 Step 6.

The exact coefficient bounds and homogeneity give G(D(alpha)(A e0+B eN))>=[18|A|^4|B|^2+15|A|^2|B|^4+14|B|^6]/768 for every N>=3 and every complex amplitude/displacement, including A=0 and zero. For unit inputs w=|B|^2, this is w(18-21w+17w^2)/768>=w/128: the bracket minus 6 equals 12(1-w)^2+3w(1-w)+8w^2>=0. Thus G>0 when B!=0 and G=0 exactly on the coherent B=0 class for nonzero inputs in this family. The SAME output obeys p3>=5/32-(3/2)(3/8-q)+w(18-21w+17w^2)/256 by p3-5/32+(3/2)(3/8-q)=3G. This does not assert sharpness or equality of the lower polynomial bound. The separate prior N=1,2 T1 formulas keep their original scope.

R7 Step 7.

The original explicitly assigns m(a)>m0 to the w<=delta0/2 branch and G(a)>=delta0/512>0 to the w>=delta0/2 branch. P8 supplies G>=0 and strictness unless coherent only in the first branch. Lipschitz constants 6 and 2, both endpoint-inclusive ranges, the exact rhoV=delta0/3072, and an approximating-sequence argument over unbounded N and displacement give the complete closed tube without attainment, compactness, support, energy or moment assumptions. Exact quotation and the limit proof are in source_adjudication. No substantive Step 7 correction is required.

R7 Step 8.

For every UNIT exact family member, support before displacement is rows/columns 0,…,N+2 and covariance preserves rank<=N+3. Physical q<=3/8 gives e2=(1-q)/2>=5/16; e3=1/32+G>=1/32, strictly for B!=0. All higher elementary symmetric coefficients are nonnegative, so D_sigma(t)>=1+t+(5/16)t^2+(1/32)t^3=(1+t/2)(1+t/4)^2=D_star(t) for t>=0. Finite nonnegative eigenvalue lists allow arbitrary zero padding: a zero contributes factor one and 0 log 0=0. Equal trace makes log(D_sigma/D_star)=O(t^2) at zero, while finite rank gives O(log t) at infinity. Thus boundary terms in integration by parts vanish, equal-trace terms cancel, and integral_0^infinity log(D_sigma(t)/D_star(t))dt/t^2=-sum lambda_i log lambda_i+sum lambda_star,j log lambda_star,j=S(sigma)-(3/2)log 2. Strict e3 makes the integrand positive for EVERY t>0 when B!=0. The exact family has S>=(3/2)log 2, with coherent equality. Its repository ENNReal vonNeumannEntropy identification still requires the finite-rank unitary/basis-transport interface, preserving the infinite zero kernel. Neither infinite-rank tube entropy nor the general countable spectral bridge is claimed.

R7 F0–F5 and the reconciled Step 7

R7 original F0–F5 mapping

F0. Reuse actual completed C_a, Phi, moment/Newton, arbitrary-input covariance, Q and trace joins through existing owners. The real-symmetric trace shortcut must follow phase reduction for this one-number family, never replace C C* on general complex inputs.

Native boundary: Analytical supplier assumptions only; no current native declaration inventory, compilation or axiom receipt.

F1. Reuse P8 full-G all-N c_N through its original owner; prove the actual two-copy Fock probability join to the R6 binomial/monotonicity calculation, beta_i formulas, paired endpoint mass, beta1 bound and all-N recurrence.

Native boundary: All hypotheses and exact inequalities are displayed above. These are ordinary all-natural-index algebra/probability statements, not an experimental or numeric oracle.

F2. Supply the full fourth/sixth trace word identities with multiplicities, H J H annihilation, diagonal J^2 and the NONVANISHING HJ^2HJ^2 term. Prove coefficient positivity, homogeneity, degenerate cases, normalization and exact same-output trace join.

Native boundary: Complete analytical proof proposed for independent assessment. A near-zero coefficient theorem, a finite list of N or a truncated relative-sector theorem is insufficient.

F3. Reuse P8 through its original owner and bounded full Q for both Lipschitz estimates; prove the uniform infimum-distance tube over unbounded N and displacement with both strict margins and all completed perturbations.

Native boundary: No compactness or attainment of Vnum, differentiable center choice, energy or support premise is required.

F4. For the restricted finite-rank entropy consequence, supply rank<=N+3 and covariance, finite spectral nonnegativity/Newton, determinant comparison and the zero-allowing integral. Join the analytic spectral entropy to source vonNeumannEntropy by the existing finite-rank unitary/basis-transport interface, preserving the infinite zero kernel.

Native boundary: No countable spectral/ENNReal native bridge is claimed. T3 retains its original rank<=5 theorem scope; this separately proved family consequence does not rewrite it.

F5. Existing authorized owners retain source search, D5/Blueprint faithful echo, utility/proof-shape, Reg attempt or honest linked-issue exception, kernel/axiom evidence, deposit, independent repository review, required checks and lifecycle custody.

Native boundary: This worker creates no implementation owner and performs or certifies none of those operations. No native acceptance, publication, merge or original parent completion follows.

The Step 7 wording is valid as originally written. For a unit b=D(alpha)(A e0+B eN), w=|B|^2 and d=||a-b||<=rhoV, respectively means two branches: if w<=delta0/2 then m(a)>=m0+delta0/2-2d>m0, so P8 gives G(a)>=0, with equality exactly when a is coherent; if w>=delta0/2 then G(a)>=delta0/256-6d>=delta0/512>0. For an unattained infimum d*=inf_{b in Vnum}||a-b||, choose b_j with actual distances d_j->d*. One branch occurs infinitely often and the corresponding inequality passes to the limit. Coherent vectors lie in Vnum with B=0, so equality in the closed tube is exactly coherent. No compactness or attainment is used. The earlier assessment’s proposed deletion of a small-w G-margin was a source misreading: the original assigns the m-margin to small w and invokes P8 there; the delta0/512 margin belongs to the large-w branch. The retained Sra source bytes are sra-v2.html, 158886 bytes, SHA256 77385ef6c2bf5ed158be92558f7ba039a2fad5718d2a14cc31b56e956c238a84, URL https://arxiv.org/html/1509.05902v2.

Local full-completed-complex radius refinement

For every complex z and every completed b perpendicular to e0,e1,e2, put u=z e2+b, rho^2=|z|^2+||b||^2 and D=||b||^2+|z|^4. If rho<=1/512, then

G(e0+u)>=(127/32768)D,

strictly for u!=0. The proof begins with the exact operator annihilations K(e0 tensor3)=0 and KS(e2)=0 from the zero relative gaps, not merely a zero quadratic form. The P8 all-N coefficient c_N=7/32-P(N)/2^(N+7)>=3/128 for P(N)=3N^4-22N^3+69N^2-42N+56 is completed over every complex l2 b by total-degree orthogonality and truncation. With w=z^2 and T4=e2 tensor e2 tensor e0+e2 tensor e0 tensor e2+e0 tensor e2 tensor e2, the exact complex phase-sensitive identity is

(1/64)|sqrt(2)b4-sqrt(3)w|^2+(3/2)|b4/(4sqrt(6))+w/8|^2=(3/64)|b4-w/sqrt(6)|^2+|w|^2/16.

For X=S(b)+z^2T4 one gets <X,KX> >=(3/128)D and ||X||^2=3D. The exact remainder in (e0+u) tensor3=e0 tensor3+zS(e2)+X+R is the six placements of z e2,b,e0, the three placements of b,b,e0, and u tensor3, with

||R||^2=6|z|^2||b||^2+3||b||^4+rho^6<=8rho^2D

for rho<=1. Since ||K||<=31/32<1, the annihilations give the full estimate

G(e0+u)>=[3/128-4sqrt(6)rho-8rho^2]D

on the entire rho<=1 expansion domain. At rho<=1/512, 4sqrt(6)<10 gives the coefficient at least 127/32768, strictly for rho>0. This includes all middle sectors, the infinite tail, nonradial cross terms and every center coefficient.

The completed coherent-overlap centering argument attains m(a), moves a maximizing gauge to sqrt(m)(e0+z e2+b), and forces a1=0 by differentiating the scalar Husimi overlap at its maximum. With m=(1+rho^2)^(-1), homogeneity gives

G(a)>=(127/32768)m^3D>=(127/32768)m(1-m)^2.

Thus the new threshold is m>=2^18/(2^18+1), and a negative physical G requires m<2^18/(2^18+1); the prior 2^20/(2^20+1) condition remains valid. No energy, moment, support, rank, global sign, entropy theorem, improved strip, or optimality claim follows.

The scalar statement for a trace-one positive operator with q<=3/8 and largest eigenvalue r>=1/2, namely p3>=(3/2)q-13/32 and e3>=1/32 with equality only at (1/2,1/4,1/4,0,…), is already the published largest-eigenvalue exclusion. Its Cauchy–Schwarz tail proof and the abstract spectrum (49/100,38/125,103/500,0,…) are retained only as explanatory reuse: the example has r<1/2 and is not asserted to be a physical output, and no duplicate theorem wrapper or new residual is counted.

R6/R7/local native and global boundary

Native availability for these analytical packages is unassessed. No Lean/Lake/LSP/.NET invocation, numerical or symbolic experiment, cutoff scan, sampling, new axiom, source implementation, PR review vote, CI result, publication, merge, or cleanup is certified by this writeback. P1–P8, T1–T3, A1–A6 and R1–R5 retain their original quantifiers, attributions, hypotheses, and native limitations. T3 remains rank<=5; the exact-family R7 entropy argument does not rewrite it. The unrestricted same-input trace, full middle/high sectors, general entropy/ENNReal bridge, all-n/all-eta conjecture, and all-input equality classification remain open.

Definition 1.1 (finiteDiagonal).

$$\forall N:\mathbb{N},(\forall p:\mathrm{Fin}\left(N\right)\to \mathbb{R},(\mathrm{finiteDiagonal}\left(N,p\right)=\sum _{k:\mathrm{Fin}\left(N\right)}(\mathrm{smul}\left(\mathrm{ComplexofReal}\left(p\left(k\right)\right),\mathrm{rankOne}\left(\mathbb{C},\mathrm{lpsingle}\left(2,\mathrm{val}\left(k\right),\mathrm{ComplexofReal}\left(1\right)\right),\mathrm{lpsingle}\left(2,\mathrm{val}\left(k\right),\mathrm{ComplexofReal}\left(1\right)\right)\right)\right))))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/Entropy.finiteDiagonal (✓ std3).

Citation. Alfred Wehrl (1978). General properties of entropy. DOI: 10.1103/RevModPhys.50.221. URL: https://doi.org/10.1103/RevModPhys.50.221.

Commentary.

The finite diagonal operator is the sum of p(k) times the occupation rank-one projector. Its definition allows arbitrary real entries; the entropy theorem supplies the bounds from zero to one.

Definition 1.2 (basisEntropy).

$$\forall T:\mathrm{ContinuousLinearMap}\left(\mathbb{C},\mathrm{lp}\left(\mathrm{Functionconst}\left(\mathbb{N},\mathbb{C}\right),2\right),\mathrm{lp}\left(\mathrm{Functionconst}\left(\mathbb{N},\mathbb{C}\right),2\right)\right),(\forall b:\mathrm{HilbertBasis}\left(\mathbb{N},\mathbb{C},\mathrm{lp}\left(\mathrm{Functionconst}\left(\mathbb{N},\mathbb{C}\right),2\right)\right),(\mathrm{basisEntropy}\left(T,b\right)=\sum _{n:\mathbb{N}}^{\prime }(\mathrm{ENNRealofReal}\left(\mathrm{negMulLog}\left(\mathrm{Re}\left(\mathrm{inner}\left(\mathbb{C},b\left(n\right),T\left(b\left(n\right)\right)\right)\right)\right)\right))))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/Entropy.basisEntropy (✓ std3).

Citation. Alfred Wehrl (1978). General properties of entropy. DOI: 10.1103/RevModPhys.50.221. URL: https://doi.org/10.1103/RevModPhys.50.221.

Commentary.

negMulLog(x)=-x log(x), with its continuous value zero at x=0. ENNReal.ofReal embeds a nonnegative real in the extended nonnegative reals; Complex.ofReal embeds a real scalar in Complex; on a density operator every diagonal probability lies in [0,1]. Natural logarithms give nats.

Definition 1.3 (vonNeumannEntropy).

$$\forall T:\mathrm{ContinuousLinearMap}\left(\mathbb{C},\mathrm{lp}\left(\mathrm{Functionconst}\left(\mathbb{N},\mathbb{C}\right),2\right),\mathrm{lp}\left(\mathrm{Functionconst}\left(\mathbb{N},\mathbb{C}\right),2\right)\right),(\mathrm{vonNeumannEntropy}\left(T\right)=\mathrm{iInf}\left((b:\mathrm{HilbertBasis}\left(\mathbb{N},\mathbb{C},\mathrm{lp}\left(\mathrm{Functionconst}\left(\mathbb{N},\mathbb{C}\right),2\right)\right))\mapsto (\mathrm{basisEntropy}\left(T,b\right))\right))$$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/Entropy.vonNeumannEntropy (✓ std3).

Citation. Alfred Wehrl (1978). General properties of entropy. DOI: 10.1103/RevModPhys.50.221. URL: https://doi.org/10.1103/RevModPhys.50.221.

Commentary.

The definition is the infimum over complete countable orthonormal bases of the diagonal Shannon entropy. Its equality with spectral von Neumann entropy for every density operator is literature-attested, following the eigenbasis and concavity characterization in Wehrl. The infinite-dimensional equivalence is not kernel-proved here. The kernel proves the finite diagonal spectral formula; the final refutation supplies the needed unitary invariance by transporting all Hilbert bases.

Theorem 1.4 (finiteDiagonal_entropy).

$$\forall N:\mathbb{N},(\forall p:\mathrm{Fin}\left(N\right)\to \mathbb{R},(((\forall j:\mathrm{Fin}\left(N\right),(0\le p\left(j\right)))\wedge (\forall j:\mathrm{Fin}\left(N\right),(p\left(j\right)\le 1)))\Rightarrow (\mathrm{vonNeumannEntropy}\left(\mathrm{finiteDiagonal}\left(N,p\right)\right)=\mathrm{ENNRealofReal}\left(\mathrm{shannonEntropy}\left(\mathrm{Fin}\left(N\right),p\right)\right))))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/FockAttenuator/Entropy.finiteDiagonal_entropy (✓ std3). ∎

Citation. Alfred Wehrl (1978). General properties of entropy. DOI: 10.1103/RevModPhys.50.221. URL: https://doi.org/10.1103/RevModPhys.50.221.

Commentary.

Concavity of -x log(x), the subprobability row bound and the Parseval column sums give the lower bound in every complete basis. The occupation basis attains it. shannonEntropy is the frozen finite Shannon functional, sum_j negMulLog(p_j). The result does not require the finite entries to sum to one.

References

• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/Entropy.basisEntropy
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/Entropy.finiteDiagonal
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/Entropy.finiteDiagonal_entropy
• Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/Entropy.vonNeumannEntropy
• Dependency: D5/S3/Entropy/MaxEntropy