Bounded Rationality and the Spectral Complexity of Games

Finding a Nash equilibrium is PPAD-complete (Daskalakis, Goldberg & Papadimitriou, 2009), yet economic models routinely assume agents play equilibrium strategies. This paper connects that benchmark to a Latent-parameterized family of inequalities: the Latent Number \(\rho\) of the payoff tensor is used to organize when spectral truncation and query-style budgets behave mildly versus sharply. Under the algebraic templates recorded below, the query proxy scales as \(N^* = C \cdot \log(1/\varepsilon) / \log(\rho)\) (Theorem 3), and truncation errors decay geometrically in the number of retained components (Theorem 4). We also formalize bookkeeping lemmas that support an EMH-style limit narrative: when a dominance parameter sends the market analogue of \(\rho\) to a regime where residual terms vanish, inefficiency can be made arbitrarily small (Theorem 11), while finite-parameter instances obey the proportional scaling recorded in the same certificate. Grossman–Stiglitz (1980) is cited as the classical information-efficiency tension this parameterization is meant to echo, not replace. Fifteen theorems are machine-checked in Lean 4 (see companion script), with no user axioms in that file.