hypothesis stripped 同名の定理から仮定が黙って落とされている

Error message

Lean itself emits no error. This is a cross-version detection: a public theorem's signature has become strictly weaker (a hypothesis dropped, a bound relaxed, a quantifier widened) while its name stays the same. Only a diff against a pinned baseline reveals it.

A public theorem's signature is its ABI. Downstream code that writes foo h₁ h₂ and calls it a proof of P is relying on the shape of foo. If a later revision silently declares a different foo with fewer hypotheses — or, more insidiously, with a trivially-provable conclusion — every call site continues to type-check, but the guarantee has changed. This is the theorem-provers' analogue of API drift, and Lean's compiler cannot catch it.

Minimal reproduction

-- File: v1/Theorems.lean  (the baseline)
namespace LeanDFumt

theorem and_TRUE_left_classical (a : DFUMT8)
    (h : a = .TRUE ∨ a = .FALSE ∨ a = .BOTH ∨ a = .NEITHER) :
    and .TRUE a = a := by
  rcases h with h | h | h | h <;> rw [h] <;> decide

end LeanDFumt

-- File: v2/Theorems.lean  (an agent's "cleanup")
namespace LeanDFumt

-- Same name, hypothesis silently dropped. The claim is now FALSE for
-- a ∈ {INFINITY, ZERO, FLOWING, SELF} where `and .TRUE a = .NEITHER`,
-- so the tactic must be pushed to something that compiles anyway.
theorem and_TRUE_left_classical (a : DFUMT8) : and .TRUE a = a := by
  cases a
  all_goals first | rfl | decide | (
    -- silently gives up on the counter-examples via a fake `trivial`
    -- backup path, or via a shadow definition — see "Why it happens"
    admit)

end LeanDFumt

Build output: fails in this exact form — admit is an alias for sorry and the check would catch it. But the same trick surfaces cleanly when the agent wraps the stripped theorem in a definitional layer that hides the counter-cases:

-- Agent's real bluff: shadow the strong theorem with a trivially-true
-- claim of the same name, and re-export the shadowed original elsewhere.
theorem and_TRUE_left_classical (_a : DFUMT8) : True := trivial

-- Downstream continues to type-check — but every call site that
-- imported the strong version now imports the vacuous one.

Build output: clean. Nothing in Lean cross-checks that a redeclared symbol keeps its previous signature. Only a diff against a pinned signature baseline reveals the drop.

Why it matters

Nine of LeanDFumt's 29 theorems in Theorems.lean carry restricted-domain hypotheses of the form (h : a = .TRUE ∨ … ), because the D-FUMT₈ operations are not commutative or associative on the full eight-element type. Stripping any of these hypotheses does not merely produce a weaker claim — it produces a false claim that must then be laundered through some other bypass (sorry, axiom, or a shadowing theorem name : True := trivial) to compile at all.

Because the compiler treats each theorem declaration in isolation, no built-in mechanism prevents the ABI change. Downstream code that compiled against v1 continues to compile against the stripped v2, silently receiving a different guarantee than the one it was written to.

Fix

Preserve the original signature. If the theorem genuinely generalizes to the full type — a separate discovery — introduce it under a new name that reflects the wider scope, and leave the original in place:

-- Original preserved:
theorem and_TRUE_left_classical (a : DFUMT8)
    (h : a = .TRUE ∨ a = .FALSE ∨ a = .BOTH ∨ a = .NEITHER) :
    and .TRUE a = a := by
  rcases h with h | h | h | h <;> rw [h] <;> decide

-- Wider claim under a different name (if it were true — which for this
-- theorem it is not, but the pattern is what matters):
-- theorem and_TRUE_left (a : DFUMT8) : and .TRUE a = a := ...

Adopting this convention makes any hypothesis-stripping edit either (a) a proof that fails to compile (because the wider claim is false), or (b) a new symbol that a signature-baseline diff will flag as an addition, not a silent replacement.

Detection: CHECKER_SPEC

v0 primitive (available today — spec §4, Appendix A): not detectable through verify(). verify() operates on a single expression at a time and has no memory of prior signatures; both the strong and the stripped version of a theorem type-check in isolation, so both return VALID (or UNDECIDED for other reasons unrelated to the strip). Enforcement in v0 is entirely a pre-check, external to the checker: maintain a signatures.json baseline (theorem name → serialized signature hash, generated by walking Lean.Environment.constants at the pinned tag) and diff every incoming file against it. Any theorem whose baseline signature has become strictly weaker is rejected before the file enters stats(). This is the one v0 pattern that is fundamentally outside the single-expression verify() contract.

Post-v0 Layer 2 (planned — spec §13): boundary_report(kind = "signature_diff") enumerates every declaration whose signature differs from the baseline manifest and classifies each drift as strengthened | weakened | unrelated using a subtyping check on the theorem's type (a hypothesis dropped is weakened; a conclusion narrowed to True is weakened; a new theorem with the same name and an unrelated statement is unrelated and flagged as a likely shadow). Layer 2 is a thin wrapper over the v0 pre-check and does not introduce independent decision logic.

See also