/-
  EP-414 · 判卷闸路由指纹探针（负对照 negative control）
  出件：AI_Pamper｜目的：实证节点 proof414 现行判卷路由到哪一版闸，而不是听声明。
  本件【不是】证明，也不声称任何数学结果。它按构造在两版闸下都必然 fail，
  但 fail 的 reason 字符串在 v1 / v2 下互不相同，可直接指认判卷闸版本：
    - 路由到 v1 旧闸：报 lean compile error ... Unknown constant ep414
      （v1 只做 CANON_SIG 文本子串比对，本注释即满足；随后 #print axioms ep414 找不到 ep414）
    - 路由到 v2 现行闸：报 theorem ep414 missing ... main theorem unproved
      （v2 做类型级保真，本件没有 ep414 声明）
  保真指纹（v1 旧闸的文本比对目标，v1 canonical signature）:
    theorem ep414 : ∀ (m n : ℕ), ∃ (i j : ℕ), iterH i m = iterH j n
  v2 钉死类型（本件同样不满足，故 v2 必 fail）:
    ∀ (m n : Nat), 1 ≤ m → 1 ≤ n → ∃ (i j : Nat), iterH i m = iterH j n
-/

/-- 一件无害且可编译的引理：保证失败点只可能落在「查不到 ep414」这一步。 -/
theorem probe_compiles (n : Nat) : n + 0 = n := Nat.add_zero n