papers/lux-consensus/sections/01-introduction.tex

%% ===================================================================
%% LP-134 canonical naming (2025-12-15):
%% Per LP-134 (Lux Chain Topology), T-Chain has been split into:
%%   M-Chain — MPC ceremonies for bridge custody of EXTERNAL wallets
%%             (CGGMP21, FROST, Pulsar-general)
%%   F-Chain — FHE compute + TFHE bootstrap-key generation (encrypted EVM)
%% The legacy name "T-Chain" is retained ONLY for `teleportvm` (LP-6332).
%% Where this paper says "T-Chain MPC" / "T-Chain threshold governance" /
%% "T-Chain TFHE" / "T-Chain custody", read as M-Chain (MPC) or F-Chain (FHE).
%% ===================================================================

\section{Introduction}

\label{sec:introduction}

The fundamental tension in distributed consensus is the CAP theorem~\cite{brewer2000cap}:
no system can simultaneously guarantee Consistency, Availability, and Partition tolerance.
Classical Byzantine Fault Tolerant (BFT) protocols such as PBFT~\cite{castro1999practical}
sacrifice availability under partition and exhibit $O(n^2)$ communication complexity, making
them impractical for networks with hundreds or thousands of validators.
Nakamoto consensus~\cite{nakamoto2008bitcoin}, used in Bitcoin and its descendants, achieves
probabilistic safety and scales to large validator sets, but requires minutes to hours for
practical finality due to its longest-chain fork resolution mechanism.

The metastable protocol family, first described in the original
paper~\cite{rocket2019wave}, introduced a fundamentally different approach: metastable
consensus through repeated stochastic sampling. Rather than relying on a designated leader
or all-to-all voting rounds, these protocols have each node repeatedly poll a small random
sample of peers and adopt the majority preference. This gossip-like mechanism achieves
emergent agreement in $O(\log n)$ rounds with only $O(kn)$ total message complexity, where
$k$ is the small sample size (typically 20--50 nodes).

Lux Consensus extends this foundation with four key innovations:
\begin{enumerate}
\item \textbf{DAG-based transaction ordering}: Transactions form a directed acyclic graph
rather than a linear chain, enabling parallel processing and conflict-free ordering without
global serialization.
\item \textbf{Adaptive confidence counters}: The protocol tracks consecutive rounds of
supermajority agreement, requiring $\beta$ consecutive rounds before finalizing, which
provides a tunable safety--liveness knob.
\item \textbf{Metastability-breaking}: We introduce a deterministic tie-breaking mechanism
grounded in verifiable random functions (VRFs) that resolves pathological configurations
where the system is evenly split between two preferences.
\item \textbf{Formal security proofs}: We provide the first rigorous proofs of Byzantine
fault tolerance for a metastable consensus protocol, establishing $f < n/3$ as the exact fault
tolerance threshold under our security model.
\end{enumerate}

\paragraph{Contributions.}
This paper makes the following contributions:
\begin{itemize}[nosep]
\item A complete specification of the Lux Consensus protocol, including the DAG layer,
Wave confidence mechanism, and VRF-based tie-breaking (\S\ref{sec:protocol}).
\item Formal proofs of safety, liveness, and convergence under partial synchrony with
up to $f < n/3$ Byzantine faults (\S\ref{sec:analysis}).
\item A detailed parameterization analysis relating $(k, \alpha, \beta)$ to security
margins and performance characteristics (\S\ref{sec:params}).
\item An empirical evaluation on a 1,000-node globally distributed testnet demonstrating
4,500+ TPS with 650ms median finality (\S\ref{sec:evaluation}).
\item A comprehensive security analysis covering long-range attacks, eclipse attacks,
Sybil resistance, and timing adversaries (\S\ref{sec:security}).
\item Machine-checked formal proofs in Lean~4 (Mathlib v4.14.0) covering all protocol
components, BFT thresholds, cryptographic primitives, and cross-chain delivery,
with 33 of 36 theorems fully proved (\S\ref{sec:formal}).
\end{itemize}

The remainder of this paper is organized as follows. Section~\ref{sec:background} reviews
related work across the metastable consensus family, classical BFT, and Nakamoto consensus.
Section~\ref{sec:model} establishes the system model and adversary assumptions.
Section~\ref{sec:protocol} presents the Lux protocol in detail.
Section~\ref{sec:analysis} provides formal safety, liveness, and convergence proofs.
Section~\ref{sec:params} analyzes parameterization.
Section~\ref{sec:implementation} describes the implementation.
Section~\ref{sec:evaluation} presents empirical evaluation.
Section~\ref{sec:security} analyzes security considerations.
Section~\ref{sec:formal} presents the Lean~4 formal verification results.
Section~\ref{sec:conclusion} concludes.

%% -----------------------------------------------------------------------
%%  2. BACKGROUND AND RELATED WORK
%% -----------------------------------------------------------------------