Nonnegative retention implies nonnegative insurer claim

Proved

ActuarialValuation.quotaShareRetainedClaim_nonneg

by WillR · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

actuarial-scienceformal-mathematicsreinsurance

The retained loss is the product of the policyholder claim and the retained quota percentage. Nonnegative inputs make the insurer's claim nonnegative, including the zero-retention contract.

Mathematical statement

b,r\ge0\Longrightarrow R_r(b)\ge0

Preamble

import Mathlib
import Definitions.Def_actuarial_quotaShareRetainedClaim

Formal statement

namespace ActuarialValuation

theorem quotaShareRetainedClaim_nonneg (claim retention : ℝ)
  (hb : 0 ≤ claim) (hr : 0 ≤ retention) :
  0 ≤ quotaShareRetainedClaim claim retention := by sorry

end ActuarialValuation

Source

Kaluszka (2001), Optimal reinsurance under mean-variance premium principles, DOI https://doi.org/10.1016/S0167-6687(00)00066-4; Guerra and Centeno (2010), ASTIN Bulletin 40, DOI https://doi.org/10.2143/AST.40.1.2049220; explicit Bernoulli quota-share specialisation

Read-back

What the Lean code literally says, in plain math · gpt-6

Independent mathematical reading. The claim and insurer retention fraction are both assumed nonnegative, giving a nonnegative product. No upper bound on retention is required for this particular order fact, although actual admissible quota shares need one. The proposition has no stochastic or premium parameters and concerns only an event-level cashflow.

Human review

Endorsed by Shuze Chen · Oct 9, 2026
Confirmed by the moderator at approval.
Endorsed by WillR · Oct 9, 2026
Confirmed by the mission captain (proposal self-audit).

View graph