MLP Set Functions Are Interaction-Dominated: A Möbius Decomposition of Neuron Subsets in GPT-2 and Pythia-160m, with Lean-Formalized Set-Function Theory

Attribution methods for language models overwhelmingly report additive, per-component contributions. We measure how much of the function an MLP layer actually computes over subsets of its neurons such reports leave out. For a prompt and a target token, define f(A) as the log-probability of the target when exactly the intermediate neurons in A of one MLP layer remain active and the rest are ablated. Enumerating all 2^10 subsets of 10-neuron sets — exhaustively, not by sampling — in GPT-2 small and Pythia-160m, we decompose f by Möbius inversion and find that interaction terms of order ≥ 2 carry the majority of the coefficient mass (GPT-2: 57% and 63% at layers 5 and 10; Pythia-160m: 74–78%), and the error of the modular (separable) approximation f̂ averages 43–48% of f's range over the subset lattice in GPT-2 and 18% in Pythia-160m. The finding is robust across neuron-set selection rules (shared and per-prompt top-activation sets, with random controls), across GPT-2 layers 1–10 (easing at the final layer), under zero ablation and, attenuated, under mean ablation, and across target types (the model's own argmax and curated correct answers); under the Shapley symmetrization of the same coefficients, the interaction ratio is 0.495 — at parity with the singleton terms — so the conclusion does not hinge on the unsymmetrized coordinates. The set-function theory used — Möbius inversion, the characterization of modularity by vanishing higher-order coefficients, the exact decomposition of a set function into a modular approximation plus a higher-order tail, and its stability bound — is classical; we contribute a machine-checked formalization in Lean 4 / Mathlib, audited at the level of axiom dependencies: every theorem cited here depends only on the standard axioms, and the core development assumes no monotonicity, normalization, or nonnegativity of v. That generality is necessary, because measured f is a signed set function, not a fuzzy measure: monotonicity fails on 42–49% of comparable pairs (GPT-2) and the full neuron set scores below the empty set in 7 of 24 cases. The measured decomposition is, numerically exactly (max discrepancy 0.0 in float64), the decomposition the formalization proves. The implication is scoped but load-bearing: an additive per-neuron account of these set functions reports f̂, and the tail it discards is a fifth to a half of the function's range.