Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings

The axiom of choice has divided the foundations of mathematics for over a century, but the distinction between classical and constructive proofs has remained a philosophical and methodological one. We use Lean 4's kernel-level tracking of axiom dependence to show that the axiom of choice has a measurable geometric correlate in proof space that obeys a one-parameter mixture law and has operational consequences for neural theorem provers. To do this, we partition 471{,}260 declarations of Mathlib by transitive dependence on the axiom of choice and represent a filtered population of 42{,}355 traced theorems by their sequences of tactic invocations. We use the constructive proofs in this dataset to train a self-supervised proof encoder and show that when using it to measure classical proofs, three complementary measurements (anomaly score, reconstruction loss, and density-superlevel containment) exhibit a common decline with the proof's distance from the axiom in the dependency graph, from sharp separation at the shallow boundary (AUC 0.847 at distance 2) to indistinguishability at distance 9{+}. Robustness controls show that the signature survives length, file, author, and topic controls, and replicates under full-source encoders trained on normalised proof source. Operationally, we show that on an evaluation sample of 251 Mathlib theorems, Lean's aesop tactic solves constructive theorems at 13\times the rate of classical ones, and a neural-guided hybrid using the ReProver tactic generator compresses the gap to 5\times. The geometric anomaly score predicts aesop failure beyond proof length, providing an operational link between the geometric signature and prover performance.