GrowthCurve: the windowed dual of WindowedDecay

A function Nat → Nat that grows from 0 at tBegin to peak at tEnd, monotone non-decreasing within the window. Same architectural pattern as WindowedDecay — bundled structure with embedded proofs — but applied to the dual shape.

This module exists to demonstrate that the bundled-structure pattern composes across dual domains. Every WindowedDecay has a complementary GrowthCurve via the bridge constructor below; future "natively growing" shapes (linear vesting written as a primitive rather than via complement, capped compound interest in a fixed window, etc.) become first-class GrowthCurve instances by providing their own toGrowthCurve constructor.

Unbounded growth shapes (e.g. open-ended compound interest with no maturity) are not GrowthCurve — they need a separate MonotoneSequence-style abstraction, which is future work documented in the project README.

Main definitions

• GrowthCurve — the bundled function + monotone-growth proofs.
• WindowedDecay.toComplementaryGrowthCurve — the canonical bridge: any decay's complement is a growth.

Main statements

The four defining properties live in the structure. The constructor proves them, so consumers get them by projection.

structure Solanalib.Finance.GrowthCurve : Type

A function Nat → Nat that grows from 0 at tBegin to peak at tEnd, monotone non-decreasing within the window. The four defining properties are bundled in (compare WindowedDecay).

Construct via a domain-specific helper (e.g. WindowedDecay.toComplementaryGrowthCurve).

• tBegin : Nat

  Start of the growth window.

• tEnd : Nat

  End of the growth window (inclusive: apply tEnd = peak).

• peak : Nat

  Peak value, reached at tEnd.

• apply : Nat → Nat

  The growth function.

• bounded (t : Nat) : self.apply t ≤ self.peak

  The growth never exceeds peak.

• at_begin : self.tBegin < self.tEnd → self.apply self.tBegin = 0

  At the start of a non-degenerate window, the value is zero.

• at_end : self.apply self.tEnd = self.peak

  At the end of the window, the value equals peak.

• monotone_in_window {t₁ t₂ : Nat} : self.tBegin ≤ t₁ → t₁ ≤ t₂ → t₂ < self.tEnd → self.apply t₁ ≤ self.apply t₂

  Within the window, the value is monotone non-decreasing in time.

def Solanalib.Finance.WindowedDecay.toComplementaryGrowthCurve (d : WindowedDecay) : GrowthCurve

The canonical bridge: every WindowedDecay d induces a GrowthCurve via t ↦ d.peak - d.apply t. This is the "vesting" view of a decay (claimable balance = total − remaining lock).

All four GrowthCurve properties are inherited mechanically from the corresponding WindowedDecay properties — this is the architectural demonstration that bundled structures compose across dual domains.

Equations

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