← Mathematical handbook

Ordering across zero and the decreasing negative branch

theorem Papers.AnsariRockel2026XiRho.sourceBand_isSI (b : ℝ) (hb : 0 < b) : (sourceBand b hb).IsSI

theorem Papers.AnsariRockel2026XiRho.negativeSourceBand_isSD (b : ℝ) (hb : 0 < b) : (negativeSourceBand b hb).IsSD

theorem Papers.AnsariRockel2026XiRho.sourceBand_independence_order (b : ℝ) (hb : 0 < b) (u v : ↑unitInterval) : ↑u * ↑v ≤ (sourceBand b hb).cdf ![u, v]

theorem Papers.AnsariRockel2026XiRho.negativeSourceBand_independence_order (b : ℝ) (hb : 0 < b) (u v : ↑unitInterval) : (negativeSourceBand b hb).cdf ![u, v] ≤ ↑u * ↑v

theorem Papers.AnsariRockel2026XiRho.sourceBand_cross_sign_order (b d : ℝ) (hb : 0 < b) (hd : 0 < d) (u v : ↑unitInterval) : (negativeSourceBand b hb).cdf ![u, v] ≤ (sourceBand d hd).cdf ![u, v]

This supplies the cross-zero case missing from same-sign parameter ordering.

theorem Papers.AnsariRockel2026XiRho.negativeSourceBand_conditionalCDF (b : ℝ) (hb : 0 < b) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (negativeSourceBand b hb).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => Verification.unitClamp (sourceBandIntercept b v - b * (1 - ↑u))

Remark 3(c): explicit clamped conditional sections of the negative branch.