; GraphAtlas proof SC-03
; Statement: In an interest rate bucket of six factors, the share that rests on the CVA sensitivity of each factor, which is the CVA weighted sensitivity times the matching entry of the correlation matrix times the net weighted sensitivities, and the share that rests on its hedge, which is the weighted hedge times R times itself less that entry, add up to the quantity under the root, whatever the sensitivities are. Divided by the capital, the shares add up to it.
; About: evaluateBucket in src/kernel/sacva.ts and the shares that sacva derives from it, with the correlation matrix IR_CORRELATION_TEXT of Table 4 as exact decimals and the hedging disallowance as an exact decimal. The statement is an identity, and the solver proves that the two sides are one polynomial.
; Source: Basel Framework, MAR50, MAR50.53(1)
; Expected: unsat for each of the 1 check below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun hedge_6 () Real)
(declare-fun hedge_5 () Real)
(declare-fun hedge_4 () Real)
(declare-fun hedge_3 () Real)
(declare-fun hedge_2 () Real)
(declare-fun hedge_1 () Real)
(declare-fun cva_6 () Real)
(declare-fun cva_5 () Real)
(declare-fun cva_4 () Real)
(declare-fun cva_3 () Real)
(declare-fun cva_2 () Real)
(declare-fun cva_1 () Real)

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (+ 0.0 (* 1.0 (- cva_1 hedge_1)) (* (/ 91.0 100.0) (- cva_2 hedge_2)) (* (/ 18.0 25.0) (- cva_3 hedge_3)) (* (/ 11.0 20.0) (- cva_4 hedge_4)) (* (/ 31.0 100.0) (- cva_5 hedge_5)) (* (/ 2.0 5.0) (- cva_6 hedge_6)))) (a!2 (+ 0.0 (* (/ 91.0 100.0) (- cva_1 hedge_1)) (* 1.0 (- cva_2 hedge_2)) (* (/ 87.0 100.0) (- cva_3 hedge_3)) (* (/ 18.0 25.0) (- cva_4 hedge_4)) (* (/ 9.0 20.0) (- cva_5 hedge_5)) (* (/ 2.0 5.0) (- cva_6 hedge_6)))) (a!3 (+ 0.0 (* (/ 18.0 25.0) (- cva_1 hedge_1)) (* (/ 87.0 100.0) (- cva_2 hedge_2)) (* 1.0 (- cva_3 hedge_3)) (* (/ 91.0 100.0) (- cva_4 hedge_4)) (* (/ 17.0 25.0) (- cva_5 hedge_5)) (* (/ 2.0 5.0) (- cva_6 hedge_6)))) (a!4 (+ 0.0 (* (/ 11.0 20.0) (- cva_1 hedge_1)) (* (/ 18.0 25.0) (- cva_2 hedge_2)) (* (/ 91.0 100.0) (- cva_3 hedge_3)) (* 1.0 (- cva_4 hedge_4)) (* (/ 83.0 100.0) (- cva_5 hedge_5)) (* (/ 2.0 5.0) (- cva_6 hedge_6)))) (a!5 (+ 0.0 (* (/ 31.0 100.0) (- cva_1 hedge_1)) (* (/ 9.0 20.0) (- cva_2 hedge_2)) (* (/ 17.0 25.0) (- cva_3 hedge_3)) (* (/ 83.0 100.0) (- cva_4 hedge_4)) (* 1.0 (- cva_5 hedge_5)) (* (/ 2.0 5.0) (- cva_6 hedge_6)))) (a!6 (+ 0.0 (* (/ 2.0 5.0) (- cva_1 hedge_1)) (* (/ 2.0 5.0) (- cva_2 hedge_2)) (* (/ 2.0 5.0) (- cva_3 hedge_3)) (* (/ 2.0 5.0) (- cva_4 hedge_4)) (* (/ 2.0 5.0) (- cva_5 hedge_5)) (* 1.0 (- cva_6 hedge_6))))) (let ((a!7 (+ 0.0 (* cva_1 a!1) (* hedge_1 (- (* (/ 1.0 100.0) hedge_1) a!1)) (* cva_2 a!2) (* hedge_2 (- (* (/ 1.0 100.0) hedge_2) a!2)) (* cva_3 a!3) (* hedge_3 (- (* (/ 1.0 100.0) hedge_3) a!3)) (* cva_4 a!4) (* hedge_4 (- (* (/ 1.0 100.0) hedge_4) a!4)) (* cva_5 a!5) (* hedge_5 (- (* (/ 1.0 100.0) hedge_5) a!5)) (* cva_6 a!6) (* hedge_6 (- (* (/ 1.0 100.0) hedge_6) a!6)))) (a!8 (+ 0.0 (* (- cva_1 hedge_1) a!1) (* (- cva_2 hedge_2) a!2) (* (- cva_3 hedge_3) a!3) (* (- cva_4 hedge_4) a!4) (* (- cva_5 hedge_5) a!5) (* (- cva_6 hedge_6) a!6) (* (/ 1.0 100.0) (+ 0.0 (* hedge_1 hedge_1) (* hedge_2 hedge_2) (* hedge_3 hedge_3) (* hedge_4 hedge_4) (* hedge_5 hedge_5) (* hedge_6 hedge_6)))))) (= a!7 a!8)))))
(check-sat)
(pop 1)