Transmission representation of the Josephson free energy beyond the short-junction limit

Beenakker's formula, U(φ)-U(0)=Δ sum n (1-sqrt 1-τ n 2(φ/2)), expresses the zero-temperature energy-phase relation of a short Josephson junction through its normal-state transmission eigenvalues. We generalize this transmission representation beyond the short-junction limit and express the phase-dependent free energy of a time-reversal-symmetric s-wave junction as a Matsubara sum over channels with frequency-dependent transmissions. The representation constrains the small-phase expansion of the free energy. In particular, we prove that the normalized ratio of its quartic and quadratic coefficients satisfies-1 α r 7/80 at finite temperature. We also construct a four-site junction with α r>0, which disproves the conjectured upper bound α r 0. So that these results can be trusted without repeating the derivations, every numbered equation is formally verified in the Lean proof assistant.