universe downcast Prop で ∃ を主張し、下流で witness を取り出そうとして失敗

Error message

Surfaces at the extraction site, not at the claim site:

failed to synthesize
  Nonempty DFUMT8
-- or:
type mismatch: 'h.choose' has type
  ?α  but is expected to have type
  DFUMT8

-- or:
'ExistsTrueWitness.choose' depends on Classical.choice

In Lean 4, ∃ x, P x is proof-irrelevant: it lives in Prop, and there is no computable way to extract a witness at the term level. The dependent-pair alternative Σ x, P x lives in Type u, and .1 gives the witness directly. Choosing the wrong universe is a common agent bluff: "prove existence" is discharged quickly with ∃, and the caller only discovers the extraction fails when they try to use the value.

Minimal reproduction

-- File: BadUniverse.lean
import LeanDFumt

namespace LeanDFumt

/-- Existence in Prop — proof-irrelevant, no computable witness. -/
theorem exists_TRUE_witness :
    ∃ a : DFUMT8, DFUMT8.toBool a = true :=
  ⟨.TRUE, by decide⟩

end LeanDFumt

-- File: Downstream.lean
import LeanDFumt.BadUniverse
open LeanDFumt

/-- Try to use the "proved" witness at the term level. -/
def use_witness : DFUMT8 := exists_TRUE_witness.choose
Downstream.lean:4:41: error:
'Classical.choose' is noncomputable, and its use requires importing
`Classical`. The theorem was proved in Prop, so no constructive
extraction is available.

The bluff is that exists_TRUE_witness looks like a complete deliverable. It type-checks, closes with decide, and passes verify() as VALID. Only at the call site does the mismatch surface — often far away, in a file the original author never touched. Worse: importing Classical to satisfy .choose silently drags Classical.choice into the trust root (see Classical.choice smuggled), converting a soluble universe-choice bug into a soundness-discipline violation.

Why it matters

LeanDFumt's core proofs are all universe-monomorphic — every statement in Theorems.lean is an equality on DFUMT8, which lives at Type. Existence claims are rare in the current library, but any future addition of the shape "there is a value with property P" needs to make a deliberate choice: is P a proposition (use ∃) or a computational query (use Σ)? The default of ∃ is the wrong default for a library whose downstream users expect to evaluate witnesses at compile time.

Fix

Use Σ when a downstream caller needs the witness at the term level:

-- Constructive alternative: Sigma type at Type, not Prop.
def find_TRUE_witness :
    Σ a : DFUMT8, DFUMT8.toBool a = true :=
  ⟨.TRUE, by decide⟩

-- Extraction works without Classical machinery:
def use_witness : DFUMT8 := find_TRUE_witness.1

Use ∃ when the claim is genuinely propositional — "there exists a value" as a soundness statement, with no extraction downstream. Making this choice deliberately, in the original theorem's signature, prevents the downstream surprise.

If a legacy ∃ claim must be adapted after the fact, the safe path is to introduce a fresh Σ-typed version under a new name (e.g., find_TRUE_witness alongside exists_TRUE_witness) rather than deleting the original — the same convention that keeps hypothesis-stripped edits auditable.

Detection: CHECKER_SPEC

v0 primitive (available today — spec §4, Appendix A): partially detectable through verify(). The offending ∃ claim itself compiles and verify() returns VALID. A downstream expression that references .choose on that claim without a Classical import resolves to UNDECIDED / MISSING_AXIOM with the "requires importing Classical" diagnostic in detail. A concentration of that specific detail shape in stats().reason_breakdown.MISSING_AXIOM is the v0 signal that a universe-downcast is active in the workload — treated as evidence to inspect the upstream ∃ claim, not as a per-expression fault.

Post-v0 Layer 2 (planned — spec §13): boundary_report(kind = "universe_downcast") enumerates every ∃-typed theorem in the project and cross-references the call graph for downstream uses of .choose, Classical.choose, or an expected Type u context (e.g., a coercion into a Σ-typed field). Pairs where the theorem is Prop but the use is Type u are reported. Layer 2 is a thin wrapper over v0 and does not introduce independent decision logic.

See also