Beenakker's formula gives the Josephson energy-phase relation of short junctions as a sum over normal-state transmission channels. No comparable channel representation exists beyond the short-junction limit. The allowed range of the normalized quartic coefficient α_r was also open, with a conjectured bound -1 ≤ α_r ≤ 0.

The phase-dependent free energy of a time-reversal-symmetric s-wave Bogoliubov–de Gennes junction is rewritten as a Matsubara sum. Each term is reduced to channel spaces using Takagi and skew-Takagi factorizations of the pairing blocks, which yields frequency-dependent transmissions. Bounds on the phase-expansion coefficients follow from termwise positivity and from analytic constraints on how fast transmissions decay with frequency. All numbered equations were formalized in Lean 4 with Mathlib by AI agents, and the manuscript is generated from the checked declarations.

The authors prove -1 ≤ α_r ≤ 7/80 at finite temperature and α_r ≤ (16-5π)/[4(4-π)] ≈ 0.085 at zero temperature. A four-site junction with α_r ≈ 0.0063 > 0 disproves the conjectured bound α_r ≤ 0. The Lean formalization and agent session logs are released on Zenodo.