CompoundInterest: discrete compounding as a MonotoneSequence

This module is the first downstream consumer that composes two Solanalib layers we built earlier:

• Solanalib.Numeric.Fraction is the rate's type — a Q68.60 fixed-point multiplier (1.0 = no growth, 1.01 = 1% growth per period, …).
• Solanalib.Finance.MonotoneSequence is the output's bundled type — the family of unbounded monotone Nat-indexed sequences.

The definition itself is short:

def balance (principal : Nat) (multiplier : Fraction) : Nat → Nat
  | 0     => principal
  | n + 1 => balance principal multiplier n * multiplier.bits / Fraction.scale

Each step multiplies by the Q68.60-encoded multiplier and divides back out by Fraction.scale. With multiplier ≥ Fraction.one (equivalently, multiplier.bits ≥ scale), this is provably monotone non-decreasing in n — that's the bundled-structure proof obligation for MonotoneSequence.

Main definitions

• Solanalib.Finance.CompoundInterest.balance — the discrete-compounding function.
• Solanalib.Finance.CompoundInterest.toMonotoneSequence — the composition: a (principal, multiplier ≥ 1) pair becomes a MonotoneSequence, inheriting all generic theorems.

Main statements

• balance_zero — balance p m 0 = p.
• balance_at_one_multiplier — with multiplier = 1.0, balance is constant.
• balance_succ_ge — one-step monotonicity (given multiplier ≥ 1).
• balance_monotone — arbitrary-step monotonicity.
• balance_ge_principal — balance never drops below the principal.

The four-property pattern follows LinearDecay's value_* discipline: one operation, several named theorems, each catching a distinct refactor-bug class (balance < principal would be a "lender loses funds" exploit; non-monotonicity would be a "wait longer, owe less" exploit; etc.).

The real-world step from this MVP to Kamino's approximate_compounded_interest is its truncated Taylor-series approximation of (1 + r)^n for large n. That refinement — and the error-bound theorem relating the approximation to the exact compounding done here — is roadmap work documented in the project README.

def Solanalib.Finance.CompoundInterest.balance (principal : LamportsUnchecked) (multiplier : Fraction) : LamportsUnchecked → LamportsUnchecked

The balance after periods periods of compounding from principal at multiplier multiplier.

Equations

• Solanalib.Finance.CompoundInterest.balance principal multiplier 0 = principal
• Solanalib.Finance.CompoundInterest.balance principal multiplier n.succ = Solanalib.Finance.CompoundInterest.balance principal multiplier n * multiplier.bits / Solanalib.Fraction.scale

Theorems

@[simp]

theorem Solanalib.Finance.CompoundInterest.balance_zero (principal : LamportsUnchecked) (multiplier : Fraction) : balance principal multiplier 0 = principal

Boundary: balance at step 0 is the principal.

theorem Solanalib.Finance.CompoundInterest.balance_at_one_multiplier (principal n : LamportsUnchecked) : balance principal Fraction.one n = principal

With a unit multiplier (i.e. Fraction.one, no growth), the balance is constant across all periods.

theorem Solanalib.Finance.CompoundInterest.balance_succ_ge (principal : LamportsUnchecked) (multiplier : Fraction) (h : Fraction.one ≤ multiplier) (n : LamportsUnchecked) : balance principal multiplier n ≤ balance principal multiplier (n + 1)

One-step monotonicity. With multiplier ≥ Fraction.one, the balance never decreases from one period to the next.

theorem Solanalib.Finance.CompoundInterest.balance_monotone (principal : LamportsUnchecked) (multiplier : Fraction) (h : Fraction.one ≤ multiplier) {n m : LamportsUnchecked} (hnm : n ≤ m) : balance principal multiplier n ≤ balance principal multiplier m

Multi-step monotonicity. With multiplier ≥ Fraction.one, the balance is monotone non-decreasing across any range of periods.

theorem Solanalib.Finance.CompoundInterest.balance_ge_principal (principal : LamportsUnchecked) (multiplier : Fraction) (h : Fraction.one ≤ multiplier) (n : LamportsUnchecked) : principal ≤ balance principal multiplier n

The balance never drops below the principal (given multiplier ≥ 1).

Composition into MonotoneSequence

The headline composition move: a (principal, multiplier ≥ 1) pair becomes a MonotoneSequence, which automatically inherits the two generic theorems proved in Solanalib.Finance.MonotoneSequence:

• MonotoneSequence.apply_zero_le — value at any step ≥ value at step 0.
• MonotoneSequence.apply_le_of_le — value-at-later ≥ value-at-earlier.

Construction discharges the single monotone obligation via balance_monotone. No new math; pure composition.

def Solanalib.Finance.CompoundInterest.toMonotoneSequence (principal : LamportsUnchecked) (multiplier : Fraction) (h : Fraction.one ≤ multiplier) : MonotoneSequence

Bundle a compounding configuration into a MonotoneSequence.

Equations

• Solanalib.Finance.CompoundInterest.toMonotoneSequence principal multiplier h = { apply := Solanalib.Finance.CompoundInterest.balance principal multiplier, monotone := ⋯ }