Spectral Taxation: The Latent Structure of Optimal Income Tax Schedules

We apply the Latent spectral framework to the Mirrlees (1971) optimal taxation problem, showing that the information rent, tax schedule complexity, and welfare cost of progressive taxation are all governed by the Latent Number \(\rho\) of the ability distribution. Information rent (the cost of incentive compatibility) satisfies rent \(\propto 1/\rho\): ability distributions with high spectral concentration have similar types, making screening cheap. The optimal tax schedule is modeled as living in an \(N^\)-dimensional Latent subspace, with the identification \(N^ = \log(1/\delta)/\log(\rho)\) for approximation tolerance \(\delta\) (distinct from labor-supply elasticity \(\varepsilon\) below), and the flat tax emerges as the \(\rho \to \infty\) limit in the same reduced-form encoding. For multi-dimensional screening (ability \(\times\) effort \(\times\) risk type), the Latent truncation reduces the intractable infinite-dimensional problem to \(N^*\) dimensions with error \(O(\rho^{-N})\) at the level of the reduced form. Formalization scope: the companion Lean proof file checks 16 algebraic templates (signs, monotonicities, and a few arithmetic scenarios) under explicit hypotheses; it is not a full existence/characterization proof of the Mirrlees program. The cross-country table in §6 pairs illustrative \(\rho\) and fiscal magnitudes with those scenario lemmas—only the stated equalities/inequalities in us_top_rate, nordic_flatter_schedule, and developing_high_progressivity are kernel-checked, not the empirical calibration of \(\rho\) or GDP shares. 16 theorems, Lean 4–verified, 0 domain axioms (standard real-arithmetic bootstrap only).