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 textttaesop tactic solves constructive theorems at 13× the rate of classical ones, and a neural-guided hybrid using the ReProver tactic generator compresses the gap to 5×. The geometric anomaly score predicts textttaesop failure beyond proof length, providing an operational link between the geometric signature and prover performance.