; GraphAtlas proof SC-04
; Statement: For three buckets that each have the same correlation of 0.5 with every other, or of 0.6, and whose sums of weighted sensitivities are cut to the range of their capital, the quantity under the root of the capital of a class is never below zero and never above the square of the sum of the bucket capitals. The capital of the class is then a real number, and the diversification it gives never lifts it above the plain sum of the buckets.
; About: evaluateClass in src/kernel/sacva.ts with the cross-bucket correlations IR_GAMMA_TEXT and FX_GAMMA_TEXT, which are 0.5 and 0.6 for every pair. The cut of S to the range of K is what MAR50.53(2) prescribes. Without it neither bound holds, and with it the proof needs only the squares and products of S and K that the lemmas bound. The solver checks three buckets. For more of them the same lemmas and the same sums apply bucket by bucket, and the certified statement SC-05 covers the seven buckets of credit spread risk.
; Source: Basel Framework, MAR50, MAR50.53(2)
; Expected: unsat for each of the 17 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)
(assert (>= k_1 0.0))
(assert (>= k_2 0.0))
(assert (>= k_3 0.0))
(assert (>= s_1 (- k_1)))
(assert (<= s_1 k_1))
(assert (>= s_2 (- k_2)))
(assert (<= s_2 k_2))
(assert (>= s_3 (- k_3)))
(assert (<= s_3 k_3))

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

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

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

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

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

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

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

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

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

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

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

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

; Lemma 13, negated
(push 1)
(assert (not (let ((a!1 (+ 0.0 (* s_1 s_1) (* s_2 s_2) (* s_3 s_3) (* (+ 0.0 (* s_1 s_2) (* s_1 s_3) (* s_2 s_3)) 2.0)))) (>= a!1 0.0))))
(check-sat)
(pop 1)
; Lemma 13 holds, so later checks may use it
(assert (let ((a!1 (+ 0.0 (* s_1 s_1) (* s_2 s_2) (* s_3 s_3) (* (+ 0.0 (* s_1 s_2) (* s_1 s_3) (* s_2 s_3)) 2.0)))) (>= a!1 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) (* (/ 1.0 2.0) (+ 0.0 (* s_1 s_2) (* s_1 s_3) (* s_2 s_3)) 2.0)))) (>= a!1 0.0))))
(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 (* (/ 1.0 2.0) (+ 0.0 (* s_1 s_2) (* s_1 s_3) (* s_2 s_3)) 2.0))) (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 3, negated
(push 1)
(assert (not (let ((a!1 (+ 0.0 (* k_1 k_1) (* k_2 k_2) (* k_3 k_3) (* (/ 3.0 5.0) (+ 0.0 (* s_1 s_2) (* s_1 s_3) (* s_2 s_3)) 2.0)))) (>= a!1 0.0))))
(check-sat)
(pop 1)

; Goal 4, 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 5.0) (+ 0.0 (* s_1 s_2) (* s_1 s_3) (* s_2 s_3)) 2.0))) (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)