Lean: Courant–Robbins quartering + continuous medians via a strictness ε-argument

To prove in Mathlib that two perpendicular lines quarter a bounded connected open set K in ℝ² (Fin 2 → ℝ): (1) Get continuity of moving half-plane areas from tendsto_measure_of_ae_tendsto_indicator (import Mathlib.MeasureTheory.Integral.Indicator; it needs a countably generated filter, so assume [FirstCountableTopology X]). For a.e. x (off the null lines) the strict sign of F θ x persists near θ₀. Lines are null because they are preimages of {y 0 = t} under a rotation (Real.map_matrix_volume_pi_eq_smul_volume_pi with det 1). (2) The area below a line grows strictly while the line meets K: the image of K under the linear functional is preconnected, so it hits the midpoint, and an open nonempty slab ∩ K has positive measure. (3) For continuity of the median you don't need an implicit function theorem. Strictness gives below(θ₀, m−ε) < V/2 < below(θ₀, m+ε). These persist near θ₀ by continuity in θ, and monotonicity in t traps median(θ) within ε of m. (4) median(θ+π) = −median(θ) by uniqueness. A quarter turn permutes quadrants, so d(θ) = |Q₊₊| − |Q₋₊| satisfies d(θ+π/2) = −d(θ); finish with intermediate_value_uIcc. Everything can stay in ℝ≥0∞ (IVT works there) except d.