Quantitative Arrow: Measuring Distance from Impossibility via the Latent Framework

Arrow's Impossibility Theorem (1951) proves that no social welfare function over three or more alternatives can simultaneously satisfy Unanimity, Independence of Irrelevant Alternatives (IIA), and Non-Dictatorship. This paper develops a quantitative narrative using the Latent Number \(\rho\): (1) IIA violation intensity is modeled to scale like \(1/\rho^2\), (2) dictator-adjacency is modeled to scale like \(1/\rho\), and (3) a companion scalar encoding records a manipulation gain bound compatible with \(1/(N-1)\) when a linear constraint \((N-1)g\le 1\) is imposed. The Latent viewpoint suggests a continuous "distance from Arrow" reading of aggregation stress, complementary to the classical impossibility statement. For an illustrative normalization with \(C=1\) and \(\rho=3\), the toy rate \(C/\rho^2=1/9\) is \(\approx 11\%\). Twelve lemmas in arrow_impossibility_proof.py are machine-checked in the Lean 4 kernel (real-arithmetic scaffolding; no extra domain axioms beyond the standard bootstrap).