theorem G67SumCoordinate.weight_continuousOn {a b c d : ℝ} (ha : 0 < a) (hc : 0 < c) (hab : a ≤ b) (hcd : c ≤ d) : ContinuousOn (weight a b c d) (Set.Icc (a + c) (b + d))

Continuity of the closed-form density, including both vanishing endpoints.

theorem G67SumCoordinate.weight_first {a b c d s : ℝ} (hL : s ≤ a + d) (hU : s ≤ b + c) : weight a b c d s = Real.log ((s - c) * (s - a) / (a * c)) / s

Closed-form early branch: both moving boundaries are below their switches.

theorem G67SumCoordinate.weight_middle {a b c d s : ℝ} (hL : s ≤ a + d) (hU : b + c ≤ s) : weight a b c d s = Real.log (b * (s - a) / (a * (s - b))) / s

Closed-form middle branch for a short horizontal side.

theorem G67SumCoordinate.weight_last {a b c d s : ℝ} (hL : a + d ≤ s) (hU : b + c ≤ s) : weight a b c d s = Real.log (b * d / ((s - d) * (s - b))) / s

Closed-form late branch: both moving boundaries have crossed their switches.

theorem G67SumCoordinate.weight_left_endpoint {a b c d : ℝ} (ha : 0 < a) (hc : 0 < c) (hab : a ≤ b) (hcd : c ≤ d) : weight a b c d (a + c) = 0

Degenerate first sum fiber has exactly zero weight.

theorem G67SumCoordinate.weight_right_endpoint {a b c d : ℝ} (ha : 0 < a) (hc : 0 < c) (hab : a ≤ b) (hcd : c ≤ d) : weight a b c d (b + d) = 0

Degenerate last sum fiber has exactly zero weight.