theorem Actus.Contract.Properties.pam_stf_sd {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (e : Protocol.EventType) (t : Protocol.Time) (s : State α) : (PAM.stf ct rf e t s).sd = t

theorem Actus.Contract.Properties.lam_stf_sd {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (e : Protocol.EventType) (t : Protocol.Time) (s : State α) : (LAM.stf ct rf e t s).sd = t

theorem Actus.Contract.Properties.nam_stf_sd {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (e : Protocol.EventType) (t : Protocol.Time) (s : State α) : (NAM.stf ct rf e t s).sd = t

theorem Actus.Contract.Properties.ann_stf_sd {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (e : Protocol.EventType) (t : Protocol.Time) (s : State α) : (ANN.stf ct rf e t s).sd = t

theorem Actus.Contract.Properties.pam_step_mono {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (h : s ↝[ct, rf] s') : s.sd ≤ s'.sd

theorem Actus.Contract.Properties.lam_step_mono {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (h : LAM.Step ct rf s s') : s.sd ≤ s'.sd

theorem Actus.Contract.Properties.nam_step_mono {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (h : NAM.Step ct rf s s') : s.sd ≤ s'.sd

theorem Actus.Contract.Properties.ann_step_mono {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (h : ANN.Step ct rf s s') : s.sd ≤ s'.sd

theorem Actus.Contract.Properties.pam_trace_mono {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (tr : PAM.Trace ct rf s s') : s.sd ≤ s'.sd

theorem Actus.Contract.Properties.lam_trace_mono {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (tr : LAM.Trace ct rf s s') : s.sd ≤ s'.sd

theorem Actus.Contract.Properties.nam_trace_mono {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (tr : NAM.Trace ct rf s s') : s.sd ≤ s'.sd

theorem Actus.Contract.Properties.ann_trace_mono {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (tr : ANN.Trace ct rf s s') : s.sd ≤ s'.sd

theorem Actus.Contract.Properties.pam_md_nt {α : Type} [Amount α] [DecidableLE α] (t : Protocol.Time) (s : State α) : (PAM.stf_MD t s).nt = 0

theorem Actus.Contract.Properties.pam_md_ipac {α : Type} [Amount α] [DecidableLE α] (t : Protocol.Time) (s : State α) : (PAM.stf_MD t s).ipac = 0

theorem Actus.Contract.Properties.pam_md_feac {α : Type} [Amount α] [DecidableLE α] (t : Protocol.Time) (s : State α) : (PAM.stf_MD t s).feac = 0

theorem Actus.Contract.Properties.pam_td_nt {α : Type} [Amount α] [DecidableLE α] (t : Protocol.Time) (s : State α) : (PAM.stf_TD t s).nt = 0

theorem Actus.Contract.Properties.pam_td_ipac {α : Type} [Amount α] [DecidableLE α] (t : Protocol.Time) (s : State α) : (PAM.stf_TD t s).ipac = 0

theorem Actus.Contract.Properties.pam_td_ipnr {α : Type} [Amount α] [DecidableLE α] (t : Protocol.Time) (s : State α) : (PAM.stf_TD t s).ipnr = 0

theorem Actus.Contract.Properties.pam_td_feac {α : Type} [Amount α] [DecidableLE α] (t : Protocol.Time) (s : State α) : (PAM.stf_TD t s).feac = 0

theorem Actus.Contract.Properties.pam_md_step_zero {α : Type} [Amount α] [DecidableLE α] {t : Protocol.Time} {s s' : State α} (he : s' = PAM.stf_MD t s) : s'.nt = 0

The maturity event of a trace step zeroes the notional.

theorem Actus.Contract.Properties.pam_ied_nt {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} (t : Protocol.Time) (s : State α) : (PAM.stf_IED ct t s).nt = Util.Conventions.sign ct.cntrl * ct.nt

theorem Actus.Contract.Properties.lam_step_det {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s₁ s₂ : State α} {e : Protocol.EventType} {t : Protocol.Time} (he₁ : s₁ = LAM.stf ct rf e t s) (he₂ : s₂ = LAM.stf ct rf e t s) : s₁ = s₂

Determinism, as a corollary of relational↔functional agreement: any two LAM steps out of s on the functional image of the same event and time coincide. (Step is the graph of the function stf.)

theorem Actus.Contract.Properties.pam_stf_md {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (e : Protocol.EventType) (t : Protocol.Time) (s : State α) : (PAM.stf ct rf e t s).md = s.md

theorem Actus.Contract.Properties.lam_stf_md {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (e : Protocol.EventType) (t : Protocol.Time) (s : State α) : (LAM.stf ct rf e t s).md = s.md

theorem Actus.Contract.Properties.nam_stf_md {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (e : Protocol.EventType) (t : Protocol.Time) (s : State α) : (NAM.stf ct rf e t s).md = s.md

theorem Actus.Contract.Properties.ann_stf_md {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (e : Protocol.EventType) (t : Protocol.Time) (s : State α) : (ANN.stf ct rf e t s).md = s.md

theorem Actus.Contract.Properties.pam_trace_md {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (tr : PAM.Trace ct rf s s') : s'.md = s.md

The maturity date is therefore constant along any execution trace.

theorem Actus.Contract.Properties.lam_trace_md {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (tr : LAM.Trace ct rf s s') : s'.md = s.md

theorem Actus.Contract.Properties.nam_trace_md {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (tr : NAM.Trace ct rf s s') : s'.md = s.md

theorem Actus.Contract.Properties.ann_trace_md {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (tr : ANN.Trace ct rf s s') : s'.md = s.md

theorem Actus.Contract.Properties.pam_stf_prf {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (e : Protocol.EventType) (t : Protocol.Time) (s : State α) : (PAM.stf ct rf e t s).prf = s.prf

theorem Actus.Contract.Properties.lam_stf_prf {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (e : Protocol.EventType) (t : Protocol.Time) (s : State α) : (LAM.stf ct rf e t s).prf = s.prf

theorem Actus.Contract.Properties.nam_stf_prf {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (e : Protocol.EventType) (t : Protocol.Time) (s : State α) : (NAM.stf ct rf e t s).prf = s.prf

theorem Actus.Contract.Properties.ann_stf_prf {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (e : Protocol.EventType) (t : Protocol.Time) (s : State α) : (ANN.stf ct rf e t s).prf = s.prf

theorem Actus.Contract.Properties.pam_pd_clock {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (t : Protocol.Time) (s : State α) : PAM.stf ct rf Protocol.EventType.PD t s = { md := s.md, nt := s.nt, ipnr := s.ipnr, ipac := s.ipac, feac := s.feac, nsc := s.nsc, isc := s.isc, prnxt := s.prnxt, ipcb := s.ipcb, prf := s.prf, sd := t }

theorem Actus.Contract.Properties.pam_dv_clock {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (t : Protocol.Time) (s : State α) : PAM.stf ct rf Protocol.EventType.DV t s = { md := s.md, nt := s.nt, ipnr := s.ipnr, ipac := s.ipac, feac := s.feac, nsc := s.nsc, isc := s.isc, prnxt := s.prnxt, ipcb := s.ipcb, prf := s.prf, sd := t }

theorem Actus.Contract.Properties.pam_std_clock {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (t : Protocol.Time) (s : State α) : PAM.stf ct rf Protocol.EventType.STD t s = { md := s.md, nt := s.nt, ipnr := s.ipnr, ipac := s.ipac, feac := s.feac, nsc := s.nsc, isc := s.isc, prnxt := s.prnxt, ipcb := s.ipcb, prf := s.prf, sd := t }

theorem Actus.Contract.Properties.pam_xd_clock {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (t : Protocol.Time) (s : State α) : PAM.stf ct rf Protocol.EventType.XD t s = { md := s.md, nt := s.nt, ipnr := s.ipnr, ipac := s.ipac, feac := s.feac, nsc := s.nsc, isc := s.isc, prnxt := s.prnxt, ipcb := s.ipcb, prf := s.prf, sd := t }

theorem Actus.Contract.Properties.pam_sc_ooo_inert {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (t : Protocol.Time) (s : State α) (h : ct.scief = Protocol.ScalingEffect.SE_OOO) : (PAM.stf_SC ct rf t s).nsc = s.nsc ∧ (PAM.stf_SC ct rf t s).isc = s.isc

def Actus.Contract.Properties.traceLen {β : Type} {r : β → β → Type} {a b : β} : Closures.Star r a b → ℕ

Number of steps in a trace (closure).

Equations

• Actus.Contract.Properties.traceLen Actus.Closures.Star.refl = 0
• Actus.Contract.Properties.traceLen (Actus.Closures.Star.step a rest) = Actus.Contract.Properties.traceLen rest + 1

theorem Actus.Contract.Properties.pam_cashflows_length {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (tr : PAM.Trace ct rf s s') : (PAM.getCashflows ct rf tr).length = traceLen tr

theorem Actus.Contract.Properties.lam_cashflows_length {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (tr : LAM.Trace ct rf s s') : (LAM.getCashflows ct rf tr).length = traceLen tr

theorem Actus.Contract.Properties.nam_cashflows_length {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (tr : NAM.Trace ct rf s s') : (NAM.getCashflows ct rf tr).length = traceLen tr

theorem Actus.Contract.Properties.ann_cashflows_length {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (tr : ANN.Trace ct rf s s') : (ANN.getCashflows ct rf tr).length = traceLen tr

theorem Actus.Contract.Properties.pam_cashflow_time {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (h : s ↝[ct, rf] s') : (PAM.getCashflow ct rf h).1.1 = s'.sd

theorem Actus.Contract.Properties.lam_cashflow_time {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (h : LAM.Step ct rf s s') : (LAM.getCashflow ct rf h).1.1 = s'.sd

theorem Actus.Contract.Properties.nam_cashflow_time {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (h : NAM.Step ct rf s s') : (NAM.getCashflow ct rf h).1.1 = s'.sd

theorem Actus.Contract.Properties.ann_cashflow_time {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (h : ANN.Step ct rf s s') : (ANN.getCashflow ct rf h).1.1 = s'.sd

theorem Actus.Contract.Properties.pam_ad_zero {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} {t : Protocol.Time} (h : s.sd ≤ t) : (PAM.getCashflow ct rf (PAM.Step.ad h)).2 = 0

theorem Actus.Contract.Properties.pam_ipci_zero {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} {t : Protocol.Time} (h : s.sd ≤ t) : (PAM.getCashflow ct rf (PAM.Step.ipci h)).2 = 0

theorem Actus.Contract.Properties.pam_rr_zero {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} {t : Protocol.Time} (h : s.sd ≤ t) : (PAM.getCashflow ct rf (PAM.Step.rr h)).2 = 0

theorem Actus.Contract.Properties.pam_rrf_zero {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} {t : Protocol.Time} (h : s.sd ≤ t) : (PAM.getCashflow ct rf (PAM.Step.rrf h)).2 = 0

theorem Actus.Contract.Properties.pam_sc_zero {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} {t : Protocol.Time} (h : s.sd ≤ t) : (PAM.getCashflow ct rf (PAM.Step.sc h)).2 = 0

theorem Actus.Contract.Properties.pam_ce_zero {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} {t : Protocol.Time} (h : s.sd ≤ t) : (PAM.getCashflow ct rf (PAM.Step.ce h)).2 = 0

theorem Actus.Contract.Properties.lam_cashflow_type {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} (e : Protocol.EventType) {t : Protocol.Time} (h : s.sd ≤ t) : (LAM.getCashflow ct rf (LAM.Step.ev e h)).1.2 = e

For the dispatching contracts, the cashflow's event type is exactly the event that produced it.

theorem Actus.Contract.Properties.nam_cashflow_type {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} (e : Protocol.EventType) {t : Protocol.Time} (h : s.sd ≤ t) : (NAM.getCashflow ct rf (NAM.Step.ev e h)).1.2 = e

theorem Actus.Contract.Properties.ann_cashflow_type {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} (e : Protocol.EventType) {t : Protocol.Time} (h : s.sd ≤ t) : (ANN.getCashflow ct rf (ANN.Step.ev e h)).1.2 = e

theorem Actus.Contract.Properties.pam_md_cashflow_type {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} {t : Protocol.Time} (h : s.sd ≤ t) : (PAM.getCashflow ct rf (PAM.Step.md h)).1.2 = Protocol.EventType.MD

theorem Actus.Contract.Properties.pam_ip_cashflow_type {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} {t : Protocol.Time} (h : s.sd ≤ t) : (PAM.getCashflow ct rf (PAM.Step.ip h)).1.2 = Protocol.EventType.IP

theorem Actus.Contract.Properties.clamp_mem (lf lc x : ℝ) (h : lf ≤ lc) : lf ≤ min (max x lf) lc ∧ min (max x lf) lc ≤ lc

A two-sided clamp min (max x lf) lc lands in [lf, lc] whenever the floor does not exceed the cap. The order lemmas come from Mathlib's ℝ.

theorem Actus.Contract.Properties.pam_rr_rate_mem (ct : Terms ℝ) (rf : RiskFactorEnv ℝ) (t : Protocol.Time) (s : State ℝ) {lf lc : ℝ} (hf : ct.lifeFloor = some lf) (hc : ct.lifeCap = some lc) (h : lf ≤ lc) : lf ≤ (PAM.stf_RR ct rf t s).ipnr ∧ (PAM.stf_RR ct rf t s).ipnr ≤ lc

Rate cap/floor bound (PAM). After a rate reset the nominal rate lies within the life floor/cap window [RRLF, RRLC] (when both are present and well-ordered). Unprovable over Float; a theorem over ℝ.

theorem Actus.Contract.Properties.ann_rr_rate_mem (ct : Terms ℝ) (rf : RiskFactorEnv ℝ) (t : Protocol.Time) (s : State ℝ) {lf lc : ℝ} (hf : ct.lifeFloor = some lf) (hc : ct.lifeCap = some lc) (h : lf ≤ lc) : lf ≤ (ANN.stf_RR ct rf t s).ipnr ∧ (ANN.stf_RR ct rf t s).ipnr ≤ lc

Rate cap/floor bound (ANN). ANN's rate reset reuses PAM's rate logic, so the same window bound holds.

theorem Actus.Contract.Properties.redeemed_no_overshoot (nt prnxt : ℝ) (hnt : 0 ≤ nt) (hp : 0 ≤ prnxt) : 0 ≤ nt - LAM.redeemed nt prnxt ∧ nt - LAM.redeemed nt prnxt ≤ nt

Redemption non-overshoot (core). When the notional and instalment are both nonnegative (the sign-normalised case), the post-redemption notional Nt − redeemed Nt Prnxt stays in [0, Nt]: a redemption never overshoots 0, nor increases the magnitude. Needs a total order — ℝ, not Float.

theorem Actus.Contract.Properties.lam_pr_nt_mem (ct : Terms ℝ) (rf : RiskFactorEnv ℝ) (t : Protocol.Time) (s : State ℝ) (hnt : 0 ≤ s.nt) (hp : 0 ≤ s.prnxt) : 0 ≤ (LAM.stf_PR ct rf t s).nt ∧ (LAM.stf_PR ct rf t s).nt ≤ s.nt

Redemption non-overshoot (LAM PR step). Specialised to the actual STF_PR_LAM next-state: the notional after a principal redemption stays in [0, Nt].

theorem Actus.Contract.Properties.pam_rr_preserves_nt {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (t : Protocol.Time) (s : State α) : (PAM.stf_RR ct rf t s).nt = s.nt

A rate reset never moves principal — only the rate (and accruals/Sd).

theorem Actus.Contract.Properties.pam_pp_nt {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (t : Protocol.Time) (s : State α) : (PAM.stf_PP ct rf t s).nt = s.nt - rf.prepayment t

Prepayment reduces the notional by exactly the observed prepayment amount.

theorem Actus.Contract.Properties.pam_ipci_capitalizes {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (t : Protocol.Time) (s : State α) : (PAM.stf_IPCI ct rf t s).nt = s.nt + PAM.ipacAccr rf t s ∧ (PAM.stf_IPCI ct rf t s).ipac = 0

Interest capitalization (IPCI) moves the accrued interest into the notional and resets accrued interest to 0 — value is conserved, not created. Holds definitionally at any amount type.

theorem Actus.Contract.Properties.lam_redeemed_full {α : Type} [Amount α] [DecidableLE α] {nt prnxt : α} (h : Amount.abs nt ≤ Amount.abs prnxt) : LAM.redeemed nt prnxt = nt

When the instalment covers the whole (sign-normalised) notional, the entire notional is redeemed.

theorem Actus.Contract.Properties.lam_redeemed_partial {α : Type} [Amount α] [DecidableLE α] {nt prnxt : α} (h : ¬Amount.abs nt ≤ Amount.abs prnxt) : LAM.redeemed nt prnxt = prnxt

Otherwise exactly the instalment is redeemed.

theorem Actus.Contract.Properties.redeemed_abs_le (nt prnxt : ℝ) : |LAM.redeemed nt prnxt| ≤ |nt|

Redeemed amount is bounded by the notional magnitude (sign-free): a redemption never pays out more than the outstanding notional. Over ℝ.

theorem Actus.Contract.Properties.lam_pr_full_repay (ct : Terms ℝ) (rf : RiskFactorEnv ℝ) (t : Protocol.Time) (s : State ℝ) (h : |s.nt| ≤ |s.prnxt|) : (LAM.stf_PR ct rf t s).nt = 0

Full repayment empties the notional. Once the instalment reaches the outstanding notional, the PR step drives it to exactly 0. Over ℝ.

theorem Actus.Contract.Properties.lam_pr_nt_lt (ct : Terms ℝ) (rf : RiskFactorEnv ℝ) (t : Protocol.Time) (s : State ℝ) (hnt : 0 < s.nt) (hp : 0 < s.prnxt) : (LAM.stf_PR ct rf t s).nt < s.nt

Strict amortization. With a strictly positive notional and instalment, a PR step strictly decreases the notional (progress toward repayment). Over ℝ.

theorem Actus.Contract.Properties.pam_rr_uncapped (ct : Terms ℝ) (rf : RiskFactorEnv ℝ) (t : Protocol.Time) (s : State ℝ) (hpc : ct.periodCap = none) (hpf : ct.periodFloor = none) (hlc : ct.lifeCap = none) (hlf : ct.lifeFloor = none) : (PAM.stf_RR ct rf t s).ipnr = rf.marketRate t * ct.rrmlt + ct.rrsp

With every cap/floor absent, a rate reset sets the rate to the raw market target Oʳᶠ(RRMO,t)·RRMLT + RRSP (the previous rate cancels).

inductive Actus.Contract.Properties.PRTrace (ct : Terms ℝ) (rf : RiskFactorEnv ℝ) : State ℝ → State ℝ → Prop

A principal-redemption trace: zero or more PR steps (each admissible, Sd ≤ t). This is the sub-relation of LAM.Trace that only redeems principal — exactly the regime in which the notional should be conserved (other events like IED/IPCI reset or grow it).

• refl {ct : Terms ℝ} {rf : RiskFactorEnv ℝ} {s : State ℝ} : PRTrace ct rf s s
• step {ct : Terms ℝ} {rf : RiskFactorEnv ℝ} {s : State ℝ} {t : Protocol.Time} {s' : State ℝ} (ht : s.sd ≤ t) (rest : PRTrace ct rf (LAM.stf_PR ct rf t s) s') : PRTrace ct rf s s'

theorem Actus.Contract.Properties.prTrace_nt_mem {ct : Terms ℝ} {rf : RiskFactorEnv ℝ} {s s' : State ℝ} (h : PRTrace ct rf s s') : 0 ≤ s.nt → 0 ≤ s.prnxt → 0 ≤ s'.nt ∧ s'.nt ≤ s.nt

Trace-level conservation. Along a whole principal-redemption trace, the notional stays in [0, Nt₀]: it never goes negative (no overshoot past 0) and never exceeds its starting value (monotone repayment). Proved by induction on the trace from the single-step bound lam_pr_nt_mem; the instalment Prnxt is preserved by PR, so its nonnegativity propagates.

theorem Actus.Contract.Properties.prTrace_abs_le {ct : Terms ℝ} {rf : RiskFactorEnv ℝ} {s s' : State ℝ} (h : PRTrace ct rf s s') (hnt : 0 ≤ s.nt) (hp : 0 ≤ s.prnxt) : |s'.nt| ≤ |s.nt|

Magnitude form: a redemption trace never increases the notional's magnitude (|Nt'| ≤ |Nt₀|), given the sign-normalised nonnegative starting state.

theorem Actus.Contract.Properties.prTrace_isTrace {ct : Terms ℝ} {rf : RiskFactorEnv ℝ} {s s' : State ℝ} (h : PRTrace ct rf s s') : Nonempty (LAM.Trace ct rf s s')

A PRTrace is a genuine LAM execution trace (each PR step is the LAM.Step for event .PR), so the conservation above is a statement about real executions, not a separate toy relation.

theorem Actus.Contract.Properties.capfl_intrinsic_nonneg (rate cap flr : ℝ) : 0 ≤ max (rate - cap) 0 + max (flr - rate) 0

Cap/floor intrinsic is non-negative. CAPFL pays N·Y·(max(rate−cap,0) + max(floor−rate,0)) per period; the rate-excess kernel is always ≥ 0, so a long cap/floor never has a negative leg.

theorem Actus.Contract.Properties.capfl_cap_inactive (rate cap : ℝ) (h : rate ≤ cap) : max (rate - cap) 0 = 0

A cap pays nothing while the rate is at or below the cap.

theorem Actus.Contract.Properties.capfl_floor_inactive (rate flr : ℝ) (h : flr ≤ rate) : max (flr - rate) 0 = 0

A floor pays nothing while the rate is at or above the floor.

theorem Actus.Contract.Properties.option_call_intrinsic_nonneg (s k : ℝ) : 0 ≤ max (s - k) 0

Option intrinsic value is non-negative — a European call (max(S−K,0)) and put (max(K−S,0)) never settle negative; the holder's payoff is ≥ 0.

theorem Actus.Contract.Properties.option_put_intrinsic_nonneg (s k : ℝ) : 0 ≤ max (k - s) 0

theorem Actus.Contract.Properties.option_call_pos_iff (s k : ℝ) : 0 < max (s - k) 0 ↔ k < s

A call is in the money exactly when the underlying exceeds the strike.

theorem Actus.Contract.Properties.futur_payoff_linear (s f : ℝ) : s - f + (f - s) = 0

Future/forward payoff is linear — the settlement S − F carries no optional floor; gains and losses are symmetric.

theorem Actus.Contract.Properties.fxout_delivery_sum (sgn nt1 nt2 : ℝ) : sgn * nt1 + -(sgn * nt2) = sgn * (nt1 - nt2)

FX delivery conservation. An FXOUT delivery settles the two notionals as sign·Nt₁ and −sign·Nt₂; at a unit FX rate the two legs net to the par-difference sign·(Nt₁ − Nt₂).

theorem Actus.Contract.Properties.swppv_net_eq_legs (sgn n fix flt y : ℝ) : sgn * n * fix * y + -(sgn * n * flt * y) = sgn * n * (fix - flt) * y

Swap net settlement equals the leg sum. A plain-vanilla swap's per-period fixed leg sign·N·fix·Y and floating leg −sign·N·flt·Y net to the single cash flow sign·N·(fix−flt)·Y — exactly what the deliverySettlement = "S" fold computes from the two D legs.

theorem Actus.Contract.Properties.cec_payout_le_value (claim value : ℝ) : min claim value ≤ value

Collateral cap. CEC settles min(coverage·exposure, collateralValue), so the payout never exceeds the posted collateral …

theorem Actus.Contract.Properties.cec_payout_le_claim (claim value : ℝ) : min claim value ≤ claim

… nor the covered claim.

theorem Actus.Contract.Properties.foldl_add_nonneg (xs : List ℝ) (a : ℝ) : 0 ≤ a → (∀ x ∈ xs, 0 ≤ x) → 0 ≤ List.foldl (fun (x1 x2 : ℝ) => x1 + x2) a xs

A non-negative accumulator stays non-negative when folding in non-negative summands — the kernel behind exposure/notional aggregation.

theorem Actus.Contract.Properties.ceg_exposure_nonneg (legs : List ℝ) (h : ∀ x ∈ legs, 0 ≤ x) : 0 ≤ List.foldl (fun (x1 x2 : ℝ) => x1 + x2) 0 legs

Credit-enhancement exposure is non-negative. A guarantee's covered exposure is a sum of per-leg magnitudes (|Nt| + accrued); aggregating non-negative legs keeps it ≥ 0, hence the payout coverage·exposure has the contract-role sign and never flips.

theorem Actus.Contract.Properties.ump_stf_sd {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (e : Protocol.EventType) (t : Protocol.Time) (s : State α) : (UMP.stf ct rf e t s).sd = t

theorem Actus.Contract.Properties.lax_stf_sd {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (e : Protocol.EventType) (x : α) (t : Protocol.Time) (s : State α) : (LAX.stf ct rf e x t s).sd = t

theorem Actus.Contract.Properties.ump_step_mono {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (h : UMP.Step ct rf s s') : s.sd ≤ s'.sd

theorem Actus.Contract.Properties.lax_step_mono {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (h : LAX.Step ct rf s s') : s.sd ≤ s'.sd

theorem Actus.Contract.Properties.swppv_step_mono {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (h : SWPPV.Step ct rf s s') : s.sd ≤ s'.sd

SWPPV monotonicity holds even though IPFX/RR keep Sd: a step either leaves Sd unchanged or advances it to the (admissible) event time.

theorem Actus.Contract.Properties.ump_trace_mono {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (tr : UMP.Trace ct rf s s') : s.sd ≤ s'.sd

theorem Actus.Contract.Properties.lax_trace_mono {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (tr : LAX.Trace ct rf s s') : s.sd ≤ s'.sd

theorem Actus.Contract.Properties.swppv_trace_mono {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (tr : SWPPV.Trace ct rf s s') : s.sd ≤ s'.sd

theorem Actus.Contract.Properties.ump_stf_md {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (e : Protocol.EventType) (t : Protocol.Time) (s : State α) : (UMP.stf ct rf e t s).md = s.md

theorem Actus.Contract.Properties.lax_stf_md {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (e : Protocol.EventType) (x : α) (t : Protocol.Time) (s : State α) : (LAX.stf ct rf e x t s).md = s.md

theorem Actus.Contract.Properties.swppv_stf_md {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (e : Protocol.EventType) (t : Protocol.Time) (s : State α) : (SWPPV.stf ct rf e t s).md = s.md

theorem Actus.Contract.Properties.ump_stf_prf {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (e : Protocol.EventType) (t : Protocol.Time) (s : State α) : (UMP.stf ct rf e t s).prf = s.prf

theorem Actus.Contract.Properties.lax_stf_prf {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (e : Protocol.EventType) (x : α) (t : Protocol.Time) (s : State α) : (LAX.stf ct rf e x t s).prf = s.prf

theorem Actus.Contract.Properties.swppv_stf_prf {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (e : Protocol.EventType) (t : Protocol.Time) (s : State α) : (SWPPV.stf ct rf e t s).prf = s.prf

theorem Actus.Contract.Properties.swppv_stf_nt {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (e : Protocol.EventType) (t : Protocol.Time) (s : State α) : (SWPPV.stf ct rf e t s).nt = s.nt

Swap notional is never exchanged. No SWPPV event moves the notional — only the period boundary Sd (via IPFL) and the floating rate (via RR) change. A swap exchanges interest, not principal.

theorem Actus.Contract.Properties.ump_step_det {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s₁ s₂ : State α} {e : Protocol.EventType} {t : Protocol.Time} (he₁ : s₁ = UMP.stf ct rf e t s) (he₂ : s₂ = UMP.stf ct rf e t s) : s₁ = s₂

theorem Actus.Contract.Properties.lax_step_det {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s₁ s₂ : State α} {e : Protocol.EventType} {x : α} {t : Protocol.Time} (he₁ : s₁ = LAX.stf ct rf e x t s) (he₂ : s₂ = LAX.stf ct rf e x t s) : s₁ = s₂

theorem Actus.Contract.Properties.swppv_step_det {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s₁ s₂ : State α} {e : Protocol.EventType} {t : Protocol.Time} (he₁ : s₁ = SWPPV.stf ct rf e t s) (he₂ : s₂ = SWPPV.stf ct rf e t s) : s₁ = s₂

theorem Actus.Contract.Properties.ump_cashflows_length {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (tr : UMP.Trace ct rf s s') : (UMP.getCashflows ct rf tr).length = traceLen tr

theorem Actus.Contract.Properties.lax_cashflows_length {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (tr : LAX.Trace ct rf s s') : (LAX.getCashflows ct rf tr).length = traceLen tr

theorem Actus.Contract.Properties.swppv_cashflows_length {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (tr : SWPPV.Trace ct rf s s') : (SWPPV.getCashflows ct rf tr).length = traceLen tr

theorem Actus.Contract.Properties.ump_cashflow_time {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (h : UMP.Step ct rf s s') : (UMP.getCashflow ct rf h).1.1 = s'.sd

theorem Actus.Contract.Properties.lax_cashflow_time {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s s' : State α} (h : LAX.Step ct rf s s') : (LAX.getCashflow ct rf h).1.1 = s'.sd

theorem Actus.Contract.Properties.swppv_cashflow_time {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} (e : Protocol.EventType) (t : Protocol.Time) (h : s.sd ≤ t) : (SWPPV.getCashflow ct rf (SWPPV.Step.ev e t h)).1.1 = t

theorem Actus.Contract.Properties.ump_cashflow_type {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} (e : Protocol.EventType) {t : Protocol.Time} (h : s.sd ≤ t) : (UMP.getCashflow ct rf (UMP.Step.ev e h)).1.2 = e

theorem Actus.Contract.Properties.lax_cashflow_type {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} (e : Protocol.EventType) (x : α) {t : Protocol.Time} (h : s.sd ≤ t) : (LAX.getCashflow ct rf (LAX.Step.ev e x h)).1.2 = e

theorem Actus.Contract.Properties.swppv_cashflow_type {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} (e : Protocol.EventType) (t : Protocol.Time) (h : s.sd ≤ t) : (SWPPV.getCashflow ct rf (SWPPV.Step.ev e t h)).1.2 = e

theorem Actus.Contract.Properties.lax_pr_nt {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (x : α) (t : Protocol.Time) (s : State α) : (LAX.stf_PR ct rf x t s).nt = s.nt - Util.Conventions.sign ct.cntrl * x

A LAX redemption reduces the notional by exactly the (signed) instalment.

theorem Actus.Contract.Properties.lax_pi_nt {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (x : α) (t : Protocol.Time) (s : State α) : (LAX.stf_PI ct rf x t s).nt = s.nt + Util.Conventions.sign ct.cntrl * x

A LAX draw increases the notional by exactly the (signed) draw.

theorem Actus.Contract.Properties.lax_md_nt {α : Type} [Amount α] [DecidableLE α] {rf : RiskFactorEnv α} (t : Protocol.Time) (s : State α) : (LAX.stf_MD rf t s).nt = 0

LAX maturity pays out and zeroes the residual notional.

theorem Actus.Contract.Properties.ump_ipci_value {α : Type} [Amount α] [DecidableLE α] {rf : RiskFactorEnv α} (t : Protocol.Time) (s : State α) : (UMP.stf_IPCI rf t s).nt = s.nt + s.nt * s.ipnr * rf.yf s.sd t ∧ (UMP.stf_IPCI rf t s).ipac = 0

UMP capitalization is value-conserving. An IPCI event grows the notional by the interest accrued over the period and resets the accrual; no cash leaves the contract (pof = 0).

theorem Actus.Contract.Properties.swppv_rr_rate_mem (ct : Terms ℝ) (rf : RiskFactorEnv ℝ) (t : Protocol.Time) (s : State ℝ) {lf lc : ℝ} (hf : ct.lifeFloor = some lf) (hc : ct.lifeCap = some lc) (h : lf ≤ lc) : lf ≤ (SWPPV.stf_RR ct rf t s).ipnr ∧ (SWPPV.stf_RR ct rf t s).ipnr ≤ lc

Rate cap/floor bound (SWPPV). After a floating-rate reset the rate lies within the life floor/cap window [lifeFloor, lifeCap] (both present and well-ordered). The swap analogue of pam_rr_rate_mem; a theorem over ℝ.

theorem Actus.Contract.Properties.swppv_pof_net (ct : Terms ℝ) (rf : RiskFactorEnv ℝ) (t : Protocol.Time) (s : State ℝ) : SWPPV.pof_IPFX ct rf t s + SWPPV.pof_IPFL rf t s = s.nt * (ct.ipnr - s.ipnr) * rf.yf s.sd t

Swap leg netting (kernel-level). A period's fixed leg pof_IPFX and floating leg pof_IPFL sum to N·(fixedRate − floatRate)·Y — exactly the single cash flow the deliverySettlement = "S" fold produces from the two gross legs. Now stated on the actual SWPPV.pof_*, not abstract terms.

theorem Actus.Contract.Properties.ump_ipci_nondecr (rf : RiskFactorEnv ℝ) (t : Protocol.Time) (s : State ℝ) (hnt : 0 ≤ s.nt) (hr : 0 ≤ s.ipnr) (hy : 0 ≤ rf.yf s.sd t) : s.nt ≤ (UMP.stf_IPCI rf t s).nt

UMP compounding never shrinks the deposit. With a non-negative notional, rate and year fraction, an IPCI capitalization leaves the notional no smaller (interest only ever adds to a positive-rate deposit). Over ℝ.

theorem Actus.Contract.Properties.swppv_ipnr_only_rr {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} (e : Protocol.EventType) (t : Protocol.Time) (s : State α) (h : e ≠ Protocol.EventType.RR) : (SWPPV.stf ct rf e t s).ipnr = s.ipnr

Only a rate reset moves the floating rate. Every non-RR SWPPV event (the two legs, clock ticks) leaves Ipnr untouched; the floating rate is changed exclusively by RR.

theorem Actus.Contract.Properties.swppv_legs_opposite (ct : Terms ℝ) (rf : RiskFactorEnv ℝ) (t : Protocol.Time) (s : State ℝ) (h : ct.ipnr = s.ipnr) : SWPPV.pof_IPFX ct rf t s = -SWPPV.pof_IPFL rf t s

At par the legs cancel. When the fixed and floating rates coincide (fixedRate = Ipnr), the fixed leg is exactly the negation of the floating leg — so the two legs are sign-opposite.

theorem Actus.Contract.Properties.swppv_par_net_zero (ct : Terms ℝ) (rf : RiskFactorEnv ℝ) (t : Protocol.Time) (s : State ℝ) (h : ct.ipnr = s.ipnr) : SWPPV.pof_IPFX ct rf t s + SWPPV.pof_IPFL rf t s = 0

At par the net settlement is zero. Hence the deliverySettlement = "S" netted period flow vanishes when the swap is at par.

inductive Actus.Contract.Properties.IPCITrace (rf : RiskFactorEnv ℝ) : State ℝ → State ℝ → Type

A capitalization trace: zero or more IPCI steps (each admissible, Sd ≤ t). Lives in Type so the multiplicative growth factor below can be extracted from it.

• refl {rf : RiskFactorEnv ℝ} {s : State ℝ} : IPCITrace rf s s
• step {rf : RiskFactorEnv ℝ} {s : State ℝ} {t : Protocol.Time} {s' : State ℝ} (ht : s.sd ≤ t) (rest : IPCITrace rf (UMP.stf_IPCI rf t s) s') : IPCITrace rf s s'

noncomputable def Actus.Contract.Properties.ipciFactor (rf : RiskFactorEnv ℝ) {s s' : State ℝ} : IPCITrace rf s s' → ℝ

The compound growth factor ∏ᵢ (1 + rateᵢ·Yᵢ) accumulated along a capitalization trace (rateᵢ/Yᵢ read from the running state at step i).

Equations

• Actus.Contract.Properties.ipciFactor rf Actus.Contract.Properties.IPCITrace.refl = 1
• Actus.Contract.Properties.ipciFactor rf (Actus.Contract.Properties.IPCITrace.step ht rest) = (1 + x✝¹.ipnr * rf.yf x✝¹.sd t) * Actus.Contract.Properties.ipciFactor rf rest

theorem Actus.Contract.Properties.ipciTrace_ipnr (rf : RiskFactorEnv ℝ) {s s' : State ℝ} (tr : IPCITrace rf s s') : s'.ipnr = s.ipnr

The nominal rate is constant under capitalization. IPCI never touches Ipnr, so it is the same throughout the trace — justifying the single rate in the closed form below.

theorem Actus.Contract.Properties.ump_ipci_closed_form (rf : RiskFactorEnv ℝ) {s s' : State ℝ} (tr : IPCITrace rf s s') : s'.nt = s.nt * ipciFactor rf tr

UMP compound-growth closed form. After a capitalization trace the notional is the initial notional times the product of the per-period growth factors: Nt' = Nt₀ · ∏ᵢ (1 + rate·Yᵢ). Proved by induction on the trace — each IPCI multiplies the notional by its (1 + rate·Y) factor.

theorem Actus.Contract.Properties.lax_pr_nt_le (ct : Terms ℝ) (rf : RiskFactorEnv ℝ) (x : ℝ) (t : Protocol.Time) (s : State ℝ) (hx : 0 ≤ x) (hsign : 0 ≤ Util.Conventions.sign ct.cntrl) : (LAX.stf_PR ct rf x t s).nt ≤ s.nt

A single LAX redemption with a non-negative instalment, on the long (sign ≥ 0) side, does not increase the notional. Unlike LAM's capped redeemed, STF_PR_LAX subtracts the raw (signed) instalment, so this is a one-sided (monotone) bound rather than a [0, Nt] window.

inductive Actus.Contract.Properties.LAXPRTrace (ct : Terms ℝ) (rf : RiskFactorEnv ℝ) : State ℝ → State ℝ → Prop

A redemption (PR) trace for LAX: zero or more DEC redemptions, each with a non-negative instalment x at an admissible time.

• refl {ct : Terms ℝ} {rf : RiskFactorEnv ℝ} {s : State ℝ} : LAXPRTrace ct rf s s
• step {ct : Terms ℝ} {rf : RiskFactorEnv ℝ} {s : State ℝ} {x : ℝ} {t : Protocol.Time} {s' : State ℝ} (hx : 0 ≤ x) (ht : s.sd ≤ t) (rest : LAXPRTrace ct rf (LAX.stf_PR ct rf x t s) s') : LAXPRTrace ct rf s s'

theorem Actus.Contract.Properties.laxPRTrace_nt_le {ct : Terms ℝ} {rf : RiskFactorEnv ℝ} {s s' : State ℝ} (h : LAXPRTrace ct rf s s') (hsign : 0 ≤ Util.Conventions.sign ct.cntrl) : s'.nt ≤ s.nt

Monotone amortization. Along a whole LAX redemption trace, the notional never increases: Nt' ≤ Nt₀ (the long-side, non-negative-instalment case). Proved by induction from the single-step bound lax_pr_nt_le.

theorem Actus.Contract.Properties.laxPRTrace_isTrace {ct : Terms ℝ} {rf : RiskFactorEnv ℝ} {s s' : State ℝ} (h : LAXPRTrace ct rf s s') : Nonempty (LAX.Trace ct rf s s')

A LAXPRTrace is a genuine LAX execution trace (each step is the LAX.Step for event .PR with payload x), so the bound above is about real executions, not a separate toy relation.