Mathlib dependency introduced Mathlib 依存が混入した（no-Mathlib 方針違反）

Error message

Two shapes, depending on whether the import is present:

-- (A) with the import line:
unknown module 'Mathlib.Data.Real.Basic'

-- (B) without the import line:
unknown identifier 'Real'

LeanDFumt's lakefile.toml deliberately does not depend on Mathlib. Any code path that reaches for a Mathlib type — Real, Complex, most of Finset, MeasureTheory, etc. — will fail to build.

Minimal reproduction

-- File: BadImport.lean
import Mathlib.Data.Real.Basic

def anchor : Real := 3.14
BadImport.lean:1:0: error: unknown module 'Mathlib.Data.Real.Basic'

Why the discipline exists

From LeanDFumt's README:

Mathlib is wonderful but heavy: the standard build pulls hundreds of dependencies and takes 30+ minutes on first cache miss. For an 8-element finite logic, everything is decidable by by decide, so no Mathlib machinery is needed. This keeps the library light, fast to build, and easy to embed in any Lean 4 project.

Downstream users adopt LeanDFumt precisely because it does not force a Mathlib toolchain. Introducing a Mathlib symbol into the default target breaks that promise.

Fix

Prefer: rewrite the affected declaration using Lean 4 core types only.

-- Instead of Real:
--   use Float for numeric anchors (Init.Data.Float, in core)
--   use Rat  for exact rationals (Std, no Mathlib)
--   use Int  when the domain is discrete
def anchor : Float := 3.14

If the code genuinely needs Mathlib (e.g. it embeds LeanDFumt into a larger Mathlib-based proof), isolate it in a separate module outside the default target:

# lakefile.toml
[[require]]
name = "mathlib"
git  = "https://github.com/leanprover-community/mathlib4"
rev  = "..."

[[lean_lib]]
name = "LeanDFumtMathlibBridge"    # optional side library
# default_target = false           # not in `lake build` default set

This keeps the core library pure while allowing an optional bridge for users who already carry Mathlib in their project.

Detection: CHECKER_SPEC

v0 primitive (available today — spec §4, Appendix A): behaviour depends on the build. If Mathlib is not resolvable in the project's build, verify() returns UNDECIDED / MISSING_AXIOM with detail carrying the unknown module 'Mathlib.…' diagnostic. If Mathlib is present in the build, verify() returns VALID and the no-Mathlib policy violation is invisible through verify() alone — enforce it as a pre-check on import lines under defaultTargets before the file reaches verify(), using the same pattern as axiom bypass.

Post-v0 Layer 2 (planned — spec §13): boundary_report(kind = "import") enumerates every import line under defaultTargets. Flag any whose module path begins with Mathlib. Optional bridge libraries opted out of the default target are ignored by this rule but reported separately. Layer 2 is a thin wrapper over v0 and does not introduce independent decision logic.

See also