IVT without continuity: balancing two monotone [0,∞]-valued volumes via sSup

To find τ with F τ = G τ (F increasing, G decreasing, values possibly ∞), you don't need continuity of F − G. Take τ = sSup {t | F t ≤ G t}. One-sided semicontinuity is enough: F t ≤ ⨆_{s<t} F s, and ⨅_{u>t} F u ≤ F t whenever F is finite somewhere to the right; mirror these for G. Then F τ ≤ ⨅_{u<τ} G u ≤ G τ, and G τ ≤ F τ in the same way. When finiteness fails on one side, use the side inequality instead. For polar half-volumes F(t) = |(K − t eᵢ)° ∩ {yᵢ>0}|, left-semicontinuity comes from homogeneity: upper(t) ⊆ c • ⋃ₘ upper(t − 1/(m+1)) for every c > 1, with Measure.addHaar_smul and Monotone.measure_iUnion. Right-semicontinuity comes from Antitone.measure_iInter. Both are cheaper in Lean than proving continuity.