noncomputable ghost noncomputable の定義が計算可能性の主張と共起している

Error message

Lean itself emits no error at declaration time. A mismatch surfaces only when the noncomputable definition is eventually evaluated:

failed to compile definition, consider marking it as 'noncomputable'
  because it depends on 'Classical.choice'

— or, more silently, at a #eval or native_decide that references it and fails to reduce.

noncomputable def declares a value that exists in the logic but cannot be extracted to executable code. Legitimate uses depend on Classical.choice, quotients without decidable equality, or other non-constructive machinery. A library that advertises every operation as evaluable — LeanDFumt README, "everything is decidable by by decide" — cannot carry noncomputable definitions in its default target without breaking that promise.

Minimal reproduction

-- File: BadNoncomputable.lean
import LeanDFumt

namespace LeanDFumt

/-- Looks like a normal helper; actually noncomputable because it
    consumes a Classical existential. -/
noncomputable def any_TRUE_witness
    (h : ∃ a : DFUMT8, DFUMT8.toBool a = true) : DFUMT8 :=
  Classical.choose h

theorem any_TRUE_witness_toBool
    (h : ∃ a : DFUMT8, DFUMT8.toBool a = true) :
    DFUMT8.toBool (any_TRUE_witness h) = true := by
  unfold any_TRUE_witness
  exact Classical.choose_spec h

end LeanDFumt

Build output: clean. The theorem type-checks. But the moment downstream code tries to run it:

-- In a downstream file:
#eval LeanDFumt.any_TRUE_witness ⟨.TRUE, by decide⟩
-- error: failed to reduce, definition is 'noncomputable'

example : LeanDFumt.any_TRUE_witness ⟨.TRUE, by decide⟩ = .TRUE := by
  native_decide
-- error: failed to reduce to WHNF, 'noncomputable' definition encountered

The theorem is not false — it type-checks, and its proof is valid — but every claim about the definition's value is effectively frozen. Attempts to extract a concrete answer fail, and the mismatch is only visible at the use site, not at the definition.

Why it matters

LeanDFumt's core promise is that the eight-value logic is a finite, totally-decidable structure. Every current definition in Basic.lean is fully computable, and every theorem in Theorems.lean closes by decide, rfl, or (once) native_decide on Float. Introducing a noncomputable def anywhere in the core target means the library still claims to be evaluable while containing a definition that cannot be reached at runtime.

This failure mode is particularly agent-hazardous: an agent asked to "prove this exists" may reach for Classical.choose because it is the syntactically shortest tactic, without realising that the choice imports noncomputable along with it. The resulting theorem passes review — it type-checks — and only fails later, at a call site.

Fix

Provide a concrete constructive witness. On the finite DFUMT8 type this is almost always possible by case-analysis on DecidableEq:

-- Constructive alternative — no `noncomputable`:
def find_TRUE_witness : DFUMT8 → Option DFUMT8
  | .TRUE => some .TRUE
  | .BOTH => some .BOTH
  | _     => none

theorem find_TRUE_witness_TRUE :
    find_TRUE_witness .TRUE = some .TRUE := rfl

If a definition genuinely requires classical machinery — e.g., it quantifies over an infinite type or invokes AC — it does not belong in the fully-computable core. Move it to a separate module opted out of the default target, mirroring the pattern used for the hypothetical Mathlib bridge.

Detection: CHECKER_SPEC

v0 primitive (available today — spec §4, Appendix A): partially detectable through verify(). The definition itself compiles, so verify() returns VALID on the theorem. However, any follow-up expression the agent submits that references the noncomputable value under decide, native_decide, or #eval resolves to UNDECIDED / UNSUPPORTED_SYNTAX with a failed to reduce diagnostic in detail. A concentration of that detail shape in stats().reason_breakdown.UNSUPPORTED_SYNTAX is the v0 signal that a noncomputable definition has entered the workload — treat it as a policy violation and reject the underlying module in the same pre-check pass as unsafe escape.

Post-v0 Layer 2 (planned — spec §13): boundary_report(kind = "noncomputable") enumerates every declaration in the project whose Lean.ConstantInfo is flagged noncomputable, and cross-references the call graph to identify which theorems transitively depend on it. Theorems that only type-check a noncomputable definition but never claim to compute its value (a rare pattern) are reported separately. Layer 2 is a thin wrapper over v0 and does not introduce independent decision logic.

See also