; GraphAtlas proof SC-01
; Statement: When the hedges of a bucket offset every one of its risk factors in the same proportion, the quantity under the root of its capital is (1 - ratio)^2 x Q + R x ratio^2 x N, where Q is the form of the CVA weighted sensitivities through the correlation matrix, N is the sum of their squares and R is the hedging disallowance of 0.01. No ratio takes it below R x Q x N / (Q + R x N), the ratio Q / (Q + R x N) reaches that value, and so the capital of a bucket with a position is never zero.
; About: evaluateBucket in src/kernel/sacva.ts, with the hedging disallowance HEDGING_DISALLOWANCE_TEXT as an exact decimal. The net weighted sensitivity of a factor is the CVA one less the hedge, and with a hedge of ratio times the CVA one it is (1 - ratio) times it. The first two terms of MAR50.53(1) then give (1 - ratio)^2 Q and the third gives R x ratio^2 x N. The proof multiplies the quantity by Q + R x N so that it needs no division, and the key step is that the difference from R x Q x N is the square ((1 - ratio) x Q - R x ratio x N)^2.
; Source: Basel Framework, MAR50, MAR50.53(1)
; Expected: unsat for each of the 3 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 (* (+ cva_form (* (/ 1.0 100.0) cva_squares)) (+ (* (- 1.0 hedge_ratio) (- 1.0 hedge_ratio) cva_form) (* (/ 1.0 100.0) hedge_ratio hedge_ratio cva_squares))))) (>= a!1 (* 1.0 (/ 1.0 100.0) cva_form cva_squares)))))
(check-sat)
(pop 1)

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

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