theorem GenusPlaneAdjunctionBridge.two_dvd_shifted_product (d : ℕ) : 2 ∣ (d - 1) * (d - 2)

The product (d - 1)(d - 2) is always even, since one of two consecutive integers is even.

theorem GenusPlaneAdjunctionBridge.two_mul_genus_plane_curve (d : ℕ) : 2 * GrothendieckBirkhoff.genus_plane_curve d = (d - 1) * (d - 2)

2 g = (d - 1)(d - 2) for the plane-curve genus formula in ℕ.

theorem GenusPlaneAdjunctionBridge.two_mul_genus_plane_curve_int (d : ℕ) (hd : 2 ≤ d) : 2 * ↑(GrothendieckBirkhoff.genus_plane_curve d) = (↑d - 1) * (↑d - 2)

Integer version of two_mul_genus_plane_curve, valid for d ≥ 2.

theorem GenusPlaneAdjunctionBridge.adjunction_chain_two_g (d g : ℤ) (hdegK : d * (d - 3) = 2 * g - 2) : 2 * g = (d - 1) * (d - 2)

Algebraic step from adjunction: deg K_D = d(d - 3) = 2g - 2 implies 2g = (d-1)(d-2).

theorem GenusPlaneAdjunctionBridge.adjunction_chain_genus (d g : ℤ) (h : 2 * g = (d - 1) * (d - 2)) : g = (d - 1) * (d - 2) / 2

Divide 2g = (d - 1)(d - 2) by 2 to obtain the genus formula g = (d-1)(d-2)/2.

theorem GenusPlaneAdjunctionBridge.adjunction_chain_degK_to_genus (d g : ℤ) (hdegK : d * (d - 3) = 2 * g - 2) : g = (d - 1) * (d - 2) / 2

Combined adjunction chain: from deg K_D = d(d - 3) = 2g - 2, conclude g = (d - 1)(d - 2)/2.

theorem GenusPlaneAdjunctionBridge.genus_plane_curve_eq_adjunction_genus (d : ℕ) (hd : 2 ≤ d) : ↑(GrothendieckBirkhoff.genus_plane_curve d) = (↑d - 1) * (↑d - 2) / 2

The packaged plane-curve genus matches the closed-form (d - 1)(d - 2)/2 from adjunction.