; GraphAtlas proof SM-02
; Statement: The concentration factor is never below one and is one up to the threshold. Above it, its square times the threshold is the exposure, so the margin of a lone factor grows with the exposure to the power 3/2. It rises with the exposure, so more exposure never lowers a weighted sensitivity, and it depends only on the exposure over the threshold, so the unit of both does not matter.
; About: concentrationFactor in src/kernel/simm.ts, which is the larger of 1 and the root of the absolute exposure over the threshold. The proof takes the absolute exposure as a number x from zero up, the threshold as a number above zero, and the root as a number r from zero up with r^2 x threshold = x, so it states the root by its square. The weighted exposure of a lone factor is its weight times the factor times the exposure.
; Source: ISDA SIMM Methodology, version 2.8+2512, paragraphs 7(b) and 8(b)
; Expected: unsat for each of the 6 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun root () Real)
(declare-fun exposure () Real)
(declare-fun threshold () Real)
(declare-fun weight () Real)
(declare-fun larger_root () Real)
(declare-fun larger_exposure () Real)
(declare-fun scaled_root () Real)
(declare-fun unit () Real)

; Goal 1, negated
(push 1)
(assert (not (=> (and (>= exposure 0.0) (> threshold 0.0) (>= root 0.0) (= (* root root threshold) exposure)) (>= (ite (>= 1.0 root) 1.0 root) 1.0))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (=> (and (>= exposure 0.0) (> threshold 0.0) (>= root 0.0) (= (* root root threshold) exposure) (<= exposure threshold)) (= (ite (>= 1.0 root) 1.0 root) 1.0))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (let ((a!1 (= (* (ite (>= 1.0 root) 1.0 root) (ite (>= 1.0 root) 1.0 root) threshold) exposure))) (=> (and (>= exposure 0.0) (> threshold 0.0) (>= root 0.0) (= (* root root threshold) exposure) (> exposure threshold)) a!1))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (let ((a!1 (* (* weight (ite (>= 1.0 root) 1.0 root) exposure) (* weight (ite (>= 1.0 root) 1.0 root) exposure) threshold))) (=> (and (>= exposure 0.0) (> threshold 0.0) (>= root 0.0) (= (* root root threshold) exposure) (>= weight 0.0) (> exposure threshold)) (= a!1 (* weight weight exposure exposure exposure))))))
(check-sat)
(pop 1)

; Goal 5, negated
(push 1)
(assert (not (let ((a!1 (<= (* exposure (ite (>= 1.0 root) 1.0 root)) (* larger_exposure (ite (>= 1.0 larger_root) 1.0 larger_root))))) (let ((a!2 (and (<= (ite (>= 1.0 root) 1.0 root) (ite (>= 1.0 larger_root) 1.0 larger_root)) a!1))) (=> (and (>= exposure 0.0) (> threshold 0.0) (>= root 0.0) (= (* root root threshold) exposure) (>= larger_exposure exposure) (>= larger_root 0.0) (= (* larger_root larger_root threshold) larger_exposure)) a!2)))))
(check-sat)
(pop 1)

; Goal 6, negated
(push 1)
(assert (not (=> (and (>= exposure 0.0) (> threshold 0.0) (>= root 0.0) (= (* root root threshold) exposure) (> unit 0.0) (>= scaled_root 0.0) (= (* scaled_root scaled_root threshold unit) (* exposure unit))) (= (ite (>= 1.0 scaled_root) 1.0 scaled_root) (ite (>= 1.0 root) 1.0 root)))))
(check-sat)
(pop 1)