Classical.choice smuggled 構成的証明のはずが Classical.choice に依存している

Error message

Lean itself emits no error. This is a policy-level detection: #print axioms on the offending theorem reveals Classical.choice in the dependency list. The compiler is entirely silent on it.

Lean 4 accepts Classical.choice as a legitimate axiom of the core standard library — it is part of Lean's trust root. But a library that advertises itself as constructive (e.g. LeanDFumt, whose 29 theorems are all closed by decide or native_decide on a finite type) cannot silently take on the choice axiom. A theorem that depends on it is no longer decide-checkable, and the promise breaks.

Minimal reproduction

-- File: BadChoice.lean
import LeanDFumt
open Classical      -- silently pulls Classical.choice into scope

namespace LeanDFumt

/-- Looks constructive; actually depends on choice. -/
theorem exists_TRUE_witness :
    ∃ a : DFUMT8, DFUMT8.toBool a = true := by
  exact ⟨Classical.choice ⟨.TRUE⟩, by decide⟩

end LeanDFumt

Build output: clean. No warning, no error. Now check the axioms:

#print axioms LeanDFumt.exists_TRUE_witness
-- 'LeanDFumt.exists_TRUE_witness' depends on axioms:
--   Classical.choice, propext, Quot.sound

The theorem compiles and looks harmless — but it is no longer part of the decide-only, no-Mathlib discipline the library advertises. Downstream code that assumed constructive availability (e.g. extracting a witness at build time) may still work, but the soundness argument has quietly shifted from "true on the finite type" to "true in classical logic."

Why it matters

Every LeanDFumt theorem in Theorems.lean and PropEmbedding.lean is closed by decide, native_decide, or rfl — tactics that reduce to a compile-time check on the eight-element finite type. This is what makes the library's soundness claim honest:

Given the axioms of Lean 4 core (excluding Classical.choice), these 29 theorems are true.

A single theorem that smuggles in Classical.choice invalidates that claim across the whole module. Because Lean does not warn, and because the polluted theorem often still admits decide-shaped tactics in other positions, the pollution can spread through a project without any interactive signal.

Fix

Rewrite the proof without Classical.choice. For existential claims on the finite DFUMT8 type, produce an explicit witness — usually one of the eight constructors:

theorem exists_TRUE_witness :
    ∃ a : DFUMT8, DFUMT8.toBool a = true :=
  ⟨.TRUE, by decide⟩

Verify the fix by re-running #print axioms:

#print axioms LeanDFumt.exists_TRUE_witness
-- 'LeanDFumt.exists_TRUE_witness' does not depend on any axioms

Also remove the open Classical line if it is no longer needed — leaving it in place is a standing invitation for the next edit to reintroduce the same bug.

If a statement genuinely requires classical reasoning and cannot be expressed on the finite type, it does not belong in LeanDFumt.Theorems. Move it to a separate module that is opted out of the constructive-check target — the same pattern used for a hypothetical Mathlib bridge library (see Mathlib dependency introduced).

Detection: CHECKER_SPEC

v0 primitive (available today — spec §4, Appendix A): not directly detectable through verify() alone. A file that silently depends on Classical.choice still compiles, so verify() returns VALID on downstream theorems. Enforcement in v0 is a pre-check that runs after compilation but before the file is admitted to stats(): for every theorem declared in the constructive-target modules (LeanDFumt.Theorems, LeanDFumt.PropEmbedding), run #print axioms <theorem> and reject the file if Classical.choice appears in any axiom list. Rejected files never enter stats(), keeping decision_rate an honest measure of what was verified under the advertised discipline rather than accepted-by-policy.

Post-v0 Layer 2 (planned — spec §13): boundary_report(kind = "classical_choice") enumerates every theorem in the project (via Lean.Environment.constants) whose transitive axiom dependencies — computed with the same algorithm used by #print axioms — include Classical.choice. Cross-check against a project-declared ConstructiveTargets.lean manifest so downstream users that explicitly opt in to classical reasoning are not falsely flagged. Layer 2 is a thin wrapper over v0 and does not introduce independent decision logic.

See also