Why Tactic-Level Rates Cannot Attribute Classical Dependencies in Lean

A proof assistant reports which axioms a theorem depends on. It does not report which step introduced them, and a proof invoking several tactics offers no way to apportion the answer. The obvious approach is statistical: score each tactic by how often its proofs carry a classical dependence the theorem did not require, and rank them. This paper reports that the approach cannot work, and gives the reason. The reason is a mismatch of random variables. Eligibility - a proof reaching Classical.choice where the statement does not - is a property of the theorem. Whether a tactic introduced that dependence is a property of the proof term. A rate conditioned on the first cannot recover the second, and the measurements show it does not. Calibration is by known-negatives: tactics that cannot introduce a classical instance, whose rate is therefore background. Across the four Lean libraries containing enough hand-written tactic proofs to measure them, that background is neither small nor constant. In Mathlib it spans 5.8 to 28.2 per cent across 30 known-negatives; in Lean core 45.0 to 100.0 per cent, with trivial at the top. rfl, which cannot introduce a classical instance, scores 16.2 per cent in Mathlib, 28.0 in Std, 48.7 in Batteries and 65.6 in Lean core. The variation is as large within a library as between them, so no normalisation recovers a threshold. Against those bands, seven candidate escapes occur across four libraries and two controls. Four belong to grind, which is not defective: it proves by refuting the negation, and refutation is classical by construction. One belongs to omega, whose classical dependence is an uncontested measurement, and simp_all ties it at exactly 100.0 per cent in the same cell. None belongs to norm_num, which sits at 5.0 per cent in Mathlib, below the known-negative floor, beneath rfl and exfalso. That last is the paper's positive result, obtained by a different method. Controlled differential construction - posing the same goal to a tactic and its alternatives and comparing axiom sets - establishes that norm_num closes numeric order goals over the naturals and integers through Classical.choice where decide and simp close them without it, by routing through a general PartialOrder lemma on types that carry DecidableEq. Equality goals are unaffected. It is a real, avoidable dependence that every rate in this paper ranks below background. A third result bounds the ambition. interval_cases scores at the top of its corpus and is innocent: its proofs close with a combinator handing the goal to norm_num, and it carries norm_num's dependence. Attribution to a surface tactic is the wrong unit regardless of the statistic. True attribution is a term-level problem, and is not solved here. Measurements cover 532,605 Mathlib theorems, three further Lean libraries, and 9,169 machine-generated proofs from the Goedel-Prover corpus. All figures derive from a single pipeline with one join rule; the accompanying archive reproduces the corpus figures with one command and no Lean, corpus download or network access.