; GraphAtlas proof SM-01
; Statement: For margins of the six risk classes that are not below zero, the quantity under the root of the margin of a product class is at least the sum of the squares of the margins and at most the square of their sum. So the margin is at least the root of the sum of squares, which is what independent risk classes give, and at most the sum of the six margins.
; About: evaluate in src/kernel/simm.ts, through aggregate in src/kernel/aggregate.ts, with PSI_TEXT as exact decimals. Every entry of the table is between 0 and 1, so each term of the form differs from the plain one by a product of two margins times a number between 0 and 2, and the products are not below zero. The lemmas state the products and the solver adds them up.
; Source: ISDA SIMM Methodology, version 2.8+2512, paragraph 6
; Expected: unsat for each of the 17 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun interest_rate_margin () Real)
(declare-fun credit_qualifying_margin () Real)
(declare-fun credit_non_qualifying_margin () Real)
(declare-fun equity_margin () Real)
(declare-fun commodity_margin () Real)
(declare-fun fx_margin () Real)
(assert (>= interest_rate_margin 0.0))
(assert (>= credit_qualifying_margin 0.0))
(assert (>= credit_non_qualifying_margin 0.0))
(assert (>= equity_margin 0.0))
(assert (>= commodity_margin 0.0))
(assert (>= fx_margin 0.0))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (* credit_qualifying_margin (+ (+ 0.0 (* (/ 1.0 10.0) interest_rate_margin)) (* 1.0 credit_qualifying_margin) (* (/ 1.0 2.0) credit_non_qualifying_margin) (* (/ 1.0 2.0) equity_margin) (* (/ 1.0 5.0) commodity_margin) (* (/ 1.0 5.0) fx_margin)))) (a!2 (+ (+ (+ 0.0 (* (/ 1.0 10.0) interest_rate_margin)) (* (/ 1.0 2.0) credit_qualifying_margin)) (* 1.0 credit_non_qualifying_margin) (* (/ 2.0 5.0) equity_margin) (* (/ 1.0 5.0) commodity_margin) (* (/ 3.0 20.0) fx_margin))) (a!3 (+ (+ (+ 0.0 (* (/ 1.0 10.0) interest_rate_margin)) (* (/ 1.0 2.0) credit_qualifying_margin)) (* (/ 2.0 5.0) credit_non_qualifying_margin) (* 1.0 equity_margin) (* (/ 1.0 4.0) commodity_margin) (* (/ 3.0 10.0) fx_margin))) (a!4 (* fx_margin (+ (+ 0.0 (* (/ 1.0 10.0) interest_rate_margin)) (* (/ 1.0 5.0) credit_qualifying_margin) (* (/ 3.0 20.0) credit_non_qualifying_margin) (* (/ 3.0 10.0) equity_margin) (* (/ 1.0 4.0) commodity_margin) (* 1.0 fx_margin))))) (let ((a!5 (+ 0.0 (* interest_rate_margin (+ 0.0 (* 1.0 interest_rate_margin) (* (/ 1.0 10.0) credit_qualifying_margin) (* (/ 1.0 10.0) credit_non_qualifying_margin) (* (/ 1.0 10.0) equity_margin) (* (/ 1.0 5.0) commodity_margin) (* (/ 1.0 10.0) fx_margin))) a!1 (* credit_non_qualifying_margin a!2) (* equity_margin a!3) (* commodity_margin (+ 0.0 (* (/ 1.0 5.0) interest_rate_margin) (* (/ 1.0 5.0) credit_qualifying_margin) (* (/ 1.0 5.0) credit_non_qualifying_margin) (* (/ 1.0 4.0) equity_margin) (* 1.0 commodity_margin) (* (/ 1.0 4.0) fx_margin))) a!4))) (<= (+ 0.0 (* interest_rate_margin interest_rate_margin) (* credit_qualifying_margin credit_qualifying_margin) (* credit_non_qualifying_margin credit_non_qualifying_margin) (* equity_margin equity_margin) (* commodity_margin commodity_margin) (* fx_margin fx_margin)) a!5)))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (let ((a!1 (* credit_qualifying_margin (+ (+ 0.0 (* (/ 1.0 10.0) interest_rate_margin)) (* 1.0 credit_qualifying_margin) (* (/ 1.0 2.0) credit_non_qualifying_margin) (* (/ 1.0 2.0) equity_margin) (* (/ 1.0 5.0) commodity_margin) (* (/ 1.0 5.0) fx_margin)))) (a!2 (+ (+ (+ 0.0 (* (/ 1.0 10.0) interest_rate_margin)) (* (/ 1.0 2.0) credit_qualifying_margin)) (* 1.0 credit_non_qualifying_margin) (* (/ 2.0 5.0) equity_margin) (* (/ 1.0 5.0) commodity_margin) (* (/ 3.0 20.0) fx_margin))) (a!3 (+ (+ (+ 0.0 (* (/ 1.0 10.0) interest_rate_margin)) (* (/ 1.0 2.0) credit_qualifying_margin)) (* (/ 2.0 5.0) credit_non_qualifying_margin) (* 1.0 equity_margin) (* (/ 1.0 4.0) commodity_margin) (* (/ 3.0 10.0) fx_margin))) (a!4 (* fx_margin (+ (+ 0.0 (* (/ 1.0 10.0) interest_rate_margin)) (* (/ 1.0 5.0) credit_qualifying_margin) (* (/ 3.0 20.0) credit_non_qualifying_margin) (* (/ 3.0 10.0) equity_margin) (* (/ 1.0 4.0) commodity_margin) (* 1.0 fx_margin)))) (a!6 (+ 0.0 (* interest_rate_margin interest_rate_margin) (* credit_qualifying_margin credit_qualifying_margin) (* credit_non_qualifying_margin credit_non_qualifying_margin) (* equity_margin equity_margin) (* commodity_margin commodity_margin) (* fx_margin fx_margin) (* (+ 0.0 (* interest_rate_margin credit_qualifying_margin) (* interest_rate_margin credit_non_qualifying_margin) (* interest_rate_margin equity_margin) (* interest_rate_margin commodity_margin) (* interest_rate_margin fx_margin) (* credit_qualifying_margin credit_non_qualifying_margin) (* credit_qualifying_margin equity_margin) (* credit_qualifying_margin commodity_margin) (* credit_qualifying_margin fx_margin) (* credit_non_qualifying_margin equity_margin) (* credit_non_qualifying_margin commodity_margin) (* credit_non_qualifying_margin fx_margin) (* equity_margin commodity_margin) (* equity_margin fx_margin) (* commodity_margin fx_margin)) 2.0)))) (let ((a!5 (+ 0.0 (* interest_rate_margin (+ 0.0 (* 1.0 interest_rate_margin) (* (/ 1.0 10.0) credit_qualifying_margin) (* (/ 1.0 10.0) credit_non_qualifying_margin) (* (/ 1.0 10.0) equity_margin) (* (/ 1.0 5.0) commodity_margin) (* (/ 1.0 10.0) fx_margin))) a!1 (* credit_non_qualifying_margin a!2) (* equity_margin a!3) (* commodity_margin (+ 0.0 (* (/ 1.0 5.0) interest_rate_margin) (* (/ 1.0 5.0) credit_qualifying_margin) (* (/ 1.0 5.0) credit_non_qualifying_margin) (* (/ 1.0 4.0) equity_margin) (* 1.0 commodity_margin) (* (/ 1.0 4.0) fx_margin))) a!4))) (<= a!5 a!6)))))
(check-sat)
(pop 1)