def Actus.Contract.LAM.lamIpcb {α : Type} [Amount α] (ct : Terms α) (nt : α) : α

Interest-calculation-base value: tracks Nt when IPCB = 'NT' (or absent), otherwise the fixed R(CNTRL)·IPCBA.

Equations

• Actus.Contract.LAM.lamIpcb ct nt = match ct.interestCalculationBase with | some Actus.Protocol.InterestCalculationBase.IPCB_NTL => Actus.Util.Conventions.sign ct.cntrl * ct.ipcba | x => nt

def Actus.Contract.LAM.ipacAccrIpcb {α : Type} [Amount α] (rf : RiskFactorEnv α) (t : Protocol.Time) (s : State α) : α

Interest accrual on the interest calculation base Ipcb.

Equations

• Actus.Contract.LAM.ipacAccrIpcb rf t s = s.ipac + rf.yf s.sd t * s.ipnr * s.ipcb

def Actus.Contract.LAM.stf_IED {α : Type} [Amount α] (ct : Terms α) (t : Protocol.Time) (s : State α) : State α

Equations

• One or more equations did not get rendered due to their size.

def Actus.Contract.LAM.redeemed {α : Type} [Amount α] [DecidableLE α] (nt prnxt : α) : α

The actual principal redeemed: the instalment Prnxt, but capped at the remaining notional so a redemption never overshoots 0 (the final instalment is partial; once Nt = 0 it pays nothing). Prnxt and Nt share the contract-role sign.

Equations

• Actus.Contract.LAM.redeemed nt prnxt = if Actus.Amount.abs nt ≤ Actus.Amount.abs prnxt then nt else prnxt

def Actus.Contract.LAM.stf_PR {α : Type} [Amount α] [DecidableLE α] (ct : Terms α) (rf : RiskFactorEnv α) (t : Protocol.Time) (s : State α) : State α

Principal redemption: pay back Prnxt (capped at the remaining notional), accruing interest on Ipcb. Prnxt already carries the contract-role sign (set in lamInit/init).

Equations

• One or more equations did not get rendered due to their size.

def Actus.Contract.LAM.stf_IPCB {α : Type} (t : Protocol.Time) (s : State α) : State α

Equations

• Actus.Contract.LAM.stf_IPCB 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.nt, prf := s.prf, sd := t }

def Actus.Contract.LAM.stf_IPCI {α : Type} [Amount α] (ct : Terms α) (rf : RiskFactorEnv α) (t : Protocol.Time) (s : State α) : State α

Equations

• One or more equations did not get rendered due to their size.

def Actus.Contract.LAM.stf {α : Type} [Amount α] [DecidableLE α] (ct : Terms α) (rf : RiskFactorEnv α) (ev : Protocol.EventType) (t : Protocol.Time) (s : State α) : State α

STF dispatcher: LAM-specific events plus PAM delegation.

Equations

• Actus.Contract.LAM.stf ct rf Actus.Protocol.EventType.IED t s = Actus.Contract.LAM.stf_IED ct t s
• Actus.Contract.LAM.stf ct rf Actus.Protocol.EventType.PR t s = Actus.Contract.LAM.stf_PR ct rf t s
• Actus.Contract.LAM.stf ct rf Actus.Protocol.EventType.IPCB t s = Actus.Contract.LAM.stf_IPCB t s
• Actus.Contract.LAM.stf ct rf Actus.Protocol.EventType.IPCI t s = Actus.Contract.LAM.stf_IPCI ct rf t s
• Actus.Contract.LAM.stf ct rf ev t s = Actus.Contract.PAM.stf ct rf ev t s

def Actus.Contract.LAM.pof_PR {α : Type} [Amount α] [DecidableLE α] (rf : RiskFactorEnv α) (t : Protocol.Time) (s : State α) : α

Equations

• Actus.Contract.LAM.pof_PR rf t s = rf.curs t * s.nsc * Actus.Contract.LAM.redeemed s.nt s.prnxt

def Actus.Contract.LAM.pof_IP {α : Type} [Amount α] (rf : RiskFactorEnv α) (t : Protocol.Time) (s : State α) : α

Interest payment accrues on the interest calculation base Ipcb (which may differ from Nt when IPCB ≠ 'NT'), unlike PAM which accrues on Nt.

Equations

• Actus.Contract.LAM.pof_IP rf t s = rf.curs t * s.isc * (s.ipac + rf.yf s.sd t * s.ipnr * s.ipcb)

def Actus.Contract.LAM.pof {α : Type} [Amount α] [DecidableLE α] (ct : Terms α) (rf : RiskFactorEnv α) (ev : Protocol.EventType) (t : Protocol.Time) (s : State α) : α

Equations

• Actus.Contract.LAM.pof ct rf Actus.Protocol.EventType.PR t s = Actus.Contract.LAM.pof_PR rf t s
• Actus.Contract.LAM.pof ct rf Actus.Protocol.EventType.IP t s = Actus.Contract.LAM.pof_IP rf t s
• Actus.Contract.LAM.pof ct rf ev t s = Actus.Contract.PAM.pof ct rf ev t s

def Actus.Contract.LAM.init {α : Type} [Amount α] (ct : Terms α) (md t₀ : Protocol.Time) : State α

Initial state. Prnxt defaults to the term PRNXT, falling back to the full notional when absent (the annuity-style fallback needs the redemption schedule, omitted here).

Equations

• One or more equations did not get rendered due to their size.

inductive Actus.Contract.LAM.Step {α : Type} [Amount α] [DecidableLE α] (ct : Terms α) (rf : RiskFactorEnv α) : State α → State α → Type

One-step LAM transition. Constructors target the LAM dispatcher stf.

• ev {α : Type} [Amount α] [DecidableLE α] {ct : Terms α} {rf : RiskFactorEnv α} {s : State α} (e : Protocol.EventType) {t : Protocol.Time} : s.sd ≤ t → Step ct rf s (stf ct rf e t s)

@[reducible, inline]

abbrev Actus.Contract.LAM.Trace {α : Type} [Amount α] [DecidableLE α] (ct : Terms α) (rf : RiskFactorEnv α) : State α → State α → Type

Equations

• Actus.Contract.LAM.Trace ct rf = Actus.Closures.Star (Actus.Contract.LAM.Step ct rf)

def Actus.Contract.LAM.getCashflow {α : Type} [Amount α] [DecidableLE α] (ct : Terms α) (rf : RiskFactorEnv α) {s s' : State α} (h : Step ct rf s s') : Protocol.Event × α

Equations

• Actus.Contract.LAM.getCashflow ct rf (Actus.Contract.LAM.Step.ev e a) = (((Actus.Contract.LAM.stf ct rf e t s).sd, e), Actus.Contract.LAM.pof ct rf e (Actus.Contract.LAM.stf ct rf e t s).sd s)

def Actus.Contract.LAM.getCashflows {α : Type} [Amount α] [DecidableLE α] (ct : Terms α) (rf : RiskFactorEnv α) {s s' : State α} : Trace ct rf s s' → List (Protocol.Event × α)

Equations

• Actus.Contract.LAM.getCashflows ct rf Actus.Closures.Star.refl = []
• Actus.Contract.LAM.getCashflows ct rf (Actus.Closures.Star.step h rest) = Actus.Contract.LAM.getCashflow ct rf h :: Actus.Contract.LAM.getCashflows ct rf rest

def Actus.Contract.LAM.LAM_contract : Abstract.ActusContract

Equations

• Actus.Contract.LAM.LAM_contract = { Terms := Actus.Contract.Terms Float, State := Actus.Contract.State Float }

def Actus.Contract.LAM.LAM_impl (ct : Terms Float) (rf : RiskFactorEnv Float) (s₀ : State Float) : Abstract.StateTransition LAM_contract

Equations

• One or more equations did not get rendered due to their size.