EXACT CLAIM

Fix a,b>0, 0<p<1, q=1-p, and x,y in C with X=|x|²<a and Y=|y|²<b. Set A=a-X, B=b-Y, d=pA+qB, R=Re(conj(x)y), and J=|sqrt(p)x-sqrt(q)y|². For 0<t<t_phys:=min(A/a²,B/b²), independently prepare the one-mode states rho_A(t)=[[1-at,x sqrt(t)],[conj(x)sqrt(t),at]] and rho_B(t)=[[1-bt,y sqrt(t)],[conj(y)sqrt(t),bt]], with zero entries outside the vacuum/one-photon subspace. These are physical finite-energy states. Retain c=sqrt(p)a_op+sqrt(q)b_op after beam-splitter mixing, obtaining rho_C(t). Define F=2pqAB(1+J/d), H=pq[2AX+2BY+(X+Y)²-4R²+2ABJ/d], and Q=pq(A-B)²+F[1-log(F/d²)]. With all parameters fixed, the EPnI gap satisfies
 g^{-1}(S(rho_C(t)))-p g^{-1}(S(rho_A(t)))-q g^{-1}(S(rho_B(t))) = H t² + Q t²/log(1/t) + o(t²/log(1/t)).
If X+Y>0, then H>0. If X=Y=0, then H=0 and Q>=F(1+log 2)>0. Consequently, for each fixed allowed parameter choice there exists t_0 in (0,t_phys] such that EPnI is strict for every 0<t<t_0. This assertion is restricted to this one-mode boundary family.

FULL FROZEN PROOF

All logarithms are natural, and all asymptotic constants may depend on the fixed parameters.

1. Physicality and exact output. The input determinants are t(A-a²t) and t(B-b²t). On the stated interval they are positive, and both diagonal entries of each input are positive because A/a²<=1/a and B/b²<=1/b. Thus the inputs are normalized positive states with mean photon numbers at and bt.

Use the complementary output mode e=-sqrt(q)a_op+sqrt(p)b_op. In the output Fock basis |n_c,n_e>, the input basis vectors transform as
 |00> -> |00>,
 |10> -> sqrt(p)|10>-sqrt(q)|01>,
 |01> -> sqrt(q)|10>+sqrt(p)|01>,
 |11> -> sqrt(2pq)|20>+(p-q)|11>-sqrt(2pq)|02>.
This fixes the phase convention and shows that the retained output has exactly support in |0>,|1>,|2>; there is no discarded photon-number tail.

Define
 m=pa+qb+2sqrt(pq)R,
 k=2pqab,
 u=sqrt(p)x+sqrt(q)y,
 v=2q sqrt(p)b x+2p sqrt(q)a y,
 w=sqrt(2pq)xy,
 h=sqrt(2pq)(sqrt(q)b x+sqrt(p)a y).
Taking the complementary partial trace gives the exact matrix
 rho_C(t)=
 [[1-mt+kt², u sqrt(t)-v t^(3/2), w t],
  [conj(u)sqrt(t)-conj(v)t^(3/2), mt-2kt², h t^(3/2)],
  [conj(w)t, conj(h)t^(3/2), kt²]].
In particular, m-|u|²=d>0.

2. Output eigenvalues. Put U=|u|², W=|w|² and
 T=-k+2Re(conj(u)v)-(m+d)U-W.
The eigenvalue near one is
 lambda_0=1-dt-Tt²+O(t³).
For completeness, its Schur-complement equation, expanded through t², is
 lambda_0=1-mt+kt²+U t+[ -2Re(conj(u)v)+(m+d)U+W ]t²+O(t³),
which proves the formula.

For an eigenvalue of order t², eliminate the vacuum component. The resulting two-by-two Schur complement has leading entries
 [[d t+O(t²), (h-conj(u)w)t^(3/2)+O(t^(5/2))],
  [(conj(h)-u conj(w))t^(3/2)+O(t^(5/2)), (k-W)t²+O(t³)]].
Consequently the smaller eigenvalue is F t²+O(t³), where initially
 F=k-W-|h-conj(u)w|²/d.
The following exact identities identify this number and establish its positivity:
 h-conj(u)w=sqrt(2pq)(sqrt(q)B x+sqrt(p)A y),
 k-W=2pq(AB+AY+BX),
 d(AB+AY+BX)-|sqrt(q)B x+sqrt(p)A y|²=AB(d+J).
Thus F=2pqAB(1+J/d)>0. Using the trace, the other small eigenvalue is
 lambda_1=d t+(T-F)t²+O(t³),
 while lambda_2=F t²+O(t³).

These expansions have the stated integer-power remainders: the characteristic polynomial of the displayed exact matrix has coefficients polynomial in t. Its simple root at lambda=1 is analytic in t. After factoring out that root, the quadratic for the remaining roots has discriminant d²t²+O(t³). Since d>0, its square root for positive t is t times an analytic function near zero. Both remaining eigenvalues therefore have convergent integer-power expansions near zero. The Schur-complement computation determines their displayed coefficients.

3. Controlled entropy inversion. We establish a general expansion used for both output and inputs. Suppose a finite-rank state's only small nonzero eigenvalues are
 lambda_1=d t+e t²+O(t³), lambda_2=f t²+O(t³),
 with d,f>0, and the other eigenvalue is 1-lambda_1-lambda_2. Write L=log(1/t). Expanding each entropy contribution gives
 S=d t(L+1-log d)+t²[(e+2f)L-e log d+f(1-log f)-d²/2]+O(t³L).
The same formula holds with f=0 when lambda_2 is absent, interpreting f log f as zero.

Since g(z)=z(1-log z)+z²/2+O(z³), define
 z_*(t)=d t+(e+2f)t²+[f(1-log(f/d²))-d²]t²/L,
 again interpreting the f term as zero when f=0. Direct substitution shows g(z_*)-S=o(t²). Also g^{-1}(S)/(dt) tends to one: for every fixed epsilon in (0,d), comparison with g((d-epsilon)t) and g((d+epsilon)t) brackets the inverse for all sufficiently small t. Hence g'(z)=log(1+1/z) is asymptotic to L throughout the interval between z_* and g^{-1}(S). The mean value theorem now gives
 g^{-1}(S)=d t+(e+2f)t²+[f(1-log(f/d²))-d²]t²/L+o(t²/L).
This proves the needed error control, rather than merely formally inverting a leading entropy term.

For input A, its determinant t(A-a²t) implies that its smaller eigenvalue is
 A t+E_A t²+O(t³), where E_A=A²-a²=-2AX-X².
Likewise E_B=B²-b²=-2BY-Y². Applying the inversion formula gives
 g^{-1}(S(rho_A))=A t+E_A t²-A²t²/L+o(t²/L),
 g^{-1}(S(rho_B))=B t+E_B t²-B²t²/L+o(t²/L).
For the output take e=T-F and f=F to obtain
 g^{-1}(S(rho_C))=d t+(T+F)t²+[F(1-log(F/d²))-d²]t²/L+o(t²/L).
Subtracting the weighted input expressions cancels the order-t term. The coefficient of t²/L is exactly
 Q=pA²+qB²-d²+F(1-log(F/d²))=pq(A-B)²+F(1-log(F/d²)).

4. Simplifying the leading coefficient and determining its sign. The coefficient of t² is H=T+F-pE_A-qE_B. To verify its advertised expression explicitly, set U_0=pX+qY and Z=2sqrt(pq)R, so U=U_0+Z and m=d+U. Expansion of the definitions gives
 2Re(conj(u)v)=4pq(bX+aY)+2(d+U_0)Z,
 T=-2pqAB+2pq(AY+BX)+4pqXY-2dU_0-U_0²-4pqR².
Substituting E_A,E_B then yields
 H=F-2pqAB+pq[2AX+2BY+(X+Y)²-4R²]
  =pq[2AX+2BY+(X+Y)²-4R²+2ABJ/d].
Since R²<=XY,
 (X+Y)²-4R² >= (X-Y)² >= 0.
Also J>=0 and A,B,p,q,d>0. Therefore H>=2pq(AX+BY)>0 whenever X+Y>0. For such parameters the gap divided by t² tends to H, regardless of the sign of Q.

If X=Y=0, then J=H=0, A=a, B=b, and F=2pqab. The exact inequality
 d²-4pqab=(pa-qb)²>=0
 implies F/d²<=1/2. Thus
 Q=pq(a-b)²+F[1-log(F/d²)] >= F(1+log 2)>0.
In this case the gap divided by t²/L tends to Q. In both cases the asserted strict inequality for sufficiently small positive t follows. This completes the proof for exactly the stated parameter family.

REMAINING GAP

The full EPnI for arbitrary independent finite-energy inputs remains unresolved. This result covers only a fixed-parameter one-mode vacuum/one-photon boundary family with strictly positive residual slopes A and B. It does not cover the saturated boundaries A=0 or B=0, parameters varying with t, nonperturbative inputs, or multimode correlations. The physical t interval is explicit, but the eventual EPnI threshold is not quantified uniformly.