Attenuator

Abstract

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

Corrected balanced Fock-two argument. The new analytic arguments in this narrative and the companion Entropy narrative are independently source-assessed mathematics pending formalization; the cited existing Lean declarations retain their own frozen scope and do not prove the new classification or countable entropy bridges. The parent problem is S(Phi(rho)) >= (3/2) log 2 for every density on completed Fock space, where Phi is the actual eta=1/2 channel with environment |2><2|. It remains open. More generally, Conjecture 1 of Van Herstraeten, Guha and Cerf, arXiv:2312.15623v2, Section IV, asks for coherent-state minimum output entropy for every eta and every number-state environment n, with possible additional minimizers. The rank-three result below is a restriction on the competing inputs, and the conditional determinant argument in Entropy leaves a universal premise unproved. Neither settles Conjecture 1 or the all-input partial-progress question in issue #17675. No finite input support, finite energy or finite entropy is assumed.

Physical coefficient correspondence. Write a completed-Fock vector as a=(a_k) in l2 and its Bargmann entire function as f(z)=sum_{k>=0} a_k z^k/sqrt(k!). The beamUnitary_fock convention sends f tensor |2> at eta=1/2 to F(z,w)=f((z+w)/sqrt(2)) (w-z)^2/(2 sqrt(2)). In normalized occupation coordinates, put N=i+j. Its coefficient matrix C_a has C_ij=0 for N<2 and C_ij=a_{N-2} sqrt(binomial(N,i)/2^N) ((i-j)^2-N)/sqrt(2N(N-1)) for N>=2. Indeed, expanding (w-z)^2(z+w)^{N-2}, the coefficient at z^i w^{N-i} is binomial(N-2,i)-2binomial(N-2,i-1)+binomial(N-2,i-2); division by binomial(N,i) gives ((N-2i)^2-N)/(N(N-1)), including the endpoint convention that out-of-range binomial coefficients vanish. Restoring occupation factorials gives the displayed C_ij. If I has binomial(N,1/2) law, E[((2I-N)^2-N)^2]=2N(N-1), so summing each anti-diagonal gives ||C_a||_HS^2=sum_k |a_k|^2. This is the exact completed-space isometry, not an assigned spectrum. With i retained, the pure output is C_a C_a^*, and its rank is the Schmidt or separation rank of F. The full square-root channel and its pure-input realization are the existing attenuatorOperator and pureAttenuatorOperator; their identification is also used inside PhaseCovariantAttenuatorCoherentRefutation.result.

Completed pure and density identification for the purity argument. At balance, the same orthogonal substitution turns V f into f(x)e2(y), so its isometry holds on the entire completed Fock space. A source DensityOperator is an arbitrary positive trace-class density: the sum of its full occupation diagonal is one, equivalently the positive square root has Hilbert-Schmidt norm one. The columns sqrt(rho)e_m satisfy sum_m |sqrt(rho)e_m><sqrt(rho)e_m|=rho in trace norm. Thus the source outputVector and attenuatorOperator are exactly the reduced beam-splitter map on rho tensor |2><2|, including off-diagonal and infinite-rank rho; pureOutputVector and pureAttenuatorOperator give its actual pure specialization C_a C_a^*. The completed-vector beam_displacement and partialTrace_pairDisplacement declarations, rather than only coherent_output_covariance, provide covariance for arbitrary inputs without a photon moment. The companion Entropy narrative uses this full identification for the two-copy compression, coherent equality and quantitative pure/density stability; these analytic consequences remain pending formalization.

Finite output rank forces an exponential polynomial. Rescaling the two complex variables preserves separation rank and replaces F by a nonzero scalar multiple of K(z,w)=(z-w)^2 f(z+w). For a finite-rank Hilbert-Schmidt coefficient operator, a singular-vector decomposition gives finitely many products of Bargmann entire functions; conversely a finite separation into entire factors bounds the analytic coefficient rank, which equals the operator rank when finite. Thus finite operator rank and finite analytic separation rank agree. Applying (partial_z-partial_w)^2 to K gives 8f(z+w). Differentiating a finite separated sum leaves a finite separated sum, so the ordinary Hankel kernel f(z+w) has finite rank. This operation takes place among entire functions and makes no assertion that differentiation is bounded on the Fock Hilbert space.

Let W be the span of all translates f(.+w), w in C. The finite-rank Hankel kernel puts W in a finite-dimensional space. Translation preserves W, and W is closed in the compact-open topology because it is finite dimensional. Difference quotients converge uniformly on compact sets to the derivative, so differentiation preserves W. If p is the characteristic polynomial of the linear map partial_z on W, Cayley-Hamilton gives p(partial_z)f=0. Factoring p over C and solving the constant-coefficient ODE gives f(z)=sum_alpha exp(alpha z) P_alpha(z), a finite sum with distinct alpha and nonzero polynomials P_alpha. Conversely each such function belongs to Bargmann Fock space, since polynomial growth times an exponential is square-integrable against the Gaussian, and its kernel K has finite separation rank by polynomial expansion. This proves the required entire-function statement directly. Engert, Finite dimensional translation invariant subspaces, Pacific J. Math. 32 (1970), 333-343, Theorem 1, printed p.340, DOI 10.2140/pjm.1970.32.333, treats a sigma-compact locally compact abelian group and measurable complex functions modulo almost-everywhere equality. Its group exponential-polynomial conclusion needs pointwise recovery and holomorphic specialization here. The direct ODE proof supplies precisely those analytic conditions. Primary text: https://msp.org/pjm/1970/32-2/pjm-v32-n2-p05-s.pdf. Engert also credits earlier continuous real-line work, including Anselone-Korevaar and Loewner; no priority inference is made.

Ranks add across distinct exponentials. For each alpha let m_alpha=deg P_alpha and use exp(alpha z) z^j, 0<=j<=m_alpha+2, as a basis in the first variable and the corresponding basis in the second. These exponential-polynomial spaces for different alpha are linearly independent: applying products of sufficiently high powers of partial_z-alpha isolates each summand, or equivalently uses the distinct generalized eigenspaces of differentiation. Since exp(alpha(z+w))=exp(alpha z)exp(alpha w), the finite coefficient matrix for K is block diagonal in these independent bases. Its rank is exactly the sum of the ranks of the nonzero polynomial blocks (z-w)^2 P_alpha(z+w). Lower coefficients and different exponentials therefore cannot cancel ranks between blocks.

All degrees in one polynomial block. Let P have nonzero leading coefficient and degree m, and set N=m+2. Apart from that leading coefficient, the coefficient on its top anti-diagonal z^i w^{N-i} is binomial(N,i) ((N-2i)^2-N)/(N(N-1)). At most two of the N+1 positions vanish, because the vanishing condition is quadratic in i. Choose all surviving row indices increasingly and their complementary column indices decreasingly. In the resulting square submatrix the diagonal is nonzero, and entries below it have total degree greater than N and vanish. The triangular minor is nonzero regardless of the lower coefficients of P. If m>=3 this gives rank at least N-1=m+1>=4. No exact rank formula for higher degrees is needed. For m=0 the three top anti-diagonal coefficients are nonzero and there are only three rows, so the rank is exactly three. For m=1 all four top anti-diagonal coefficients are nonzero and there are only four rows, so the rank is exactly four.

The quadratic block, including complex coefficients. Write P(z)=a0+a1 z+a2 z^2/sqrt(2), a2!=0. In the physical occupation basis the endpoint rows and columns give two nonzero pivots. Eliminating them leaves the 2 by 2 block [[-a0/sqrt(2),-a1/sqrt(8)],[-a1/sqrt(8),-a2/2]], hence rank C=2+rank of that block. It is never zero, and its determinant is a0 a2/(2 sqrt(2))-a1^2/8. Consequently it has rank one exactly when a1^2=2 sqrt(2) a0 a2, and otherwise rank two. This is precisely the zero-discriminant condition for P. Thus a quadratic double root gives rank three; a quadratic with distinct roots gives rank four. The argument is over C and does not assume real input coefficients.

Exhaustive pure-input classification. Every nonzero exponential block has rank at least three. Rank three therefore requires one exponential and a polynomial that is either constant or quadratic with a double root. For any nonzero completed-Fock pure input, rank Phi(|f><f|)=3 if and only if, up to a nonzero normalization factor, f(z)=exp(alpha z) or f(z)=exp(alpha z)(z-beta)^2. There is no nonzero pure input with output rank below three. A function outside the finite exponential-polynomial class has infinite output rank. These conclusions quantify over arbitrary completed vectors; the polynomial calculations are the consequence of finite output rank, not an imposed finite occupation cutoff.

Covariance and the shifted root. In the source Weyl convention D(gamma)f(z)=exp(-|gamma|^2/2+gamma z) f(z-conj(gamma)). Thus D(-alpha)[exp(alpha z)(z-beta)^2] is a nonzero constant times (z-(beta-conj(alpha)))^2. The invariant radial parameter after displacement is r=|beta-conj(alpha)|, not |beta|. The beam_displacement and partialTrace_pairDisplacement identities provide the completed-vector displacement transport; coherent_output_covariance is the coherent special case. For the number-state environment phase rotation is also covariant: replacing a_k by exp(ik theta)a_k changes C to exp(-2i theta) D_theta C D_theta^T, where D_theta is diagonal with entries exp(ij theta). Hence C C^* changes by unitary conjugation. This direct coefficient calculation supplies arbitrary-input phase covariance; it is not inferred from coherent_output_covariance. A phase can therefore put every noncoherent rank-three case in the form f_r(z)=(z+r)^2/sqrt(Z), r>=0, x=r^2, Z=x^2+4x+2, with Fock coefficients (x,2r,sqrt(2))/sqrt(Z). The source’s unitary entropy transport is already used inside PhaseCovariantAttenuatorCoherentRefutation.result.

Compression of the actual occupation matrix. Before division by sqrt(Z), row 0 couples to rows 2,3,4 with entries x/2, sqrt(6)r/2, sqrt(3)/2, respectively. The block on rows and columns {1,2} is -(1/sqrt(2)) [[x,r],[r,1]]. Rotate its rank-one direction onto (r,1)/sqrt(x+1); its nonzero entry is -s, s=(x+1)/sqrt(2). Row 0 then couples to this direction with u=x/(2sqrt(x+1)). Its remaining coupling vector has squared norm v^2=x^3/(4(x+1))+3x/2+3/4=P/(4(x+1)), P=x^3+6x^2+9x+3; rotate that vector onto one further axis. The only nonzero compression is B/sqrt(Z), with B=[[0,u,v],[u,-s,0],[v,0,0]]. These are orthogonal changes of basis in the physical coefficient matrix. In particular det B=s v^2 is nonzero. Its three real nonzero eigenvalues mu_i are the roots of mu^3+s mu^2-T mu-s v^2=0, T=u^2+v^2=(x^2+6x+3)/4. The three nonzero physical output eigenvalues are mu_i^2/Z. The Entropy narrative derives the exact symmetric coefficients, strict entropy bound, mixed-support extension and equality cases from this compression.

Source scope and literature correspondence. The model correspondence uses BeamSplitter.beamUnitary_fock, Attenuator’s square-root ensemble and pureAttenuatorOperator, and DisplacementCovariance’s completed-vector identities at source revision 1ecf52f8c59f714ae936b8cea08c578355c80946 (Lean 4.35.0, Mathlib 56a005855ea17e0b0958f73ec801ae140b0a1679). Van Herstraeten, Guha and Cerf, https://arxiv.org/html/2312.15623v2, equation (44), gives displacement covariance for arbitrary environments; Lemma 1 requires rotation/reflection symmetry, satisfied by |2><2|, and equation (45) defines the physical Fock attenuator. Its Conjecture 1 does not supply the classification above. Lupu-Gladstein, Hertz, Heshami and Goldberg, Entanglement, loss, and quantumness: When balanced beam splitters are best, https://arxiv.org/html/2411.03423v1, Theorems 7,9,11, addresses respectively vacuum-loss purity for pure inputs, finite-support G-concurrence with an infinite-product warning, and mixed-input convex-roof entanglement with vacuum environment. Mode exchange and that mixed extension do not replace vacuum by fixed |2><2| with arbitrary competing input. Existing frozen vacuum-loss, Wigner-majorization and mixed-environment Conjecture 2 results likewise do not close the present Fock-two problem. These are checks of exact hypotheses in the cited literature and a bounded source overlap check, not an exhaustive absence or priority claim.

Three-copy realization on the full completed domain. Let H be Bargmann-Fock space with orthonormal basis e_k(z)=z^k/sqrt(k!), and write V f(z,w)=f((z+w)/sqrt(2))(w-z)^2/(2sqrt(2)). The orthogonal substitution x=(z+w)/sqrt(2), y=(w-z)/sqrt(2) preserves the Gaussian norm, and y^2/sqrt(2) has norm one. Hence V is an isometry for every a in complex l2, with no mean-photon-number assumption. Define the orthogonal antisymmetrizer P_alt=(1/6)sum_{pi in S3} sign(pi)U_pi on three retained outputs and Q=(V tensor3)^(P_alt,A tensor I_B)(V tensor3). Then 0<=Q<=I and e3(C_a C_a^)=<a tensor3,Q(a tensor3)>. The factor 1/6 belongs to the antisymmetrizer; there is no extra factorial in this expectation or in the increasing-triple exterior basis. The physical question is nonnegativity of Q-I/32 on actual tensor cubes a tensor3. The stronger assertion of positivity on every symmetric three-copy vector fails, as shown in Entropy.

Center and relative coordinates, without a center cutoff. For the three input variables put t=(x1+x2+x3)/sqrt(3), u=(x1-x2)/sqrt(2), v=(x1+x2-2x3)/sqrt(6), c=t/sqrt(3), and r_i=x_i-c. Then sum_i r_i=0, h2=sum_i r_i^2=u^2+v^2, and h3=r1 r2 r3=(3u^2v-v^3)/(3sqrt(6)). Apply the same orthogonal change to the environment and both output triples. The three identical splitters separate into center and relative splitters. A retained-output permutation acts identically on its center, so its conjugation cancels the center splitter. Taking the environment expectation yields Q=I_center tensor q. The transformed environment |2,2,2> still has six photons; writing it as sum_{d=0}^6 |6-d>center tensor chi_d and tracing the center gives a positive trace-one relative density block diagonal in d. Relative photon conservation gives q=direct_sum{M>=0}q_M. All steps use bounded unitaries and projections on completed spaces. No differentiation operator on H is used here.

The invariant relative sectors and their physical components. Simultaneous copy permutations intertwine the splitters, fix the environment and preserve P_alt; consequently q_M preserves the S3-invariant relative subspace. The fundamental theorem of symmetric polynomials with sum r_i=0 identifies its polynomial algebra as C[h2,h3], since h2=-2e2(r) and h3=e3(r). An exact basis at degree M is {h2^p h3^j:2p+3j=M}. The invariant space is one-dimensional for M=0,2,3,4,5, absent for M=1, and of dimension at most 11 for M<64. These dimensions concern the invariant subspaces, not the full relative degree-M spaces. Define F_a(t,u,v)=product_{i=1}^3 f(c+r_i) and let F_{a,M} be its orthogonal relative-degree-M projection. It is the transformed physical tensor cube, so every component is invariant and sum_M ||F_{a,M}||^2=||a||^6. Every center coefficient is retained as a vector of the entire completed center space.

Exact same-function differential polynomials. Every prime in this paragraph denotes the ordinary complex derivative in the Bargmann argument c, and every occurrence of f or a derivative is evaluated at c. Define P3=(f^2 f’‘’-3f f’ f’‘+2(f’)^3)/2, P4=(f^2 f’‘’‘-4f f’ f’‘’+3f(f’‘)^2)/48, and P5=(f^2 f’‘’‘’-5f f’ f’‘’‘+2f f’’ f’‘’+8(f’)^2 f’‘’-6f’(f’‘)^2)/48. The full projected vectors are F_{a,3}=P3(t/sqrt(3))h3, F_{a,4}=P4(t/sqrt(3))h2^2, and F_{a,5}=P5(t/sqrt(3))h2h3. They obey the entire identity f(c)P5(c)=f(c)P4’(c)-3f’(c)P4(c). If the center coefficient is differentiated in t instead, P4’(c) is sqrt(3) times d[P4(t/sqrt(3))]/dt. Thus changing derivative variables changes that coefficient.

Derivation and behavior at zeros. The power sums of r_i are p2=h2, p3=3h3, p4=h2^2/2 and p5=5h2h3/2. On any disk where f is nonzero, choose a local g=log f and expand exp(sum_i g(c+r_i)). Its relative degrees three, four and five are f^3 g’‘’ h3/2, f^3(g’‘’‘/48+(g’‘)^2/8)h2^2, and f^3(g’‘’‘’/48+g’‘g’‘’/4)h2h3. Expanding the logarithmic derivatives gives exactly P3,P4,P5 above. Differentiating the expression for P4 gives P4’=3(f’/f)P4+P5. Multiplication by f yields the displayed polynomial identity. Since all final expressions are polynomial in entire derivatives, analytic continuation extends them across every zero; f identically zero is immediate. Direct differentiation of the polynomial P4 also verifies fP4’-3f’P4=fP5 without division. These formulas supply no global logarithm and require no zero-free hypothesis.

Weighted norms with exact Gaussian and factorial normalization. Define ||P||_3^2=(3/pi)integral_C |P(c)|^2 exp(-3|c|^2)d^2c. The change t=sqrt(3)c gives ||P(t/sqrt(3))||_center^2=||P||_3^2, and ||c^k||3^2=k!/3^k. Orthogonality of Bargmann monomials gives ||h3||^2=2!/6+3!/54=4/9; ||h2^2||^2=4!+4(2!2!)+4!=64; and, since h2h3=(u^4v+(2/3)u^2v^3-v^5/3)/sqrt(6), ||h2h3||^2=4+8/9+20/9=64/9. It follows that ||F{a,3}||^2=(4/9)||P3||3^2, ||F{a,4}||^2=64||P4||3^2 and ||F{a,5}||^2=(64/9)||P5||_3^2. The center Gaussian is part of every norm; evaluating only at center vacuum would change the assertion.

Why the projected identities and weighted integrability hold for every complex l2 input. Cauchy-Schwarz gives |f(z)|<=||a||exp(|z|^2/2), hence f is entire. The three-mode orthogonal coordinate change is unitary on completed Fock space and maps a tensor3 to F_a, of squared norm ||a||^6. For truncations a_L, their tensor cubes converge in Hilbert norm, while the corresponding f_L and every fixed derivative converge uniformly on compact disks by reproducing estimates and Cauchy’s formula. The projected polynomial identities hold for f_L. Orthogonal projection is bounded; projected Hilbert convergence and continuous center evaluation therefore identify the limiting coefficients with Pj(f)(t/sqrt(3)). The degree-three, four and five invariant spaces are exactly the one-dimensional lines already identified, so these are the whole projected vectors. Their norms are finite because they are bounded projections of F_a. This proves the weighted integrability of the displayed derivative combinations without assuming that differentiation is bounded on H or that the individual derivatives belong to H. Infinite support, arbitrary phases, unbounded mean photon number, and the full center coordinate remain in scope.

Evidence and literature boundary for this package. The same-function identities, relative-sector estimates and physical perturbation arguments here and in Entropy are independently source-assessed analytic mathematics pending formalization. The analytic evidence includes independent source assessment of the pinned owner definitions and their model correspondence; source reading is not kernel verification. No successful Pro source audit of those owners is part of this evidence. Further literature checks preserve exact settings: arXiv:1301.5229, Section III and equations (11)-(14), has a vacuum second input; arXiv:2411.03423v1, Lemma 6 and Theorem 7, uses two vacuum environment modes in its two-copy overlap mechanism. Neither supplies this three-copy two-photon estimate. The coherent-transform convex-functional theorem in arXiv:2210.14798, Theorem 1, does not identify its phase-space integral with 2p3-3s p2+(13/16)s^3. No such missing bridge is assumed. These bounded checks make no worldwide novelty or priority claim.

Attainment and variation for the balanced two-photon channel (A1–A6). The coefficient localization and weak-profile splitting proved here feed the attainment and variational argument in the Entropy owner. Throughout H=ℓ²(ℕ;ℂ), with Bargmann basis eₙ(z)=zⁿ/√(n!), and no support, rank, energy or photon-moment restriction is imposed. These are readable analytic proofs, with the physical/library identifications made explicit; the new attainment statements and the cited D/P/T analytic dependencies still require their exact native realization. Existing Lean declarations and their Describes retain their own narrower scopes.

The physical map is V f(z,w)=f((z+w)/√2)(w−z)²/(2√2), with z retained and w discarded. It is the balanced specialization of BeamSplitter.rotate, beamSplitter, fockExpansion and beamUnitary_fock with environment e₂: the orthogonal coordinates x=(z+w)/√2, y=(w−z)/√2 turn it into f(x)e₂(y). Thus V is an isometry on the completed space. Write Cₐ for its occupation coefficient operator, (Cₐ)ᵢⱼ=cᵢⱼaᵢ₊ⱼ₋₂. For N=i+j≥2, cᵢⱼ=√(binom(N,i)/2ᴺ)·((i−j)²−N)/√(2N(N−1)); set it to zero when N<2 or an index is invalid, and take negative input indices as zero. Indeed expanding (z+w)ᴺ⁻²(w−z)² gives binom(N,i)((N−2i)²−N)/(N(N−1)); the occupation factorials give exactly the displayed coefficient, including its sign. In particular Cₐ is symmetric. The orthogonal anti-diagonals and isometry give ‖Cₐ‖₂=‖a‖ and σₐ=CₐCₐ*=Φ(|a⟩⟨a|), positive trace class with Tr σₐ=‖a‖². Here ‖·‖₂ and ‖·‖₁ denote Hilbert–Schmidt and trace norms; Tr is the analytic trace-class trace.

This output is the actual pureAttenuatorOperator, not a chosen spectrum: pureOutputVector supplies precisely its discarded-mode columns, whose rank-one mixture is CₐCₐ*. For a general source DensityOperator, positivity and the full occupation diagonal sum one imply a normal trace-class density. The columns of its positive square root give its rank-one sum in trace norm, and outputVector/attenuatorOperator apply the same channel to this sum. The normal channel is Φ(T)=Tr_w(VTV*), with its actual bounded positive unital adjoint Φ*(K)=V*(K⊗Id)V. For all u,v∈H and bounded K, Tr[KΦ(|u⟩⟨v|)]=⟨v,Φ*(K)u⟩ (inner products are conjugate-linear in the first variable). These completed vectorization, trace-class and trace-pairing identifications are analytic joins to the source definitions; they are explicit outstanding native bridges, rather than consequences of merely displaying those definitions.

A1. Compactness of both fixed finite occupation restrictions. Let P_L project onto occupations 0,…,L, where L stays fixed. Orthogonal anti-diagonals give ‖C_bP_L‖₂²=Σₖ≥₀w_L(k)|bₖ|², where w_L(k)=Σ₀≤ⱼ≤min(L,k+2)|cₖ₊₂₋ⱼ,ⱼ|² and 0≤w_L(k)≤1. With N=k+2≥2 and 0≤j≤N, 0≤(N−2j)²≤N² implies |(N−2j)²−N|≤N(N−1). Hence |c_N−j,j|²≤binom(N,j)N(N−1)/(2·2ᴺ)≤Nʲ⁺²/(2j!2ᴺ). Summing gives the explicit bound w_L(k)≤(1/8)(Σⱼ₌₀ᴸ1/j!)(k+2)ᴸ⁺²2⁻ᵏ→0. The bound depends on L; no uniformity as L→∞ is used.

Let Q_K truncate input coordinates at K. The maps b↦C_(Q_Kb)P_L have finite-dimensional range, and the squared norm of the omitted map is at most supₖ>K w_L(k)→0. Thus b↦C_bP_L is an operator-norm limit of finite-rank maps from H to S₂, and is compact. Symmetry cᵢⱼ=cⱼᵢ gives the identical weighted estimate and approximation for b↦P_LC_b. Both maps therefore take every bounded weakly null sequence to zero in S₂. The full map b↦C_b is an isometry on an infinite-dimensional space and is not compact. Neither a varying L nor a discarded infinite tail occurs in this argument.

A2. Trace-class decoupling of a weak profile. Fix any a∈H and any bounded sequence rₙ⇀0. First suppose a is supported in 0,…,M, so Cₐ is supported in rows and columns 0,…,M+2. For L=M+2, Schatten Hölder and A1 give ‖CₐC_rₙ*‖₁=‖Cₐ(C_rₙP_L)‖₁≤‖Cₐ‖₂‖C_rₙP_L‖₂→0. For a general a, choose finite-support b approaching a. The error is at most ‖C_(a−b)C_rₙ‖₁≤‖a−b‖‖rₙ‖, uniformly in n. Taking first n→∞ and then b→a proves the same conclusion. Its adjoint C_rₙCₐ* has the same trace norm.

The remainder outputs vanish against every compact output test K. For finite occupation compression, |Tr(P_LKP_Lσ_rₙ)|≤‖K‖Tr(P_Lσ_rₙ)=‖K‖‖P_LC_rₙ‖₂²→0. For arbitrary compact K, ‖K−P_LKP_L‖→0, while ‖σ_rₙ‖₁=‖rₙ‖² is uniformly bounded. Approximation therefore gives Tr(Kσ_rₙ)→0. K need not be positive or finite rank. This is convergence against compact operators; the remainder outputs need not tend to zero in trace norm.

Set A=σₐ and Rₙ=σ_rₙ. The exact quadratic output expansion reads σ_(a+rₙ)=A+Rₙ+εₙ, with εₙ=CₐC_rₙ*+C_rₙCₐ*→0 in S₁. On bounded trace-norm sets, telescoping products give |Tr(Tʲ−Sʲ)|≤jMʲ⁻¹‖T−S‖₁ for j=2,3, when the operator norms are at most M. Every product has a trace-class factor and otherwise bounded factors. It remains to expand A+Rₙ without assuming commutativity. The quadratic cross traces are Tr(ARₙ)+Tr(RₙA)=2Tr(ARₙ)→0. The six cubic words are A²Rₙ, ARₙA, RₙA² and ARₙ², RₙARₙ, Rₙ²A; cyclicity gives respectively 3Tr(A²Rₙ) and 3Tr(ARₙ²). The compact tests with A,A² kill the first mixed traces. Positivity and Rₙ²≤‖Rₙ‖Rₙ give 0≤Tr(ARₙ²)≤‖Rₙ‖Tr(ARₙ)→0. Thus pⱼ(a+rₙ)=pⱼ(a)+pⱼ(rₙ)+o(1), j=2,3, where pⱼ(b)=Tr σ_bʲ. All infinite rows and columns remain present.

For unnormalized b write s(b)=‖b‖², e₂(σ_b)=(s(b)²−p₂(b))/2 and E(b)=e₃(σ_b)=(s(b)³−3s(b)p₂(b)+2p₃(b))/6. The elementary symmetric sums converge absolutely for positive trace-class operators (e₃≤s³/6). Weak convergence gives s(a+rₙ)=s(a)+s(rₙ)+o(1). Substitution of the moment splitting into these Newton identities yields E(a+rₙ)=E(a)+E(rₙ)+s(a)e₂(σ_rₙ)+s(rₙ)e₂(σₐ)+o(1). Both unnormalized cross masses survive, including when a or a remainder is zero. This is the physical splitting used below; neither cross term can be dropped.

The trace-ideal estimates have existing supplier homes in D5/S3/Quantum/Analysis/TraceClass: GeneralProduct.isTraceClass_mul_of_isHilbertSchmidt, IdealNorm.traceNorm_mul_le_of_isHilbertSchmidt and traceNorm_mul_mul_le, TraceAlgebra.trace_mul_cycle, Pairing.tracePairingContinuousLinearMap, and Compact.isCompactOperator_of_isTraceClass. Their attributed physlib source is b9043cc548ef6d63a28454cf3a57fb12a0c2e142 (Tom Ole Diem, Apache 2.0). They supply norm, product, trace and compactness tools, rather than the new physical coefficient or splitting theorems. Pinned Mathlib supplies compact-map composition and operator-norm closure, and real bounded-bilinear differentiation. Future native work must reuse exact matching statements and establish the actual channel bridges; no duplicate binding theorem is introduced here. Conditional completed-channel structural package R1-R3. All statements in this addendum are analytic prose pending native formalization. They use H=l2(N;C), e_n(z)=z^n/sqrt(n!), the inner product conjugate-linear in its first argument, and exactly the balanced Fock-two channel Phi(T)=Tr_w U(T tensor |e2><e2|)U^, with (U(f tensor e))(z,w)=f((z+w)/sqrt(2))e((w-z)/sqrt(2)). Thus V f=U(f tensor e2)=f((z+w)/sqrt(2))(w-z)^2/(2sqrt(2)), sigma_a=Phi(|a><a|)=C_a C_a^, and Phi^(K)=V^(K tensor Id)V. The bounded normal-channel extension to all complex trace-class T and this actual trace-dual adjoint are the intended interfaces, not a newly assigned output spectrum. Write E(b)=e3(sigma_b), I=inf_{||b||=1}E(b), q=Tr(sigma_a^2), p3=Tr(sigma_a^3), mu=q-p3, B=Phi^*(sigma_a-sigma_a^2), and A=(1/2)Id-sigma_a. Assume I<1/32 and an actual unit global minimizer a. No initial energy, support, output-rank, coefficient-phase or moment hypothesis is imposed.

Exact attainment/variational prerequisites for the conditional argument. A1 is compactness, for each fixed finite occupation projection P_L, of b -> C_b P_L and b -> P_L C_b from H to S2; the full map b -> C_b is an isometry, not a compact map. A2 says that, for every fixed b and every bounded weakly-null r_j, ||C_b C_rj^*||_1 ->0 and Tr(K sigma_rj)->0 for every compact output K; it also supplies the unnormalized quadratic/cubic moment splitting. A3-A4 give 25/864<=I<=1/32 and, for every minimizing sequence, a strongly convergent unit-minimizing subsequence after maximizing coherent displacements and phases. In that representative a_0=sqrt(m(a))>0 and a_1=0, where m(b)=sup_alpha |<coherent(alpha),b>|^2. This existence and gauge package is a separate analytic prerequisite: the conditional argument here does not supply its full proof, and the existing Lean declarations do not certify it. R1, the general spectral-range part of R2 and R3 do not require that centered gauge.

A5-A6 in the exact physical domain. A5 gives real Frechet smoothness of the bounded trace-polynomial E, the actual trace-dual Phi^, compactness of Phi^(K) for every compact output K, and Ba=mu a. At unit a, DE(a)[h]=2 Re<h,[e2(sigma_a)Id-B]a>; at an unnormalized input the exact formula is DE(a)[h]=2 Re<h,[e2(sigma_a)Id-||a||^2 Phi^(sigma_a)+Phi^(sigma_a^2)]a>, so the unit formula must not be used without its normalization. A6 states, for every complex h with <a,h>=0, X_h=Phi(|h><a|+|a><h|) and <h,Bh>+Tr(A X_h^2)<=mu||h||^2. For the same negative minimizer, the earlier physical purity and spectral arguments give q<=3/8, ||sigma_a||<1/2, 0<=B<=mu Id and B positive compact. In particular epsilon=1/2-||sigma_a||>0 and A>=epsilon Id. These are conditional analytic premises from the entire A1-A6 package and its D/P/T dependencies, pending their native joins. Neither an abstract compact operator nor purity alone supplies these same-input hypotheses. All traces below are analytic S1 traces, never the total algebraic LinearMap.trace outside finite dimension.

R1: the actual Weyl multiplier on every complex trace-class input. Let D(xi)=exp(xi c^-conj(xi)c) denote the bounded strongly continuous Weyl unitary in the source convention, and chi_T(xi)=Tr(T D(xi)). This notation does not differentiate an unbounded exponential. The completed splitter identity gives U^(D(xi) tensor Id)U=D(xi/sqrt(2)) tensor D(-xi/sqrt(2)). Pairing this bounded identity with T tensor |e2><e2|, and using the defining partial trace, gives chi_Phi(T)(xi)=chi_T(xi/sqrt(2))<e2,D(-xi/sqrt(2))e2>. It holds for arbitrary, possibly non-self-adjoint T in S1, with no photon moments. The environmental sign follows from the actual repository rotation.

Continuity across the circles and Weyl uniqueness. For finite-rank F, strong continuity of D and its matrix coefficients makes chi_F continuous. Finite-rank trace-norm approximation gives |Tr((T-F)D(xi))|<=||T-F||_1 uniformly in xi, hence chi_T is continuous for every complex T in S1. If Phi(T)=0, the multiplier identity makes chi_T(xi/sqrt(2)) zero off the two circles. Scaling and continuity give chi_T=0 everywhere. Fourier-Weyl Plancherel, with measure d^2xi/pi in this complex displacement normalization, is injective on S2; S1 is contained in S2. Applying it to this same T proves T=0. Thus the actual channel is injective on all S1, including non-self-adjoint perturbations. This use of Weyl uniqueness supplies no lower bound for an inverse channel norm.

R1: simplicity needs both complex directions. Suppose h is complex-perpendicular to a and Bh=mu h. A6 implies Tr(A X_h^2)<=0. Since X_h=X_h^* is S1 and A>=epsilon Id, trace-ideal cyclicity gives Tr(A X_h^2)=||A^(1/2)X_h||_2^2>=epsilon||X_h||_2^2, so X_h=0. Apply A6 separately to ih, which is again perpendicular and a mu-eigenvector, to obtain X_ih=0. For Y=Phi(|h><a|), complex linearity and adjoint preservation give X_h=Y+Y^* and X_ih=iY-iY^*. Both equations force Y=0. Channel injectivity gives |h><a|=0; applying it to the unit a gives h=0. Every mu-eigenvector of self-adjoint B splits into a multiple of a and such an h. Hence ker(B-mu Id)=C a. Compactness alone would not prove this simplicity.

R1: a gap for this fixed self-consistent operator. B preserves the complex perpendicular a^perp. Its positive compact restriction has norm strictly below mu: if the norm equalled the nonzero mu, compact self-adjoint spectral theory would give a further mu-eigenvector in a^perp, contradicting simplicity. Thus delta_a=mu-||B restricted to a^perp||>0 and <h,Bh><=(mu-delta_a)||h||^2 there. Newton gives 6I=1-q-2mu. The strict inequality I<1/32 implies mu>13/32-q/2, and q<=3/8 implies mu>7/32. There is no numerical, input-uniform or all-minimizer uniform delta_a. Simplicity concerns the B generated by this a; a different physical input generates a different B, so no uniqueness of minimizers follows.

R2: auxiliary environmental transfer for arbitrary bounded output K. For any environmental vector e put J_e b=U(b tensor e) and Phi_e^(K)=J_e^(K tensor Id)J_e. The mixed map (e,f) -> J_e^*(K tensor Id)J_f is bounded sesquilinear, with norm at most ||K||||e||||f|| because ||J_e||=||e||. After realification this is a bounded real-bilinear operation. No positivity, compactness, smooth symbol, finite rank or moment assumption on K is needed. The target channel remains Phi=Phi_e2 throughout; the other environments are auxiliary terms in an identity.

Repository-sign displacement transfer. The source rotation sends displacement labels (alpha,beta) to ((alpha-beta)/sqrt(2),(alpha+beta)/sqrt(2)). A signal displacement (alpha,0) gives output labels (alpha/sqrt(2),alpha/sqrt(2)); an environment displacement (0,-alpha) gives (alpha/sqrt(2),-alpha/sqrt(2)). Their retained labels agree and partial trace removes the differing discarded displacements. Thus Phi_e(D(alpha)T D(alpha)^)=Phi_{D(-alpha)e}(T)=D(alpha/sqrt(2))Phi_e(T)D(alpha/sqrt(2))^ for every T in S1. Rank-one identities extend by polarization and trace-norm continuity. Trace duality gives D(alpha)^Phi_e^(K)D(alpha)=Phi_{D(-alpha)e}^*(K) for every bounded complex K. No Weyl phase survives conjugation. The attenuator paper uses the opposite environmental sign in its splitter convention; even e2 parity does not permit silently changing the sign of a displaced auxiliary environment.

R2: real operator-norm C-infinity from a known finite Fock vector. For e=e2, D(-alpha)e2(z)=exp(-|alpha|^2/2-alpha z)(z+conj(alpha))^2/sqrt(2). Every real derivative is a polynomial in z, alpha and conj(alpha) times the same exponential. On |alpha|<=R, each finite derivative order has squared Bargmann integrand bounded by C(1+|z|)^M exp(-|z|^2+2R|z|), which is integrable. Norm differentiation under the integral proves that alpha -> D(-alpha)e2 is C-infinity from R^2 into H. The identical argument works for every finite Fock polynomial. Composing with the bounded sesquilinear map proves that alpha -> D(alpha)^Phi^(K)D(alpha) is C-infinity in operator norm for every bounded K. All smoothness here is real smoothness, not holomorphy, and D(alpha) itself is never differentiated in operator norm.

R2: isolate the spectral range before differentiating any unknown eigenvector. Now, only for this spectral step, assume K compact self-adjoint and let L=Phi^*(K). A5 makes L compact self-adjoint. A nonzero eigenvalue lambda has an isolated finite-rank spectral projection P. Choose a resolvent contour Gamma enclosing lambda and no other spectrum. L_alpha=D(alpha)^*L D(alpha) is norm-C-infinity by the preceding argument. Inversion is C-infinity on the invertible elements of the complete operator algebra; for R=(z Id-L_alpha)^(-1), its first derivative is R(dL_alpha)R and higher derivatives are finite products with uniformly bounded resolvents on compact contour and parameter sets. Consequently P_alpha=(2pi i)^(-1) integral_Gamma (z Id-L_alpha)^(-1)dz is norm-C-infinity. Unitary conjugacy gives P_alpha=D(-alpha)P D(alpha). No regularity of a lambda-eigenvector has been assumed in obtaining this projection.

Finite smooth seeds give the whole eigenspace, without simplicity or a gauge assumption. Finite Fock vectors form a dense linear subspace. Its image under P is a dense linear subspace of finite-dimensional Ran P, so equals Ran P. Choose finitely many such vectors v_j whose Pv_j span Ran P. The exact identity D(-alpha)Pv_j=P_alpha D(-alpha)v_j expresses the left orbit using two already smooth factors. Every fixed linear combination, hence every vector in the lambda-eigenspace, has a norm-C-infinity displacement orbit. These finite seed vectors do not restrict the support of the eigenvector. R1 simplicity is needed only for the optional explicit centered formula: with P=|a><a| and a_0=sqrt(m(a))>0 real, Pe0=sqrt(m(a))a and D(-alpha)a=m(a)^(-1/2)P_alpha D(-alpha)e0. That last formula must not be asserted for an arbitrary uncentered phase choice.

The zero-eigenvalue boundary and the actual minimizer. Lambda=0 is excluded: its kernel need not be an isolated finite-dimensional spectral range. Compactness and self-adjointness of K enter only the spectral argument, while arbitrary-bounded-K norm smoothness holds without them. In particular Phi^*(Id)=Id, so the argument does not claim that all bounded K have compact images. For the same hypothetical minimizer take K=sigma_a-sigma_a^2, compact self-adjoint, and lambda=mu>7/32. Its eigenvector a therefore has a norm-C-infinity displacement orbit, without any initial photon-domain assumption.

Exact pure Wirtinger derivative in the occupation basis. This coordinate and domain argument applies to every nonzero-eigenvalue eigenvector just obtained, including the minimizer; denote it by a. Set F(alpha)=D(-alpha)a, alpha=x+iy, and partial_alpha=(partial_x-i partial_y)/2. Its norm derivatives now exist, so bounded coordinate evaluation commutes with them. In the conjugate-linear-first convention, F(alpha)n=<D(alpha)e_n,a>; transferring differentiation to that first slot changes partial_alpha into partial_conj(alpha). Differentiating the known finite-Fock orbit yields (partial_alpha^k F(0))n=(-1)^k sqrt(n!/(n-k)!)a(n-k) for n>=k, and zero for n<k. Equivalently the pure alpha derivative at zero of exp(-|alpha|^2/2-alpha z)f(z+conj(alpha)) is (-z)^k f(z). There is no conjugation of a(n-k) and no missing factor two. Mixed Wirtinger derivatives have additional terms and are not being identified with this pure derivative. The computation identifies an already existing norm derivative; it does not apply an unbounded creation operator to an arbitrary starting vector.

Parseval and every number-operator domain. Parseval gives the exact equality ||partial_alpha^k F(0)||^2=sum_{j>=0}((j+k)!/j!)|a_j|^2=0. For the number operator N e_j=j e_j and any integer r>=0, take k=2r and use (j+1)^(2r)<=product_{ell=1}^{2r}(j+ell); k=0 handles r=0. Therefore sum_j(j+1)^(2r)|a_j|^2<infinity, exactly a in Dom((N+1)^r). Arbitrarily large r give rapid occupation coefficients. In the standard Hermite identification with the Schrodinger oscillator, these are Schwartz vectors: every word in creation and annihilation has square-summable coefficients; thus all polynomially weighted derivatives are L2, and Sobolev estimates supply all Schwartz seminorms. This Hermite/Schwartz identification is an analytic bridge, still to be supplied natively if a formal statement names SchwartzMap. No exponential decay, analytic-vector property, finite support, finite output rank, uniform moment bound or tail deletion is concluded.

Primary source and prior-method scope for R1-R2. The actual displacement and splitter conventions are in BeamSplitter and DisplacementCovariance at immutable published revision bc0d5339476df8b41d58d7cde040a82266a9f416, including beamUnitary_fock, beam_displacement and partialTrace_pairDisplacement on the full completion. Kiukas, Lahti, Schultz and Werner, Characterization of informational completeness for covariant phase space observables, https://arxiv.org/html/1204.3188v1, Section 2 and Proposition 4, supply classical Fourier-Weyl Plancherel and the continuous-transform/dense-complement mechanism, including complex trace-class operators. Their phase-space observable is not Phi: the actual channel multiplier is derived above. Bastianoni, Cordero and Nicola, Decay and Smoothness for Eigenfunctions of Localization Operators, https://arxiv.org/html/1902.03413v2, Theorem 3.10 and Remark 3.11, prove Schwartz eigenfunction regularity under Schwartz-window and weighted modulation-symbol hypotheses. Those symbol hypotheses have not been established for B, so that theorem is not imported; the direct environmental transfer and finite-seed spectral argument supply the needed regularity here. No novelty is claimed for harmonic analysis or spectral smoothing methods.

Positive overlap inherited from the entire prerequisite packages. Zixuan He, The energy cost of optical noise, version 1.0, https://zenodo.org/records/23629201, DOI 10.5281/zenodo.23629201, Theorem 8 and Appendix F already establish all-normal balanced Fock purity, the bounded copy kernel and coherent equality for n>=2. Appendix K.5 gives coherent-orbit compactness when difference-vacuum overlap tends to one; K.6 contact-family assumptions do not classify every pure-e2 e3 minimizer. Ramos, Eigenfunctions, Free Boundaries, and Time-Frequency Localization, https://arxiv.org/html/2607.21590v2, Section 7, gives Weyl profiles and concentration-compactness for a quadratic Gaussian localization functional with a set-measure constraint, not this degree-six physical functional. Frank, Nicola and Tilli, The generalized Wehrl entropy bound in quantitative form, https://arxiv.org/html/2307.14089v3, Theorem 3 and Remarks 4, compare convex Husimi integrals for positive trace-one operators; the P-package uses its stated normalization, but no equality with the physical cubic cycle term or exclusion of our minimizer follows. These are positive prior overlaps with precise applicability limits, not claims of worldwide novelty or absence.

Channel source and unresolved scope. Van Herstraeten, Guha and Cerf, https://arxiv.org/html/2312.15623v2, Section IV, equations (44)-(45), give the actual Fock channel and arbitrary-environment displacement covariance, with the splitter-sign difference just stated. Their Conjecture 1 remains the all-n/all-eta minimum-output-entropy question in that version. R1-R3 are conditional analytic consequences for the same hypothetical negative minimizer. They do not prove E>=1/32, unrestricted balanced-Fock-two entropy, the countable spectral/ENNReal bridge or Conjecture 1; they construct no negative physical input and classify no minimizer. The companion Entropy narrative retains the whole real-Hessian proof and every same-function center/relative-sector obligation. All infinite coefficients and all complex directions remain in scope.

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.

T1: the complete complex quadratic family. Keep the physical map and increasing-triple exterior convention above. For arbitrary A,B,C in C, put xi=A e0+B e1+C e2, s=|A|^2+|B|^2+|C|^2, R=|B|^2+|C|^2 and G(xi)=e3(C_xi C_xi^)-s^3/32. Expanding the actual isometry on f(z)=A+Bz+Cz^2/sqrt(2) gives its full nonzero occupation block C_xi=[[0,0,A/2,sqrt(6)B/4,sqrt(6)C/4],[0,-A/sqrt(2),-B/(2sqrt(2)),0,0],[A/2,-B/(2sqrt(2)),-C/2,0,0],[sqrt(6)B/4,0,0,0,0],[sqrt(6)C/4,0,0,0,0]]. Every other row and column vanishes. The three occupied anti-diagonals contribute |A|^2, |B|^2 and |C|^2 to the squared Hilbert-Schmidt norm, so Tr(C_xi C_xi^)=s. In particular G(lambda xi)=|lambda|^6 G(xi); the subtraction is ||xi||^6/32 even before normalization. These statements include all phases and zero coefficients.

Complete third-minor calculation by unitary compression. Set x=A/2, y=-A/sqrt(2), z=-B/(2sqrt(2)), w=-C/2, u=sqrt(6)B/4, v=sqrt(6)C/4 and Delta=yw-z^2. If R>0, a unitary U on coordinates 3,4 sends (u,v)^T to (r,0)^T, r=sqrt(3R/8). The unitary congruence diag(I3,U) C_xi diag(I3,U)^T preserves singular values: its right transpose times its complex conjugate is the identity. Its only nonzero block is M=[[0,0,x,r],[0,y,z,0],[x,z,w,0],[r,0,0,0]]. Consequently every minor containing the remaining zero coordinate vanishes, and the full exterior Hilbert-Schmidt norm of the original five-by-five matrix equals that of M. The signed cofactor matrix of M, in index order 0,1,2,3, is [[0,0,0,-r Delta],[0,-r^2 w,r^2 z,-r x z],[0,r^2 z,-r^2 y,r x y],[-r Delta,-r x z,r x y,-x^2 y]]. This lists all sixteen complementary third minors: cofactor (i,j) is (-1)^(i+j) times the determinant with row i and column j omitted, in increasing order. Thus the seven displayed nonzero monomial types -r Delta,-r^2 w,r^2 z,-r x z,-r^2 y,r x y,-x^2 y have multiplicities 2,1,2,2,1,2,1; the other five positions vanish. There is no factorial multiplier. Cauchy-Binet therefore gives e3(C_xi C_xi^*)=2r^2|Delta|^2+r^4(|y|^2+2|z|^2+|w|^2)+2r^2|x|^2(|y|^2+|z|^2)+|x|^4|y|^2. This accounts for the entire original hundred-minor sum by an exterior-unitary equivalence, including every multiplicity and cofactor sign, rather than checking selected minors.

The factorization and every degenerate fiber. Substitute Delta=(2sqrt(2)AC-B^2)/8 and r^2=3R/8 into the complete minor sum. After subtracting s^3/32 it gives 256G(xi)=R^3+3R|B^2-2sqrt(2)AC|^2-6|A|^2R|C|^2. Expanding the bracket R^2+3|B^2-2sqrt(2)AC|^2-6|A|^2|C|^2 yields 4|B|^4+2|B|^2|C|^2+|C|^4+18|A|^2|C|^2-12sqrt(2)Re(B^2 conjugate(AC)). The same expansion is 2|sqrt(2)B^2-3AC|^2+2|BC|^2+|C|^4. Hence the exact identity is 256G(xi)=R(2|sqrt(2)B^2-3AC|^2+2|BC|^2+|C|^4). If R>0, vanishing would force C=0 from |C|^4, then B=0 from the square, a contradiction. If R=0, B=C=0 and the original matrix directly has e3=|A|^6/32; this includes A=0 and uses no choice of coupling direction or division by zero. Thus G>=0 with equality exactly B=C=0. For example e2 has physical spectrum (3/8,3/8,1/4), so e3=9/256 and G=1/256, consistent with the complete degree-six identity.

T2: the exact completed pure rank-through-five characterization. For every nonzero a in complex l2 with Bargmann function f, rank(C_a C_a^*)<=5 if and only if f(z)=exp(alpha z)P(z) for some alpha in C and a nonzero polynomial P of degree at most two. Reuse the entire-function proof in ‘Finite output rank forces an exponential polynomial’ and the following translation/Cayley-Hamilton paragraph: finite operator rank equals finite separation rank, (partial_z-partial_w)^2[(z-w)^2 f(z+w)]=8f(z+w), and the finite-dimensional compact-open translation space is derivative invariant. This supplies every completed-vector hypothesis, without bounded differentiation on Fock space. Reuse ‘Ranks add across distinct exponentials’ and ‘All degrees in one polynomial block’ for the independent exponential blocks and the nonzero triangular minor, regardless of lower coefficients. Every nonzero block has rank at least three, including degrees zero, one and two as computed above. Two distinct exponential blocks already have rank at least six. For a single block of degree m>=5 the top anti-diagonal has m+3 positions and at most two zeros, hence rank>=m+1>=6. The only remaining excluded degrees are m=3 and m=4: N=m+2 is respectively 5 or 6, and the equation (N-2i)^2=N has no integer solution. All six or seven top entries survive, giving rank exactly six or seven. Thus rank<=5 forces precisely one exponential block of degree<=2. Engert’s measurable-function theorem is classical context for the already supplied direct entire-function argument; it is not imported with an unstated holomorphic or pointwise hypothesis.

Converse, exact displacement, ranks and equality. In the source convention D(gamma)f(z)=exp(-|gamma|^2/2+gamma z)f(z-conj(gamma)), so D(-alpha)[exp(alpha z)P(z)]=exp(|alpha|^2/2)P(z+conj(alpha)). Both the plus conjugate shift and the norm prefactor are essential. The completed identities beam_displacement and partialTrace_pairDisplacement conjugate the actual output by D(-alpha/sqrt(2)); they preserve its rank, e3, input norm and G. Thus the converse follows from the T1 matrix, which has rank at most four. More exactly, when R=0 a nonzero constant has rank three. When R>0 the endpoint pivot gives rank M=2+rank([[y,z],[z,w]]); its Schur correction to this middle block is zero. This middle block is nonzero. If C=0 and B!=0 its determinant is -B^2/8!=0, giving rank four. If C!=0, the rank is three exactly when B^2=2sqrt(2)AC, otherwise four. These include all double-root quadratics and all complex degeneracies. Therefore every nonzero pure output of rank<=5 has rank three or four, and no pure output has rank five. Applying the homogeneous T1 identity after displacement gives G(a)>=0 throughout this class, with equality exactly for nonzero scalar coherent vectors. In particular noncoherent rank-three inputs also have strict G>0. The original input exp(alpha z)P(z) generally has infinite Fock support; polynomial support is obtained by an exact unitary displacement forced by the rank condition, not by an input cutoff.

An interior physical example for the additional exclusion. The normalized input a=(8e0+e2)/sqrt(65) has output rank four, q=Tr(sigma^2)=50443/135200, largest eigenvalue 32/65, coherent overlap maximum m=64/65, and G=1153/(25665^3)>0. These values follow from the actual T1 matrix. Before normalization its isolated coefficient eigenvalue is -4sqrt(2); the remaining nonzero real symmetric block is N=[[0,4,sqrt(6)/4],[4,-1/2,0],[sqrt(6)/4,0,0]], whose absolute row sums are at most 4+sqrt(6)/4<5<4sqrt(2). Thus its squared eigenvalues are below 32. Also Tr N^2=33, Tr N=-1/2, e2(N)=-131/8 and det N=3/16. Hence e2(N^2)=17173/64 and Tr N^4=17675/32; adding 1024 and dividing by 65^2 gives q. For the coherent maximum, |8+z^2/sqrt(2)|<=8+|z|^2/sqrt(2), and exp(-x)(8+x/sqrt(2))^2 decreases for x>=0 because its derivative is exp(-x)(8+x/sqrt(2))(sqrt(2)-8-x/sqrt(2))<0. Equality at z=0 gives m. T1 gives the gap numerator 224^2+1=1153. The deficit 3/8-q=257/135200 is positive and exceeds 1/[10(2^20+1)]; q>37/100>(17-5sqrt(5))/16, 32/65<1/2 and 64/65<2^20/(2^20+1). This is an actual point inside the necessary scalar region, now excluded by the quadratic identity. It illustrates the uncountable quadratic family and does not assert realizability of arbitrary spectra.

Scope of T1-T2. These analytic consequences, together with T3 in Entropy, remain pending formalization. The existing completed-source Lean declarations retain their own statements and do not kernel-prove the new conclusions. Finite determinant arguments are credited in Entropy, and the physical purity/kernel/coherent-equality prerequisite is positively attributed there to He. The cited literature establishes the stated overlaps and exact hypotheses, without an exhaustive novelty or priority claim. The all-input physical e3 bound and the original all-n/all-eta entropy conjecture remain open.

Analytical writeback R4 and conditional R5

This section is the complete analytical writeback accepted for the same owner after the earlier R1–R3 package. It is prose pending native formalization. The actual channel is fixed throughout: completed Bargmann–Fock H=l2(N;C), e_n(z)=z^n/sqrt(n!), conjugate-linear first slot, D(alpha)f(z)=exp(-|alpha|^2/2+alpha z)f(z-conjugate(alpha)), U(f tensor e)(z,w)=f((z+w)/sqrt(2))e((w-z)/sqrt(2)), V=J_e2, sigma_a=Phi(|a><a|)=C_a C_a*, and Phi*(K)=V*(K tensor Id)V. Every input support, moment, energy, coefficient phase, and output rank remains unrestricted. Write s=||a||^2, E(a)=(s^3-3s Tr(sigma_a^2)+2Tr(sigma_a^3))/6, G(a)=E(a)-s^3/32, I=inf_{||a||=1}E(a), q=Tr(sigma_a^2), p3=Tr(sigma_a^3), mu=q-p3, B=Phi*(sigma_a-sigma_a^2), and A=(1/2)Id-sigma_a. A negative minimizer means I<1/32 and an attained unit minimizer; it does not mean E<0. All A1–A6 attainment, centering, smoothness, variational, purity and spectral statements remain explicit analytical premises supplied by the earlier owner package.

R4 theorem: operator extension, local analytic eigenvector orbits, moments, and the common centered family

For every bounded complex K, with no compactness or self-adjointness assumption, the real map (x,y) -> D(x+iy)* Phi*(K) D(x+iy) has an entire operator-norm holomorphic extension in independent complex x,y. In the repository sign convention it is

L_K(x,y)=J_{E2(conjugate(x),conjugate(y))}*(K tensor Id)J_{E2(x,y)},

where E2(x,y)(z)=exp(-(x^2+y^2)/2-(x+iy)z)(z+x-iy)^2/sqrt(2). The reflected adjoint is holomorphic because adjunction conjugates the antiholomorphic scalar coefficients. The channel covariance used here is Phi_e(D(alpha)T D(alpha))=Phi_{D(-alpha)e}(T), and trace duality gives D(alpha)Phi_e(K)D(alpha)=Phi_{D(-alpha)e}(K), for every complex trace-class T and bounded K. This is the actual splitter sign; no alternate literature convention is substituted.

If K is compact self-adjoint, lambda is any nonzero eigenvalue of L=Phi*(K), and v is any vector in ker(L-lambda Id), then (x,y) -> D(-x-iy)v has a local H-valued holomorphic extension. The eigenspace can have arbitrary finite multiplicity. There are r>0 and M<infinity, uniform for that eigenspace vector, such that for every k>=0,

sum_n ((n+k)!/n!) |v_n|^2 <= M^2 (k!)^2 r^(-2k),

and, for 0<c<r,

sum_n exp(c sqrt(n+1))|v_n|^2 <= 2M^2/(1-(c/r)^2).

Thus v lies in Dom(exp((c/2)sqrt(N+1))); no exp(tN), entire eigenvector orbit, finite support, finite output rank, or uniform moment bound is asserted.

R4 proof

Step 1: Valid: finite environmental and seed vectors have entire complexified orbits..

For any finite Fock polynomial w, W_w(x,y)(z)=exp(-(x^2+y^2)/2-(x+iy)z)w(z+x-iy) is pointwise entire. On every compact parameter polydisc, each fixed parameter derivative has squared Bargmann integrand bounded by C(1+|z|)^m exp(-|z|^2+C|z|). This is integrable. Dominated difference quotients give H-valued partial holomorphy and joint Banach holomorphy. No unknown v is differentiated here.

Step 2: Valid: reflected adjoint is jointly holomorphic; the repository environmental sign is minus..

J_e depends boundedly complex-linearly on e, ||J_e||=||e||, and ||J_e*(K tensor Id)J_f||<=||K||||e||||f||. If E2 has a local vector power series, E2(conjugate(x),conjugate(y)) is antiholomorphic; adjunction conjugates its scalar coefficients again. Thus J_{E2(conjugate(x),conjugate(y))}* is holomorphic in both variables, and its product with J_{E2(x,y)} is entire for every bounded complex K. Source rotate sends (alpha,0) to (alpha/sqrt2,alpha/sqrt2), and (0,-alpha) to (alpha/sqrt2,-alpha/sqrt2). The discarded-mode unitary cancels in partial trace, so Phi_e(D(alpha)T D(alpha))=Phi_{D(-alpha)e}(T) for all S1 T. Trace duality gives precisely D(alpha)Phi_e(K)D(alpha)=Phi_{D(-alpha)e}(K). This verifies the sign rather than importing another splitter convention.

Step 3: Valid: local analytic spectral projection around any nonzero eigenvalue..

A5 supplies compact self-adjoint L for compact self-adjoint K. A nonzero lambda is isolated with finite-rank orthogonal projection P. On a small fixed circle Gamma around lambda, the resolvent of L_K is (z-L)^(-1)[Id-(L_K-L)(z-L)^(-1)]^(-1). A locally uniform Neumann series proves operator-norm holomorphy, and its contour integral defines holomorphic P(x,y). On real parameters unitary conjugacy gives P(x,y)=D(-alpha)P D(alpha). This step does not apply to an arbitrary zero eigenspace.

Step 4: Valid also for degenerate eigenspaces: finite seeds introduce no finite-support hypothesis..

The image P(D_fin) of the dense linear finite-polynomial subspace is dense in Ran P. It is a linear subspace of a finite-dimensional space, hence closed and equal to Ran P. For any v there is a finite polynomial w with Pw=v, not merely an approximating sequence. F_v=P(x,y)W_w(x,y) is holomorphic and for real parameters equals D(-alpha)v. Simplicity is unnecessary here. No generator domain is used.

Step 5: Valid: exact creation line, coefficient factors and k=0..

For fixed z, bounded Bargmann evaluation of F_v agrees on real x,y with exp(-(x^2+y^2)/2-(x+iy)z)f_v(z+x-iy). The scalar right side is entire even before its H-membership is known. Successive one-variable identity theorems on a local polydisc identify it with the holomorphic evaluation of F_v. On x=t/2,y=t/(2i), x+iy=t, x-iy=0, and x^2+y^2=0, so g_v(t)(z)=exp(-tz)f_v(z). Cauchy gives ||g_v^(k)(0)||<=M k! r^(-k). Its occupation coefficient at n>=k is (-1)^k sqrt(n!/(n-k)!)v_{n-k}, and is zero for n<k. Parseval yields exactly the rising-factorial inequality after reindexing. For k=0 it is ||v||^2<=M^2. Hilbert-space derivatives exist before multiplication by z^k is recognized, so there is no circular unbounded-operator argument.

Step 6: Valid: square-root moment and constants, including the factor 1/2 in the operator domain..

For all k>=0, (n+1)^k<=(n+k)!/n!, including equality at k=0. With u=c sqrt(n+1), exp(u)<=2cosh(u). Tonelli and (2k)!>=(k!)^2 bound the weighted sum by 2M^2 sum_{k>=0}(c/r)^(2k)=2M^2/(1-(c/r)^2). The squared norm of exp(t sqrt(N+1))v uses weight exp(2t sqrt(n+1)), hence t=c/2. This is a proved moment, not an input assumption.

Step 7: Valid for every sequence in the entire centered family, not just chosen representatives..

A3 gives a_0>c0 on M_c. For any sequence a_j in M_c, weak subsequential compactness gives a_j weakly to a with a_0>=c0, so t=||a||^2>0. Apply A2 directly to a_j=a+r_j: r_j is bounded weakly null and ||r_j||^2 tends to 1-t. A4 homogeneity and the physical e2 bound yield I>=I[t^3+(1-t)^3]+(5/16)[t(1-t)^2+(1-t)t^2]=I+t(1-t)(5/16-3I). Since I<=1/32, the last factor is at least 7/32>0, so t=1. Thus convergence is strong. E, occupation coordinates, and sqrt(m), which is 1-Lipschitz, preserve E=I and the maximizing positive gauge. Reapplying A3 to the limiting actual negative minimizer retains its strict lower bound. This proves nonempty compact M_c without a new displacement, energy bound, or assumed analytic vector.

Step 8: Valid: common gap follows from positive-compact ordered eigenvalue continuity..

On unit vectors, ||sigma_a-sigma_b||_1<=2||a-b||. Hence K_a varies continuously in operator norm; for example ||K_a-K_b||<=3||sigma_a-sigma_b||1<=6||a-b||. Contractivity of Phi* gives continuity of B_a. The min-max formulas imply |lambda_j(B)-lambda_j(C)|<=||B-C|| for positive compact operators, including j=1,2 and zero padding. R1 makes the top eigenvalue simple and A6 identifies it as mu_a>0. Therefore delta(a)=lambda_1(B_a)-lambda_2(B_a)>0 is continuous on the compact whole M_c, and its minimum delta* is positive. This argument tolerates rank changes. It does not assert a Hessian gap.

Step 9: Valid: common complex neighborhood, positive-seed gauge, Cauchy radius and tail..

For every density 0<=K_a<=Id/4. The bounded J map gives ||L_K(x,y)-Phi*(K)||<=||K||[||E2(conjugate(x),conjugate(y))-e2||||E2(x,y)||+||E2(x,y)-e2||], which tends uniformly to zero over this K-family. Choose rho as in the theorem. On Gamma_a: |z-mu_a|=delta_/3, self-adjoint spectral distances give ||(z-B_a)^(-1)||<=3/delta_; Neumann inversion gives ||(z-L_{K_a})^(-1)||<=6/delta_*. Its contour projection therefore has norm at most 2. At zero P_a=|a><a| and P_a e0=a_0 a because a_0 is real positive. Thus F_a=a_0^(-1)P_a(x,y)W_0(x,y) extends D(-alpha)a and has common bound M=2S_rho/c0. The line |t|<=rho lies in |x|,|y|<=rho/2, leaving a holomorphic neighborhood of the closed t-disc. Hence r=rho is valid, with no missing factor 2. Steps 5-6 apply uniformly, c=r/2 gives C=8M^2/3, and n>L implies sqrt(n+1)>=sqrt(L+2), proving the stated tail.

R4 complete centered-family conclusion

Under I<1/32, let M_c be the entire set of unit global minimizers satisfying the positive maximizing coherent gauge a_0=sqrt(m(a))>0 real and a_1=0, where m(a)=sup_alpha |<D(alpha)e0,a>|^2. The supplied A3–A4 package makes M_c nonempty and norm compact. For a in M_c put K_a=sigma_a-sigma_a^2 and B_a=Phi*(K_a), with mu_a=q_a-p3_a=||B_a||. The top eigenvalue is simple by R1, so with lambda_2(B_a) the second ordered eigenvalue, counting multiplicity and padding finite rank by zeros,

delta_* = min_{a in M_c}(mu_a-lambda_2(B_a))>0.

The min–max Lipschitz bound |lambda_j(B)-lambda_j(C)|<=||B-C|| and ||B_a-B_b||<=6||a-b|| give continuity, and compactness gives the common gap. Choose c0=((4-sqrt(10))/24)^(1/4), so a_0>c0 on M_c. Uniform holomorphy and the common gap give rho>0 with ||L_{K_a}(x,y)-B_a||<=delta_/6 on |x|,|y|<=rho. If W_0(x,y)(z)=exp(-(x^2+y^2)/2-(x+iy)z) and S_rho is its supremum norm on that polydisc, take M=2S_rho/c0 and r=rho. At the Riesz projection P_a(0)=|a><a|, P_a(0)e0=a_0a; finite polynomial seeds establish the degenerate case before the centered rank-one formula is used. The contour resolvent has norm at most 6/delta_ and the projection norm is at most two. Cauchy estimates, the exact creation line, Parseval, Tonelli and exp(u)<=2cosh(u) yield the factorial and square-root estimates uniformly on M_c. In particular c=r/2 and C=8M^2/3 give

sup_{a in M_c} sum_n exp(c sqrt(n+1))|a_n|^2 <= C,

sum_{n>L}|a_n|^2 <= C exp(-c sqrt(L+2))

for every L>=0. The common constants are existential; no numerical value, uniform exp(tN), uniqueness of minimizers, or Hessian gap is claimed.

R5 theorem: one finite coordinate projection and exact l2 tail graphs

Assume the same conditional I<1/32 problem and define Z={z in H:z_0=0} as a real Hilbert space, B_Z={||z||<1}, Xi(z)=sqrt(1-||z||^2)e0+z, F=E o Xi, and K={a-a_0e0:a in M_c}. There is one integer L>=2 and P=P_L projecting onto the complex span of e_1,…,e_L, with Q=Id-P on Z. The ambient chart and every variation retain arbitrary complex a_1 and the entire l2 tail. There are c,H,Cemb,Cgrad,kappa>0, theta in [1/2,1), and 0<epsilon<(1/32-I)/2, depending only on this fixed conditional problem, such that:

every a,b in M_c satisfy ||a-b||<=Cemb (sum_{n=1}^L |a_n-b_n|^2)^(1/2); hence P is injective on the whole centered minimizing family and has a Lipschitz inverse on its image; * finitely many open product neighborhoods in PZ x QZ cover K, and in each there is a real-analytic l2-valued Psi_j:U_j->QZ with Q grad F(x+y)=0 iff y=Psi_j(x); * f_j(x)=F(x+Psi_j(x)) obeys f_j>=I and, with eta=y-Psi_j(x), (c/2)||eta||^2 <= F(x+y)-f_j(x) <= (H/2)||eta||^2, ||eta|| <= c^(-1)||Q grad F(x+y)||; * within these neighborhoods F=I iff y=Psi_j(x) and f_j(x)=I, full stationarity iff y=Psi_j(x) and grad f_j(x)=0, and local minima correspond exactly between F and f_j; the phase slice gives the corresponding full-sphere statements while arbitrary displacements and other kernel directions remain; * every unit completed input a with E(a)<=I+epsilon satisfies (E(a)-I)^theta<=Cgrad||R(a)||, where sphere stationarity is exactly R(a)=0, so no stationary energy lies in (I,I+epsilon]; and * every unit global minimizer has lambda_6(sigma_a)>=kappa, while after reducing epsilon every unit E<=I+epsilon input has lambda_6>=kappa/2 and sum_{j>=6}lambda_j>=kappa/2, with ordered eigenvalues counted with multiplicity and padded by zeros at finite rank.

R5 proof

Step 1: Physical real analyticity, full phase slice, and residual.

The bound ||C_u C_v*||_1<=||u||||v|| and trace-ideal multiplication make E a continuous real homogeneous degree-six polynomial on all H. Xi is real analytic on B_Z, hence so is F. This never differentiates an unbounded number, creation, or Weyl generator.

With a=Xi(z) and a0=sqrt(1-||z||^2), J_z v=D Xi(z)v=v-e0 Re<z,v>/a0. Its range is {h:Re<a,h>=0 and Im h0=0}. Every full real sphere tangent vector decomposes uniquely as J_z v+t ia because a0>0: take t=Im h0/a0 and v=P_Z(h-t ia). Thus the slice removes exactly one real phase direction, without removing either real component of a1.

On the unit sphere, A5 gives ambient grad E=2(e2 Id-B_a)a. Euler homogeneity gives radial derivative 6E and thus sphere grad E=2[(e2-3E)a-B_a a]=-2R(a), since e2-3E=q-p3. Therefore grad F=J_z*[-2R(a)]. Phase invariance gives zero derivative on ia, so grad F=0 iff the full sphere gradient vanishes. This proves stationarity iff R=0, not merely one implication.

J_zJ_z=Id+ell_zell_z, ell_z(v)=Re<z,v>/a0, so ||J_z||=1/a0. Compactness and the vacuum bound give a uniform chart bound near K. Consequently any inequality controlled by ||grad F|| converts to a physical residual inequality with a fixed factor 2 sup||J_z||.

Step 2: Exact Hessian 2Q and one uniform high-direction coercivity.

At every z in K, a=Xi(z) is a constrained critical point, so the chart Hessian equals the constrained Hessian pulled back by J_z. The accepted normalized real-curve expansion is E((a+t h)/sqrt(1+t^2||h||^2))=I+t^2 Q_a(h)+O(t^3), h in the FULL real sphere tangent. Hence D2F(z)[v,v]=2Q_a(J_z v). The factor 2 is compulsory and correctly retained.

Define on H_R the compact real-linear map M_a h=((1/2)Id-sigma_a)^(1/2)Phi(|h><a|+|a><h|), with values in S2_R. Its squared norm is Tr(((1/2)Id-sigma_a)X_h^2). Using real adjoints and composition by J_z gives D2F(z)=2mu_a Id+T_z, T_z=2mu_a ell_zell_z-2J_z(B_a+M_aM_a)J_z. Every term in T_z is compact and real self-adjoint. No claim that unrestricted M_aM_a preserves the tangent is used; J_z* performs the necessary compression.

The map z->T_z is operator-norm continuous on K directly from T_z=D2F(z)-2mu_a Id. Here mu_a is trace-polynomial continuous. Thus {T_z:z in K} is a NORM-compact set of compact operators. For a single compact T, Q_L->0 strongly and finite-rank approximation give ||Q_L T Q_L||->0. A finite operator-norm net then gives sup_K||Q_L T_z Q_L||->0. Pointwise compactness without this norm-compactness would not justify one L.

Let mu_=min_K mu_a>7/32. Choose L so sup_K||Q_L T_z Q_L||<=mu_. Then D2F(z)[v,v]>=mu_*||v||^2 for v in Q_L Z. A finite continuity cover of compact K gives rho,c,H>0 with the entire tube U={dist(z,K)<rho} contained in B_Z, high-direction D2F>=c Id, and ||D2F||<=H on U. Taking rho below the distance from K to the chart boundary ensures this tube condition. Enlarging L preserves the same c,H,rho because the new high space is a subspace of the old one. No full-Hessian positivity or common kernel complement is assumed.

Step 3: Integrated-Hessian global finite-coordinate embedding.

Compactness of the ENTIRE K in l2 gives sup_{z in K}||Q_L z||->0. Enlarge the SAME L from Step 2 until this supremum is <rho/8. For any z,w in K set u=P(w-z), v=Q(w-z); then ||v||<rho/4.

If ||u||<rho/2, every point of z+t(u+v), 0<=t<=1, lies within 3rho/4 of z in K, hence in U. Both endpoint gradients vanish. The fundamental theorem for the continuous Hessian, paired with the fixed real high vector v, gives 0=integral_0^1 D2F(z+t(u+v))[u+v,v]dt >= c||v||^2-H||u||||v||. For v=0 the desired bound is immediate; otherwise division yields ||v||<=(H/c)||u||.

If ||u||>=rho/2, the unit-ball bound gives ||w-z||<=2<=(4/rho)||u||. Thus for every pair in K, ||w-z||<=C_Z||P(w-z)|| with C_Z=max(sqrt(1+(H/c)^2),4/rho). In particular a zero low-coordinate difference forces a zero whole difference.

The convex closed ball ||z||<=sqrt(1-c0^2) contains K, and ||D Xi||<=1/c0 on it. Integrating D Xi along its line segments proves the stated estimate for a,b in M_c with Cemb=C_Z/c0. This proves global injection and a Lipschitz inverse on the image; local IFT charts alone would not prove that global assertion.

Step 4: Analytic l2 tail graphs, estimates and all point correspondences.

For z0=x0+y0 in K apply the REAL-analytic Banach IFT to g(x,y)=Q grad F(x+y), a map PZ x QZ->QZ. Its y derivative A_Q=Q D2F(z0)|_{QZ} is bounded self-adjoint and >=c Id. This implies an isomorphism: its range is closed by the lower bound and dense because ker(A_Q*)=0. Also ||A_Q^(-1)||<=1/c. The IFT yields a QZ-valued real-analytic Psi, uniqueness of g=0 in a product neighborhood, and Psi(x0)=y0.

Shrink each product neighborhood so that Psi(x) stays in its high ball and every segment between Psi(x) and y remains in U at fixed x. With eta=y-Psi(x), integrating the high Hessian twice gives F(x+y)-F(x+Psi(x))=integral_0^1 (1-t)D2F(x+Psi(x)+t eta)[eta,eta]dt, hence the exact c/2 and H/2 bounds.

Integrating once and pairing with eta gives <Q grad F(x+y),eta> >= c||eta||^2, since Q grad F vanishes at the graph. Cauchy-Schwarz proves ||eta||<=||Q grad F(x+y)||/c, including eta=0.

On the graph, Df(x)[u]=DF(x+Psi(x))[u+D Psi(x)u]=<P grad F(x+Psi(x)),u>, because D Psi takes values in QZ and the high gradient vanishes. Thus grad f=P grad F on the graph, so full stationarity is equivalent to grad f=0 there. The phase decomposition of Step 1 makes this a full sphere stationary correspondence.

Every chart point is an actual unit input, so F>=I and f>=I. The positive transverse remainder proves F=I iff eta=0 and f=I. It also proves the general local-minimum correspondence: a local minimum of f lifts to one of F, and restriction to the continuous graph gives the converse. A finite subcover covers every point of K. Nothing claims a single global analytic extension over an open set of low coordinates; all high amplitudes remain in the true l2-valued Psi.

Step 5: All exponents, constants and the uniform local gradient inequality.

At each graph base x_j, f_j is real analytic on a finite-dimensional REAL space PZ, f_j(x_j)=I and grad f_j(x_j)=0. Feehan-Maridakis v10 Theorem 2.2(1) gives (f_j-I)^alpha_j<=A_j||grad f_j|| for some 0<alpha_j<1 near x_j. With 0<=f_j-I<=1, replacing alpha_j by theta_j=max(alpha_j,1/2) preserves the inequality. If f_j is locally constant at I, choose theta_j=1/2; its inequality is trivial. No Morse-Bott part (2) is invoked.

For z=x+y, p=grad F(z), and eta=y-Psi_j(x), Step 4 yields ||eta||<=||p||/c. The Hessian bound on the high segment gives ||grad f_j(x)||<=||p||+H||eta||<=(1+H/c)||p||, and 0<=F(z)-f_j(x)<=D||p||^2 with D=H/(2c^2).

For 0<theta_j<1, subadditivity gives (F-I)^theta_j<=A_j(1+H/c)||p||+D^theta_j||p||^(2theta_j). Shrink around each base so ||p||<=1. Since 2theta_j>=1, ||p||^(2theta_j)<=||p||. Thus a valid local constant is Atilde_j=A_j(1+H/c)+D^theta_j. This verifies every exponent direction and the vertical-error power.

Choose a finite collection of these shrunk neighborhoods covering K. With theta=max_j theta_j<1, A=max_j Atilde_j, and F-I<=1, the same inequality (F-I)^theta<=A||grad F|| holds on their union. A common bound J_* for J_z gives Cgrad=2J_* A after Step 1. Alternatively D2F(z)=2mu Id+compact is index-zero Fredholm under the real Hilbert Riesz identification, so the checked Theorem 1 applies. The finite-dimensional proof above supplies the exact reduction and estimates rather than assuming its exponent.

Step 6: Every low centered input lies near the whole compact family.

More precisely, for every open norm neighborhood O of K in B_Z there is epsilon_O>0 such that every coherently maximizing, positive-phase centered unit b with E(b)<=I+epsilon_O has b-b0 e0 in O. Suppose otherwise and choose such b_j outside O with E(b_j)->I. These are arbitrary already centered near-minimizers, not just selected orbit representatives.

A3 gives an eventually uniform b_j0>c0. Take a weakly convergent subsequence b_j weakly to b, and set t=||b||^2. Then b0>=c0, so 0<t<=1; r_j=b_j-b is bounded weakly null and ||r_j||^2->1-t. Apply A2 directly to this sequence. Both cross-mass terms, homogeneity and the physical e2 lower bound yield I>=I[t^3+(1-t)^3]+(5/16)[t(1-t)^2+(1-t)t^2]=I+t(1-t)(5/16-3I).

Because I<=1/32, the last coefficient is >=7/32>0. Thus t=1, whence b_j->b strongly, ||b||=1 and E(b)=I. No convergence of E(r_j) or energy/moment bound is required: the pointwise homogeneous lower bound suffices under liminf.

The coherent supremum sqrt(m(.)) is 1-Lipschitz in H. Strong convergence therefore preserves b0=sqrt(m(b))>0 real and b1=0, so b belongs to the ENTIRE M_c. The chart coordinates converge into K subset O, a contradiction. The same argument proves uniform distance of all centered low-sublevel inputs to M_c tends to zero as the sublevel shrinks. Merely knowing compactness modulo unspecified displacements would not supply this statement.

Step 7: All-input physical residual inequality and critical-value gap.

Use Step 6 for the neighborhood obtained in Step 5. For every arbitrary unit completed a choose any attained maximizing coherent overlap and a scalar phase, giving b=W a in the positive centered gauge. The chosen W is a FIXED bounded complex unitary when differentiating. Completed covariance and homogeneity imply E(Wu)=E(u) for every u.

Differentiating with W held fixed and using real Hilbert Riesz uniqueness gives grad_sphere E(Wa)=W grad_sphere E(a). Thus R(Wa)=W R(a) and ||R(b)||=||R(a)||. No differentiability or continuous choice of the maximizing center as a function of a is needed, and no initially finite photon moment is used.

Step 5 applied to b therefore gives (E(a)-I)^theta<=Cgrad||R(a)|| for EVERY unit a in the common low sublevel. Reduce epsilon to be positive and <(1/32-I)/2, and later reduce it for Step 8. If a is stationary in this sublevel, R(a)=0, so E(a)=I. Conversely every global minimizer is stationary by A5. A family of minima or additional degeneracy at the same bottom value is fully consistent with this result.

Step 8: Sixth-eigenvalue mass with all ranks and all low inputs.

T2 implies rank(sigma_a)>=6 for each a in M_c, so lambda_6(sigma_a)>0. For positive compact S,T on this same infinite H, the min-max formula gives |lambda_j(S)-lambda_j(T)|<=||S-T|| with multiplicity and finite-rank zero padding, including j=6. It needs no simple eigenvalues, common eigenvectors or locally fixed rank.

For unit a,b, the rank-one decomposition gives ||sigma_a-sigma_b||_1<=|| |a><a|-|b><b| ||1<=2||a-b||, using the trace-norm contraction of the physical channel on self-adjoint trace class. Since operator norm<=trace norm, lambda_6 o sigma is continuous on the whole norm-compact M_c. Therefore kappa=min{a in M_c}lambda_6(sigma_a)>0. Pointwise positive rank alone, without that compactness/continuity, would not imply this minimum.

The distance version of Step 6 puts EVERY centered low-sublevel b within kappa/4 of M_c after one common reduction of epsilon. Choosing a corresponding a in M_c gives lambda_6(sigma_b)>=kappa-2||b-a||>=kappa/2 (with a strict inequality available if the distance is strict). Output displacement covariance preserves the eigenvalues and extends the same bound to every original unit input. It also gives lambda_6>=kappa for all uncentered global minimizers.

Because all ordered eigenvalues are nonnegative, sum_{j>=6}lambda_j>=lambda_6. The sum is well-defined for every positive trace-class output, including infinitely many positive eigenvalues. Rank changes therefore cause no gap in either the eigenvalue or the mass statement.

R5 F0–F5 interfaces and native limits

F0. Reuse the exact completed occupation/Bargmann, C_a/S2, Phi/S1, trace and normal-channel joins. Instantiate bounded real polynomial differentiation on the realification of H, the positive-vacuum sphere chart and arbitrary-input displacement covariance. Prove sphere grad=-2R and the phase-slice equivalence.

Native boundary: The named historical physical joins and analytical A5 are evidence, not new kernel receipts. No active source inspection was allowed, so exact current native declaration/API availability is unassessed. A coherent-input-only covariance theorem is insufficient.

F1. Reuse or expose R3 full real sphere Hessian and compact coherence map; supply real Hilbert-Schmidt/adjoint identities, J* compression, the constrained second derivative 2Q, and D2F=2mu Id+compact. Prove norm continuity from the actual analytic F. The scalar bound mu>7/32 uses Newton and physical q<=3/8.

Native boundary: Do not claim the fixed-B gap supplies a Hessian gap. R1 channel injectivity, simplicity and R2/R4 analytic orbit machinery are unnecessary extra dependencies if the scalar bound and the compact-family clauses are independently available.

F2. Reuse compactness of the ENTIRE M_c, exact gauge and vacuum lower bound. Prove uniform compression of a norm-compact compact-operator family by occupation tails; select one L and one tube; prove the integrated-Hessian all-pairs estimate and Xi Lipschitz bound. Supply the genuine REAL-analytic Banach IFT on infinite-dimensional QZ, high-Hessian invertibility, analytic Riesz gradient, exact graph equivalence and integral remainder/residual bounds.

Native boundary: Native suppliers for compact operator approximation, operator-norm continuity, Banach differentiation/integration, real adjoints and the analytic IFT must be found or proved under repository rules. A merely smooth IFT would not by itself certify analytic f; a finite-dimensional or truncated-tail IFT would prove a different theorem.

F3. Supply a proved finite-dimensional real-analytic Lojasiewicz gradient theorem with exactly Theorem 2.2(1) hypotheses, or a proved real Hilbert analytic-Fredholm specialization of Theorem 1, then instantiate the finite-cover exponent and all-input transfer estimates. A continuous real Riesz identification is definite and D2F=2mu Id+compact is Fredholm index zero, so the alternative Theorem 1 has its hypotheses.

Native boundary: This primary citation establishes a valid mathematical ingredient, not a Lean axiom or a verified existing supplier. No source search was allowed here, so no assertion that a suitable native theorem is present or absent is made. If unavailable, retain the full analytical theorem and mark the gradient/critical-value native claims as awaiting this supplier. The embedding, tail graph and spectral conclusions have no Lojasiewicz dependency.

F4. Reuse A2-A4 for every ALREADY centered minimizing sequence and both cross-mass terms; prove the low-sublevel neighborhood/distance lemma, coherent-supremum Lipschitz gauge continuity and fixed-unitary real-gradient equivariance. For the spectrum reuse T2, the actual positive trace-class output, trace-norm continuity, compact positive min-max and finite-rank zero padding.

Native boundary: No local fixed-rank eigenvector API, finite output-rank assumption or countable spectral entropy theorem is needed for lambda_6 and the nonnegative tail sum. A claim merely about one chosen minimizing sequence or one selected representative per orbit is too weak for the final uniform statements.

F5. Keep the inherited P/T/A/R scopes, all center coefficients, every middle and high relative sector, initial unrestricted domain and all global-sign/entropy abstentions. Retain source identity and same-owner responsibility for the analytical-to-native joins.

Native boundary: R5 does not turn the analytic premises into compiled declarations. Future same-owner formalization needs faithful D5/Blueprint statements, actual suppliers, scoped kernel/axiom evidence, and existing repository validation/admission gates. This worker neither inspected nor performed those gates.

R4/R5 boundaries and preserved global target

The fixed-B spectral gap from R1 is not a full Hessian gap: R3 retains the real Hessian 2Q, the restricted real adjoint, compact coherence correction, phase direction, and coercivity only off the entire finite-dimensional kernel. R5 does not assert isolated minimizers, Morse–Bott structure, a finite cutoff, finite output rank, or a classification of the Hessian kernel. Its Lojasiewicz input is a finite-dimensional real-analytic theorem applied after the exact l2-valued graph reduction; a smooth, finite-dimensional, or truncated-tail substitute would prove a different statement. All complex coefficients, including a_1 before the phase-only slice, and all same-input physical covariance remain in scope.

The same-input inequality p3>=5/32-(3/2)(3/8-q) remains open for arbitrary physical inputs. At a hypothetical negative minimizer retain Ba=mu a, the full real second variation, every center coefficient, every M=6,…,63 sector and the complete M>=64 tail. No global e3 sign, entropy theorem, all-n/all-eta conjecture, uniqueness, or parent-goal completion follows. R4 and R5 are conditional analytical results, pending the named native suppliers and the repository gates described below.

Definition 1.1 (ProbabilityVector).

$\forall p : P ro babi l i t y V ec t or, (weight (p) : N \to R) \forall p : P ro babi l i t y V ec t or, (\forall n : N, (0 \leq weight (p, n))) \forall p : P ro babi l i t y V ec t or, (HasSum (weight (p), 1))$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/Attenuator.ProbabilityVector (✓ std3).

Citation. Zacharie Van Herstraeten; Saikat Guha; Nicolas J. Cerf (2024). Classical capacity of quantum non-Gaussian attenuator and amplifier channels. DOI: 10.1142/S0219749924400033. URL: https://arxiv.org/abs/2312.15623v2.

Commentary.

The structure has precisely the data field weight: Nat -> Real and proof fields nonneg and normalized displayed as separate rows above; its support is unrestricted.

Definition 1.2 (DensityOperator).

$\forall r h o : De n s i t y Op er a t or, (operator (r h o) : ContinuousLinearMap (C, lp (Functionconst (N, C), 2), lp (Functionconst (N, C), 2))) \forall r h o : De n s i t y Op er a t or, (IsPositive (operator (r h o))) \forall r h o : De n s i t y Op er a t or, (HasSum ((n : N) \mapsto (Re (inner (C, lpsingle (2, n, ComplexofReal (1)), operator (r h o) (lpsingle (2, n, ComplexofReal (1)))))), 1))$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/Attenuator.DensityOperator (✓ std3).

Commentary.

The structure has precisely the data field operator and proof fields positive and trace_one displayed as separate rows above. For a positive bounded operator, finite full-basis diagonal sum characterizes trace class. No Fock-diagonality assumption is made on inputs.

Definition 1.3 (outputVector).

$\forall e t a : R, (\forall h Et a : e t a \in SetIcc (0, 1), (\forall p : P ro babi l i t y V ec t or, (\forall r h o : De n s i t y Op er a t or, (\forall q : Prod (N, Prod (N, N)), (outputVector (e t a, h Et a, p, r h o, q) = smul (ComplexofReal (sqrt (weight (p, fst (q)))), beamSplitter (e t a, h Et a, tensor (CFCsqrt (operator (r h o)) (lpsingle (2, fst (snd (q)), ComplexofReal (1))), lpsingle (2, fst (q), ComplexofReal (1)))) (snd (snd (q)))))))))$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/Attenuator.outputVector (✓ std3).

Commentary.

q=(n,m,l) indexes the environment number n, the square-root column m of the input, and the discarded-mode slice l. This is the square-root Kraus realization of Tr_2[U_eta(rho tensor sum_n p_n|n><n|)U_eta^dagger], including off-diagonal inputs.

Definition 1.4 (attenuatorOperator).

$\forall e t a : R, (\forall h Et a : e t a \in SetIcc (0, 1), (\forall p : P ro babi l i t y V ec t or, (\forall r h o : De n s i t y Op er a t or, (attenuatorOperator (e t a, h Et a, p, r h o) = mixture (Prod (N, Prod (N, N)), (q : Prod (N, Prod (N, N))) \mapsto (outputVector (e t a, h Et a, p, r h o, q)))))))$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/Attenuator.attenuatorOperator (✓ std3).

Commentary.

The displayed equation specifies the defining expression.

Definition 1.5 (attenuator).

$\forall e t a : R, (\forall h Et a : e t a \in SetIcc (0, 1), (\forall p : P ro babi l i t y V ec t or, (\forall r h o : De n s i t y Op er a t or, (operator (attenuator (e t a, h Et a, p, r h o)) = attenuatorOperator (e t a, h Et a, p, r h o)))))$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/Attenuator.attenuator (✓ std3).

Commentary.

The state constructor has this operator field. Summability, positivity and trace one of the full triple-index ensemble are checked in Lean.

Definition 1.6 (pureDensity).

$\forall v : lp (Functionconst (N, C), 2), (\forall h v : ∥ v ∥ = 1, (operator (pureDensity (v, h v)) = rankOne (C, v, v)))$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/Attenuator.pureDensity (✓ std3).

Commentary.

The normalized vector gives its existing Mathlib rank-one projector as the operator field; positivity and trace-one proofs complete the density structure.

Definition 1.7 (pureOutputVector).

$\forall e t a : R, (\forall h Et a : e t a \in SetIcc (0, 1), (\forall p : P ro babi l i t y V ec t or, (\forall v : lp (Functionconst (N, C), 2), (\forall q : Prod (N, N), (pureOutputVector (e t a, h Et a, p, v, q) = smul (ComplexofReal (sqrt (weight (p, fst (q)))), beamSplitter (e t a, h Et a, tensor (v, lpsingle (2, fst (q), ComplexofReal (1)))) (snd (q))))))))$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/Attenuator.pureOutputVector (✓ std3).

Commentary.

The displayed equation specifies the defining expression.

Definition 1.8 (pureAttenuatorOperator).

$\forall e t a : R, (\forall h Et a : e t a \in SetIcc (0, 1), (\forall p : P ro babi l i t y V ec t or, (\forall v : lp (Functionconst (N, C), 2), (pureAttenuatorOperator (e t a, h Et a, p, v) = mixture (Prod (N, N), (q : Prod (N, N)) \mapsto (pureOutputVector (e t a, h Et a, p, v, q)))))))$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/Attenuator.pureAttenuatorOperator (✓ std3).

Commentary.

The pure-input ensemble agrees with the full square-root attenuator. The environment expansion sums p_n times the partial trace of U_eta(v tensor |n>).

Theorem 1.9 (coherent_output_covariance).

$\forall e t a : R, (\forall h Et a : e t a \in SetIcc (0, 1), (\forall p : P ro babi l i t y V ec t or, (\forall a lp ha : C, (pureAttenuatorOperator (e t a, h Et a, p, displacement (a lp ha, lpsingle (2, 0, ComplexofReal (1)))) = conjStarAlgEquiv (displacement ((ComplexofReal (sqrt (e t a))) \cdot (a lp ha)), pureAttenuatorOperator (e t a, h Et a, p, lpsingle (2, 0, ComplexofReal (1))))))))$

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

Commentary.

For every countably supported phase-invariant environment, every coherent input has a displaced vacuum output. The assertion concerns the full operator, including its coherences.

Definition 1.10 (coherentDensity).

$\forall a lp ha : C, (operator (coherentDensity (a lp ha)) = rankOne (C, coherent (a lp ha), coherent (a lp ha)))$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/Attenuator.coherentDensity (✓ std3).

Commentary.

The displayed equation specifies the defining expression.

Definition 1.11 (fockDensity).

$\forall n : N, (operator (fockDensity (n)) = rankOne (C, lpsingle (2, n, ComplexofReal (1)), lpsingle (2, n, ComplexofReal (1))))$

Formalization. D5/S3/Quantum/QuantumChannels/FockAttenuator/Attenuator.fockDensity (✓ std3).

Commentary.

The displayed equation specifies the defining expression.

References

Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/Attenuator.DensityOperator
Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/Attenuator.ProbabilityVector
Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/Attenuator.attenuator
Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/Attenuator.attenuatorOperator
Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/Attenuator.coherentDensity
Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/Attenuator.coherent_output_covariance
Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/Attenuator.fockDensity
Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/Attenuator.outputVector
Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/Attenuator.pureAttenuatorOperator
Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/Attenuator.pureDensity
Truth anchor: D5/S3/Quantum/QuantumChannels/FockAttenuator/Attenuator.pureOutputVector
Dependency: D5/S3/Quantum/QuantumChannels/FockAttenuator/DisplacementCovariance

Keyboard shortcuts

trureturing — Discovering truth