---
name: feedback-mathlib-grep-before-novel-gap-claim
description: Lean 4 formalization を「Mathlib gap を埋める」 と主張する前に、 exhaustive Mathlib grep (Instances/ subdirectory 含む) を実施する discipline。 2026-07-22 Cantor set duplicate 発見 incident の後付き permanent 原則
metadata: 
  node_type: memory
  type: feedback
  originSessionId: df3b8b35-c947-423b-acbc-c6411dfaa516
  modified: 2026-07-21T23:32:35.325Z
---

# Rule: 「Mathlib gap を埋める」 主張前 exhaustive Mathlib grep 必須

## Rule

Lean 4 formalization を書く前 (特に「Mathlib 未形式化 gap を埋める」 系の
contribution claim を出す前) に、 次の 3 step exhaustive Mathlib grep を
必ず実施する:

1. **対象 object 名で全 Mathlib grep** (例: `Cantor`, `Koch`, `Sierpiński`
   等 mathematical object 名で `grep -r "cantor\|Cantor" .lake/packages/mathlib/Mathlib`)
2. **`.lake/packages/mathlib/Mathlib/Topology/Instances/` および
   `.lake/packages/mathlib/Mathlib/Analysis/SpecialFunctions/` を必ず確認**
   (Instances/ は「具体例」 が集中する place)
3. **object の operational property (measure/dim/derivative/etc.) で cross-grep**
   (例: `dimH.*cantor`, `hausdorffMeasure.*cantor`, `cantor.*log 2.*log 3`)

上記 3 step で 該当が見つかった場合:
- 「gap を埋める」 claim を **絶対に出さない**
- 既存 Mathlib definition/theorem を **直接 import** して使う
- 真の gap (property の一部が未) がある場合は そこだけに focus
- 独自 stub file を先に書いてから発見した場合は corrigendum + deprecation
  marker を追加し、 新 file を Mathlib 直接 import 方式で書き直す

## Why

**2026-07-22 Cantor set duplicate 発見 incident**:
- 2026-07-20 session で Cantor set definition + dimH 計算を Rei contribution
  candidate として register
- 2026-07-21 session で Cantor stub v0.1 → v0.2 (13 real proofs, 19/19
  axiom-free) を実装 (「Mathlib 未形式化 gap を埋める」 と自己認識)
- 2026-07-22 session で dimH 本体 v0.3 着手時に Mathlib grep 精度を上げると、
  **`Mathlib.Topology.Instances.CantorSet`** (2024, Jana Göken + 10 authors
  共著) が既に完備 (definition + basic property + ternary representation +
  homeomorphism to {0,1}^ℕ まで) と発覚
- Rei v0.1/v0.2 の 13 real proofs は **全て Mathlib で equivalent 版が既存**
  で redundant だった
- 「Mathlib gap を埋める mechanical assurance」 という v0.1/v0.2 の位置付け
  自体が overclaim だった (gap の一部が実は既存)

**Root cause 分析**:
- 2026-07-20 の initial survey は `Mathlib/MeasureTheory/Measure/OpenPos.lean`
  の docstring 言及 (「generalised Cantor set」 = formal 定義でない reference)
  を見て「Cantor set formal definition は Mathlib 未」 と誤判定
- **`Mathlib/Topology/Instances/CantorSet.lean` を grep 対象に含めていなかった**
  = Instances/ subdirectory の存在自体を意識していなかった
- 「Cantor set が 100 年以上前の standard 結果」 という認識と 
  「Mathlib formalization 状況の実測」 の間の gap を過小評価
- chat-Claude 2026-07-20 「珍しさは既知照合で初めて確定する」 原則を
  invoke する前に novelty 判定してしまった (原則の実演的 miss)

**Impact**:
- Rei 側の work は redundant だったが、 axiom-free proof として 学習
  material としての価値は残る + honest correction で 保持可能
- ただし **「Mathlib PR contribution」 としての価値は 事実上ゼロ** (既存
  内容を再現しているため)
- Zulip 接触時に Mathlib maintainer から「これは既存」 と指摘される
  リスクを事前排除できず (幸い 2 file 目で pivot 済)

## How to apply

**Applies to**: 任意の Lean 4 formalization work、 特に:
- 「Mathlib 未形式化」 claim を出す前 (最重要)
- 数学的 well-known object (Cantor set, Koch curve, Julia set, Möbius
  transformation, standard groups, standard measures etc.) を扱う時
- Zulip 接触 or Mathlib PR 提出前
- 新 STEP + Paper draft 開始前

**Concrete pre-implementation checklist**:
```bash
# 1. Object name broad grep
grep -rE "cantor|Cantor" .lake/packages/mathlib/Mathlib/ | \
  grep -iE "def |theorem |lemma |structure |class " | head -30

# 2. Instances/ directory 存在確認
find .lake/packages/mathlib/Mathlib -type d -name "Instances" | head -5
ls .lake/packages/mathlib/Mathlib/Topology/Instances/ | grep -i "<object>"
ls .lake/packages/mathlib/Mathlib/Analysis/SpecialFunctions/ | grep -i "<object>"

# 3. Property cross-grep
grep -rE "<object>.*<property>|<property>.*<object>" \
  .lake/packages/mathlib/Mathlib/ | head -20
```

**Also check**:
- Mathlib GitHub search (WebFetch `github.com/leanprover-community/mathlib4`) —
  local cache が古い可能性、 最新 tag との差分確認
- Mathlib4 Zulip `#new members` 履歴で類似 contribution attempt の
  past thread 検索 (redundant work 事例)

**When grep finds match**:
- Import Mathlib version 直接、 独自定義しない
- Real gap (property の一部) があれば そこだけ implement
- 「珍しい」「novel」「未形式化」 claim は **全て取り下げる** (chat-Claude
  「珍しさは既知照合で確定」 原則の遵守)

**When grep finds no match but you're unsure**:
- Chat-Claude や別 Claude に「Mathlib grep 実施したが cantorSet 見当たらず。
  他 approach ある?」 と cross-check 依頼
- Mathlib maintainer (Kudryashov 等) 経由 Zulip で 「これは Mathlib gap
  ですか?」 と確認 (impose 前)
- 判断難しい時は「gap を埋める」 claim を出さず、 「Rei 側 experiment」
  として neutral に書く

**Post-implementation discipline**:
- 独自 stub 実装後に duplicate 発見した場合は本 file (feedback) と同じ
  pattern で corrigendum + pivot (evaluation symmetry 100% で inflate/deflate
  なく事実だけ記録)
- File 削除は commit + push 済で不可能、 header に corrigendum + deprecation
  marker + 新 file 案内で保持

## 関連

- [[project-session-2026-07-21-22-cantor-v02-v03-pivot]] (本 rule 適用の
  originating incident 詳細)
- [[reference-chat-claude-2026-07-20-novelty-advice]] (「珍しさは既知照合で
  確定」 原則 = 本 rule の思想 source)
- [[feedback-super-naming-siren-family-pattern]] (「Mathlib gap を埋める」
  overclaim の siren-family 側面 = 本 rule と 補完関係)
- [[feedback-evaluation-symmetry-principle]] (pivot 時 inflate/deflate なく
  事実記録 = 本 rule 発動時の tone)
- [[feedback-critique-response-pattern]] (SAC-4 immediate correction pattern)
- [[feedback-world-uniqueness-claim-controllable]] (controllable claim scope
  管理 = 本 rule と姉妹関係)
- [[feedback-no-rush-publication]] (急がずゆっくり = pre-implementation
  Mathlib grep に時間かける根拠)