; GraphAtlas proof SC-02
; Statement: With the hedges of the previous statement, a ratio of hedging above zero and below 2 x Q / (Q + R x N) lowers the quantity under the root of the capital of a bucket, that ratio leaves it where it was with no hedge, and a ratio above it or below zero raises it. With the disallowance of 0.01 and a single factor, a hedge of more than 198 per cent of the exposure costs more capital than no hedge.
; About: evaluateBucket in src/kernel/sacva.ts for hedges in one proportion of the CVA sensitivities. The quantity under the root less its value with no hedge is ratio x ((Q + R x N) x ratio - 2 x Q), so its sign is that of the ratio times the sign of the ratio less 2 x Q / (Q + R x N). For one factor Q and N are equal and the edge is 2 / (1 + R), which is 1.98 for the disallowance of 0.01.
; Source: Basel Framework, MAR50, MAR50.52 and MAR50.53(1)
; Expected: unsat for each of the 4 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun cva_form () Real)
(declare-fun cva_squares () Real)
(declare-fun hedge_ratio () Real)
(assert (> cva_form 0.0))
(assert (> cva_squares 0.0))

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (< hedge_ratio (/ (* 2.0 cva_form) (+ cva_form (* (/ 1.0 100.0) cva_squares))))) (a!2 (< (+ (* (- 1.0 hedge_ratio) (- 1.0 hedge_ratio) cva_form) (* (/ 1.0 100.0) hedge_ratio hedge_ratio cva_squares)) (+ (* (- 1.0 0.0) (- 1.0 0.0) cva_form) (* (/ 1.0 100.0) 0.0 0.0 cva_squares))))) (=> (and (> hedge_ratio 0.0) a!1) a!2))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (let ((a!1 (- 1.0 (/ (* 2.0 cva_form) (+ cva_form (* (/ 1.0 100.0) cva_squares))))) (a!2 (* (/ 1.0 100.0) (/ (* 2.0 cva_form) (+ cva_form (* (/ 1.0 100.0) cva_squares))) (/ (* 2.0 cva_form) (+ cva_form (* (/ 1.0 100.0) cva_squares))) cva_squares))) (= (+ (* a!1 a!1 cva_form) a!2) (+ (* (- 1.0 0.0) (- 1.0 0.0) cva_form) (* (/ 1.0 100.0) 0.0 0.0 cva_squares))))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (let ((a!1 (> hedge_ratio (/ (* 2.0 cva_form) (+ cva_form (* (/ 1.0 100.0) cva_squares))))) (a!2 (> (+ (* (- 1.0 hedge_ratio) (- 1.0 hedge_ratio) cva_form) (* (/ 1.0 100.0) hedge_ratio hedge_ratio cva_squares)) (+ (* (- 1.0 0.0) (- 1.0 0.0) cva_form) (* (/ 1.0 100.0) 0.0 0.0 cva_squares))))) (=> a!1 a!2))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (let ((a!1 (> (+ (* (- 1.0 hedge_ratio) (- 1.0 hedge_ratio) cva_form) (* (/ 1.0 100.0) hedge_ratio hedge_ratio cva_squares)) (+ (* (- 1.0 0.0) (- 1.0 0.0) cva_form) (* (/ 1.0 100.0) 0.0 0.0 cva_squares))))) (=> (< hedge_ratio 0.0) a!1))))
(check-sat)
(pop 1)