; GraphAtlas proof SM-04
; Statement: The parts of a product class add up to its margin. In a risk class, the parts of the regular buckets add up to the quantity under the root over the root, which is the core margin, and the residual bucket gives its own margin. The parts of the six risk classes, each the margin times the weighted margin over the total, add up to the total, which is the Euler identity of the table between risk classes.
; About: evaluate in src/kernel/simm.ts. A bucket that is not residual has the derivative own = 1 over the core margin and the residual bucket has own = 1 over its K, and a risk class has the factor scale = weighted margin over the total of its product class. Steps one and two say that the parts of the buckets, each K^2 + S x C by SM-03 times own, add up to the core margin and to the residual margin. Step three adds them in a risk class. Step four is the identity of the table PSI_TEXT as exact decimals, and steps five and six are the loop over the six risk classes, which keeps the sum of the parts equal to the inverse of the total times the sum of the products. Division is written as a multiplication by an inverse that has the inverse times the number equal to 1.
; Source: ISDA SIMM Methodology, version 2.8+2512, paragraphs 6, 7(d) and 8(d)
; Expected: unsat for each of the 6 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun core () Real)
(declare-fun radicand () Real)
(declare-fun own () Real)
(declare-fun k () Real)
(declare-fun q () Real)
(declare-fun own_residual () Real)
(declare-fun delta () Real)
(declare-fun scale () Real)
(declare-fun fx_margin () Real)
(declare-fun commodity_margin () Real)
(declare-fun equity_margin () Real)
(declare-fun credit_non_qualifying_margin () Real)
(declare-fun credit_qualifying_margin () Real)
(declare-fun interest_rate_margin () Real)
(declare-fun margin () Real)
(declare-fun weighted_margin () Real)
(declare-fun products_so_far () Real)
(declare-fun inverse_of_total () Real)
(declare-fun parts_so_far () Real)
(declare-fun total () Real)
(declare-fun undiversified () Real)

; Goal 1, negated
(push 1)
(assert (not (=> (and (> core 0.0) (= (* own core) (to_real 1)) (= radicand (* core core))) (= (* own radicand) core))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (=> (and (>= core 0.0) (> k 0.0) (= (* own_residual k) (to_real 1)) (= q (* k k))) (= (* own_residual q) k))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (let ((a!1 (= (* scale (+ (* own radicand) (* own_residual q))) (* scale delta)))) (=> (and (>= core 0.0) (>= k 0.0) (>= scale 0.0) (>= own 0.0) (>= own_residual 0.0) (>= radicand 0.0) (>= q 0.0) (= (* own radicand) core) (= (* own_residual q) k) (= delta (+ core k))) a!1))))
(check-sat)
(pop 1)

; Goal 4, 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))) (=> (and (>= interest_rate_margin 0.0) (>= credit_qualifying_margin 0.0) (>= credit_non_qualifying_margin 0.0) (>= equity_margin 0.0) (>= commodity_margin 0.0) (>= fx_margin 0.0)) (= a!5 a!5))))))
(check-sat)
(pop 1)

; Goal 5, negated
(push 1)
(assert (not (let ((a!1 (= (+ parts_so_far (* weighted_margin inverse_of_total margin)) (* inverse_of_total (+ products_so_far (* weighted_margin margin)))))) (=> (= parts_so_far (* inverse_of_total products_so_far)) a!1))))
(check-sat)
(pop 1)

; Goal 6, negated
(push 1)
(assert (not (=> (and (> total 0.0) (>= undiversified total) (= (* inverse_of_total total) (to_real 1)) (= products_so_far (* total total)) (= parts_so_far (* inverse_of_total products_so_far))) (= parts_so_far total))))
(check-sat)
(pop 1)