Spectral Microstructure: Kyle's Lambda, Price Discovery, and the HFT Debate through the Latent Lens

We recast Kyle's (1985) insider-trading and price-discovery story in the Latent spectral framework: price impact \(\lambda\), spreads, and depth are read through the Latent Number \(\rho\) of the price signal. Under the Latent identification \(\rho\lambda=\text{const}\) across regimes (a comparative-statics encoding made explicit below), spectrally concentrated markets have lower \(\lambda\) and tighter spreads. We use a geometric narrative for discovery—residual mispricing scaled by \(\rho^{-N}\) after \(N\) trades—as the economic decoder; the companion Lean proof file instead certifies short arithmetic lemmas (e.g., one-step multiplicative updates and transitivity of bounds). For HFT, we package speed as extracting spectral components faster; the machine-checked layer records inverse scaling of per-trade rents under a constant-product hypothesis in \((\rho,\text{profit})\), while the S\&P 500 / penny-stock table is illustrative calibration whose numeric anchors appear as hypotheses in the lemmas sp500_liquid_market and penny_stock_illiquid. Flash-crash discussion: if \(\rho\) drops while \(\rho\lambda\) is held fixed, \(\lambda\) rises (ratio \(\rho_{\text{normal}}/\rho_{\text{crash}}\) for the spike factor). Verification: 15 named lemmas in market_microstructure_proof.py, Lean 4 proof environment, 0 user axioms.