; GraphAtlas proof SM-05
; Statement: For three buckets with the cross-bucket correlation of 3/10, any clipped sums within their K and any ratios of the concentration factors between 0 and 1, the quantity under the root of a risk class is at most the square of the sum of the bucket margins and at least 2/5 of the sum of their squares. So the cross-bucket aggregation never adds to the plain sum, the quantity is never below zero, and the floor in the engine is not reached.
; About: evaluateRisk in src/kernel/simm.ts, with IR_GAMMA_TEXT as an exact decimal. The quantity under the root is the sum of the K^2 plus twice the sum, over the three pairs of buckets, of gamma times the ratio of the concentration factors times the product of the two clipped sums. The ratio is between 0 and 1 because it is a smaller over a larger, and each clipped sum is within K. The lemmas bound each product, and the solver adds them up. Four buckets or more are not in the proof, and the tests check that the quantity is never below zero for random books with many.
; Source: ISDA SIMM Methodology, version 2.8+2512, paragraph 7(d)
; Expected: unsat for each of the 23 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun k_1 () Real)
(declare-fun k_2 () Real)
(declare-fun k_3 () Real)
(declare-fun s_1 () Real)
(declare-fun s_2 () Real)
(declare-fun s_3 () Real)
(declare-fun ratio_12 () Real)
(declare-fun ratio_13 () Real)
(declare-fun ratio_23 () Real)
(assert (>= k_1 0.0))
(assert (>= k_2 0.0))
(assert (>= k_3 0.0))
(assert (and (>= s_1 (* (- 1.0) k_1)) (<= s_1 (* 1.0 k_1))))
(assert (and (>= s_2 (* (- 1.0) k_2)) (<= s_2 (* 1.0 k_2))))
(assert (and (>= s_3 (* (- 1.0) k_3)) (<= s_3 (* 1.0 k_3))))
(assert (and (>= ratio_12 0.0) (<= ratio_12 1.0)))
(assert (and (>= ratio_13 0.0) (<= ratio_13 1.0)))
(assert (and (>= ratio_23 0.0) (<= ratio_23 1.0)))

; Lemma 1, negated
(push 1)
(assert (not (<= (* s_1 s_2) (* 1.0 1.0 k_1 k_2))))
(check-sat)
(pop 1)
; Lemma 1 holds, so later checks may use it
(assert (<= (* s_1 s_2) (* 1.0 1.0 k_1 k_2)))

; Lemma 2, negated
(push 1)
(assert (not (>= (+ (* s_1 s_2) (* 1.0 1.0 k_1 k_2)) 0.0)))
(check-sat)
(pop 1)
; Lemma 2 holds, so later checks may use it
(assert (>= (+ (* s_1 s_2) (* 1.0 1.0 k_1 k_2)) 0.0))

; Lemma 3, negated
(push 1)
(assert (not (>= (* ratio_12 (- (* 1.0 1.0 k_1 k_2) (* s_1 s_2))) 0.0)))
(check-sat)
(pop 1)
; Lemma 3 holds, so later checks may use it
(assert (>= (* ratio_12 (- (* 1.0 1.0 k_1 k_2) (* s_1 s_2))) 0.0))

; Lemma 4, negated
(push 1)
(assert (not (>= (* ratio_12 (+ (* 1.0 1.0 k_1 k_2) (* s_1 s_2))) 0.0)))
(check-sat)
(pop 1)
; Lemma 4 holds, so later checks may use it
(assert (>= (* ratio_12 (+ (* 1.0 1.0 k_1 k_2) (* s_1 s_2))) 0.0))

; Lemma 5, negated
(push 1)
(assert (not (>= (* (- 1.0 ratio_12) k_1 k_2) 0.0)))
(check-sat)
(pop 1)
; Lemma 5 holds, so later checks may use it
(assert (>= (* (- 1.0 ratio_12) k_1 k_2) 0.0))

; Lemma 6, negated
(push 1)
(assert (not (>= (* k_1 k_2) 0.0)))
(check-sat)
(pop 1)
; Lemma 6 holds, so later checks may use it
(assert (>= (* k_1 k_2) 0.0))

; Lemma 7, negated
(push 1)
(assert (not (>= (* (- k_1 k_2) (- k_1 k_2)) 0.0)))
(check-sat)
(pop 1)
; Lemma 7 holds, so later checks may use it
(assert (>= (* (- k_1 k_2) (- k_1 k_2)) 0.0))

; Lemma 8, negated
(push 1)
(assert (not (<= (* s_1 s_3) (* 1.0 1.0 k_1 k_3))))
(check-sat)
(pop 1)
; Lemma 8 holds, so later checks may use it
(assert (<= (* s_1 s_3) (* 1.0 1.0 k_1 k_3)))

; Lemma 9, negated
(push 1)
(assert (not (>= (+ (* s_1 s_3) (* 1.0 1.0 k_1 k_3)) 0.0)))
(check-sat)
(pop 1)
; Lemma 9 holds, so later checks may use it
(assert (>= (+ (* s_1 s_3) (* 1.0 1.0 k_1 k_3)) 0.0))

; Lemma 10, negated
(push 1)
(assert (not (>= (* ratio_13 (- (* 1.0 1.0 k_1 k_3) (* s_1 s_3))) 0.0)))
(check-sat)
(pop 1)
; Lemma 10 holds, so later checks may use it
(assert (>= (* ratio_13 (- (* 1.0 1.0 k_1 k_3) (* s_1 s_3))) 0.0))

; Lemma 11, negated
(push 1)
(assert (not (>= (* ratio_13 (+ (* 1.0 1.0 k_1 k_3) (* s_1 s_3))) 0.0)))
(check-sat)
(pop 1)
; Lemma 11 holds, so later checks may use it
(assert (>= (* ratio_13 (+ (* 1.0 1.0 k_1 k_3) (* s_1 s_3))) 0.0))

; Lemma 12, negated
(push 1)
(assert (not (>= (* (- 1.0 ratio_13) k_1 k_3) 0.0)))
(check-sat)
(pop 1)
; Lemma 12 holds, so later checks may use it
(assert (>= (* (- 1.0 ratio_13) k_1 k_3) 0.0))

; Lemma 13, negated
(push 1)
(assert (not (>= (* k_1 k_3) 0.0)))
(check-sat)
(pop 1)
; Lemma 13 holds, so later checks may use it
(assert (>= (* k_1 k_3) 0.0))

; Lemma 14, negated
(push 1)
(assert (not (>= (* (- k_1 k_3) (- k_1 k_3)) 0.0)))
(check-sat)
(pop 1)
; Lemma 14 holds, so later checks may use it
(assert (>= (* (- k_1 k_3) (- k_1 k_3)) 0.0))

; Lemma 15, negated
(push 1)
(assert (not (<= (* s_2 s_3) (* 1.0 1.0 k_2 k_3))))
(check-sat)
(pop 1)
; Lemma 15 holds, so later checks may use it
(assert (<= (* s_2 s_3) (* 1.0 1.0 k_2 k_3)))

; Lemma 16, negated
(push 1)
(assert (not (>= (+ (* s_2 s_3) (* 1.0 1.0 k_2 k_3)) 0.0)))
(check-sat)
(pop 1)
; Lemma 16 holds, so later checks may use it
(assert (>= (+ (* s_2 s_3) (* 1.0 1.0 k_2 k_3)) 0.0))

; Lemma 17, negated
(push 1)
(assert (not (>= (* ratio_23 (- (* 1.0 1.0 k_2 k_3) (* s_2 s_3))) 0.0)))
(check-sat)
(pop 1)
; Lemma 17 holds, so later checks may use it
(assert (>= (* ratio_23 (- (* 1.0 1.0 k_2 k_3) (* s_2 s_3))) 0.0))

; Lemma 18, negated
(push 1)
(assert (not (>= (* ratio_23 (+ (* 1.0 1.0 k_2 k_3) (* s_2 s_3))) 0.0)))
(check-sat)
(pop 1)
; Lemma 18 holds, so later checks may use it
(assert (>= (* ratio_23 (+ (* 1.0 1.0 k_2 k_3) (* s_2 s_3))) 0.0))

; Lemma 19, negated
(push 1)
(assert (not (>= (* (- 1.0 ratio_23) k_2 k_3) 0.0)))
(check-sat)
(pop 1)
; Lemma 19 holds, so later checks may use it
(assert (>= (* (- 1.0 ratio_23) k_2 k_3) 0.0))

; Lemma 20, negated
(push 1)
(assert (not (>= (* k_2 k_3) 0.0)))
(check-sat)
(pop 1)
; Lemma 20 holds, so later checks may use it
(assert (>= (* k_2 k_3) 0.0))

; Lemma 21, negated
(push 1)
(assert (not (>= (* (- k_2 k_3) (- k_2 k_3)) 0.0)))
(check-sat)
(pop 1)
; Lemma 21 holds, so later checks may use it
(assert (>= (* (- k_2 k_3) (- k_2 k_3)) 0.0))

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (+ 0.0 (* k_1 k_1) (* k_2 k_2) (* k_3 k_3)))) (let ((a!2 (+ a!1 (* (/ 3.0 10.0) 2.0 (+ 0.0 (* ratio_12 s_1 s_2) (* ratio_13 s_1 s_3) (* ratio_23 s_2 s_3))))) (a!3 (+ a!1 (* (+ 0.0 (* k_1 k_2) (* k_1 k_3) (* k_2 k_3)) 2.0)))) (<= a!2 a!3)))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (let ((a!1 (+ 0.0 (* k_1 k_1) (* k_2 k_2) (* k_3 k_3)))) (let ((a!2 (+ a!1 (* (/ 3.0 10.0) 2.0 (+ 0.0 (* ratio_12 s_1 s_2) (* ratio_13 s_1 s_3) (* ratio_23 s_2 s_3)))))) (>= a!2 (* (/ 2.0 5.0) a!1))))))
(check-sat)
(pop 1)