papers/lux-credit-protocol-spec/sections/04-system-invariants.tex

\section{System Invariants}

\label{sec:invariants}

Let $B$ denote total backing value, $L$ total outstanding credit liabilities, and $E = B - L$ protocol equity. All values are denominated in the base asset's native unit.

\subsection{Core Issuance Invariant}

\begin{invariant}[Issuance Cap]
\label{inv:issuance}
\begin{equation}
  L \leq \lambda \cdot B
\end{equation}
where $\lambda = \texttt{issuanceLtvCap}$. For LETH with $\lambda = 0.9$: $L \leq 0.9 \cdot B$. Checked on every mint; reverts on violation.
\end{invariant}

\subsection{Redemption Invariant}

\begin{invariant}[In-Kind Redemption]
\label{inv:redemption}
\begin{equation}
  \texttt{burn}(x\;\text{LETH}) \Rightarrow \texttt{release}(x\;\text{ETH})
\end{equation}
subject only to finality delay (Section~\ref{sec:finality}), solvency state constraints (Section~\ref{sec:state-machine}), and applicable compliance requirements.
\end{invariant}

\subsection{Parity Invariant}

\begin{invariant}[Unit Parity]
\label{inv:parity}
Redeemable principal per unit of credit token equals exactly one unit of the base asset at all times, independent of surplus level or strategy performance.
\end{invariant}

\subsection{Equity Threshold}

\begin{invariant}[Minimum Equity Ratio]
\label{inv:equity}
Under maximum LTV $\lambda$:
\begin{equation}
  \frac{E}{B} \geq 1 - \lambda \quad\Leftrightarrow\quad \frac{L}{B} \leq \lambda
\end{equation}
For $\lambda = 0.9$: equity ratio $\geq 10\%$, leverage ratio $\leq 90\%$.
\end{invariant}