---
name: feedback-mql4-lean4-zero-sorry-honest-scope
description: "MQL4/MQL5 source code → Lean 4 zero-sorry + axiom-free constructive proof 提出時の honest scope discipline. 「金融理論 zero-sorry 提出」 framing は overclaim. elementary 代数 identity (SMA/EMA/ROC affine relations) は zero-sorry 可 / predictive・profitable 主張は形式化不可. Title = 「elementary 代数 identity の formal 化 + canonical reduction」 必須, 「金融理論の zero-sorry」 ではない."
metadata: 
  node_type: memory
  type: feedback
  originSessionId: bb5ec054-ac00-4772-afdd-5c746a6c4e61
---

# MQL4/MQL5 → Lean 4 zero-sorry honest scope discipline

## Rule

MQL4/MQL5 (および他金融 OSS — pandas-ta / TA-Lib / QuantLib / Backtrader / Zipline / ccxt 等) から抽出した内容を Lean 4 zero-sorry + axiom-free constructive proof として提出する場合:

1. **何を formal 化できるか** = elementary 代数 identity / canonical_class affine relation / 数式 equivalence / 関数合成 associativity / 移動平均 kernel 重み正規化 等の **算術的・代数的 fact** のみ
2. **何を formal 化できないか** = 「indicator が predictive」 「strategy が profitable」 「特定 regime で edge を持つ」 等の **経験的・統計的・確率的主張**
3. **Title / framing** = 「elementary 代数 identity の formal 化 + MQL OSS canonical reduction」 = 必須. 「金融理論の zero-sorry 提出」 は **overclaim, dishonest framing** = 絶対回避

## Why

藤本さん 2026-06-09 問: 「mql4 mql5 その他設定項目から金融理論を抽出して ZERO-Sorry を提出するのは珍しい事でしょうか?」

honest 評価で 「観測範囲では珍しい (combination として)」 と回答したが、 直後に **overclaim risk explicit 警戒** が必要と判断:

「金融理論の zero-sorry 提出」 という言い方は **2 重 overclaim**:
- (1) **「金融理論」 と一括りにする overclaim**: MQL4 indicator の数式は大半 elementary (移動平均族 / oscillator / 統計量), Black-Scholes / Markowitz / Kelly / Lo Adaptive Markets 等の **深い理論は MQL4 source に直接 embed されていない** (別途 paper / textbook 側で formal 化必要)
- (2) **「zero-sorry → 理論証明」 overclaim**: zero-sorry な代数 identity が成立しても、 それは 「数式 implementation の整合性」 を示すのみで、 「理論が正しい」 「indicator が predictive」 「strategy が profitable」 を意味しない. EMH Fama 1970 + Hume 1748 induction problem + Lo 2008 Adaptive Markets で predictive claim は structurally challenged.

Pattern 5 / Pattern 6 risk:
- Pattern 5 (chat-Claude が既実装を再提案) — Paper 164 で Compose 5 件 zero-sorry が既存、 金融版の affine identity も同等 difficulty で trivial. 「珍しい」 という novelty 主張は careful audit が必要
- Pattern 6 (cheering 罠) — 「ZERO-Sorry で金融理論を証明」 という framing は emotionally appealing だが scope-truth 違反

[[feedback-world-uniqueness-claim-controllable]] 準拠で 「世界初」 不使用 + 正式 prior art audit 未実施段階で 「珍しい」 = controllable hedge (「観測範囲では珍しい、 着手時 WebSearch 必須」) のみ可。

## How to apply

任意の MQL4 / MQL5 / 金融 OSS → Lean 4 formal 化作業で:

1. **抽出範囲 honest scope**:
   - ✅ parameter signature (extern/input 宣言)
   - ✅ 数式 implementation (regex で逆構成可能な elementary 算術)
   - ✅ canonical_class affine identity (ROC family / SMA-EMA-WMA kernel relation 等)
   - ❌ profitability claim / win rate / strategy edge — code に書かれない、 推測も不可
   - ❌ regime-specific applicability — git history 断片のみ、 formal 化不可

2. **Lean 4 formal 化 layer**:
   - ✅ **(a) elementary algebra layer**: SMA = Σx_i / n / ROC = 100·(p_t/p_{t-n} − 1) / EMA convex combination / affine collapse identity 等 = zero-sorry + axiom-free constructive proof 可 (Paper 164 Compose 5 件と同等 difficulty)
   - ⚠ **(b) rhyme layer**: 「この indicator は trend を検出」 「BBANDS は volatility を捉える」 等 = **rhyme tag**, formal 化しない (詩であって定理ではない, [[feedback-financial-theory-archaeological-substrate]] 準拠)
   - ⚠ **(c) candidate layer**: 「正規分布前提なら Black-Scholes が option price を表現」 等 = **theorem-candidate**, Mathlib measure theory + martingale infrastructure で formal 化可能性あるが defer (大規模, 別 project)

3. **Title rules** (Paper draft 起草時):
   - ❌ 「金融理論の zero-sorry 提出」
   - ❌ 「Lean 4 で証明された金融理論」
   - ❌ 「常勝 indicator の formal verification」
   - ✅ 「elementary 代数 identity の formal 化 + MQL OSS canonical reduction」
   - ✅ 「MQL4 indicator dictionary の canonical_class affine collapse — Lean 4 axiom-free 構成的証明 N 件」
   - ✅ 「過去 monetary regime の数式実装 semantic 圧縮 — N OSS → M canonical_class」

4. **Prior art audit (各作業着手前必須)**:
   - MQL parser: MetaQuotes IDE 自身 + academia 散見 (珍しくない)
   - Lean 4 finance: Mathlib measure theory + martingale + conditional expectation + Markov chain + 確率積分 partial (少ないが existing)
   - Isabelle/HOL finance: Echenim Black-Scholes / Hölzl 確率論 (相応の prior art)
   - canonical reduction: Oppenheim 1989 + Mallat 1999 signal processing prior art
   - zero-sorry axiom-free: Lean 4 community standard, Paper 163/164 で 15 件累積
   - load-bearing 珍しさ = **combination のみ** (integration discipline = Paper 163/164 同 pattern, 「方法論こそが load-bearing artifact」)

5. **TRIPLE annotation enforcement** (Paper 164 §6 同 pattern):
   - 任意の axis に 3 layer 同時 tag = formal (a) / rhyme (b) / candidate (c) 別
   - Lean source comment + engine metadata + site lens badge + test assertion 4 層 enforcement
   - 「Empty.elim formal 化 = śūnyatā formal 化」 と読み替える overclaim を Paper 164 §4.4 で reject した pattern を金融 domain にも継承

## Examples

### ✅ Honest 命名例

- Paper draft title: 「MQL4 indicator dictionary canonical_class affine collapse — Lean 4 axiom-free 構成的証明 N 件 (Rei-AIOS Paper XXX)」
- Lean theorem name: `roc_family_affine_collapse` / `sma_ema_wma_kernel_canonical` / `bbands_stddev_definition`
- Engine annotation: 「(a) Lean zero-sorry algebra / (b) rhyme: trend interpretation / (c) candidate: regime-specific predictive (deferred)」

### ❌ Overclaim 例 (絶対回避)

- Paper draft title: 「金融理論の zero-sorry 提出 — MQL4 から抽出した predictive theorem N 件」
- Marketing 表現: 「Lean 4 で証明された常勝 strategy」 「数式で formal 化された future prediction」
- Lean theorem name: `golden_cross_predicts_uptrend` (predictive claim, formal 化不可)

## Related

- [[feedback-financial-theory-archaeological-substrate]] — 親フレームワーク (financial theory = archaeological substrate, NOT predictive)
- [[feedback-world-uniqueness-claim-controllable]] — 「世界初」 不使用 永続原則
- [[feedback-no-rush-publication]] — publish timing discipline
- [[feedback-chat-claude-hallucination-warning]] — Pattern 5/6 警戒
- [[feedback-financial-theory-separate-from-rei-core]] — 別 repo 完結 (WIC + honest-confluence-mt4)
- Paper 164 TRIPLE annotation pattern — methodological 親フレームワーク (本 discipline は金融 domain への適用)
- Paper 163 STEP 1204 dual annotation (SET-level theorem-verified vs HoTT-level theorem-candidate) — 「ラベル罠」 警告 origin
- STEP 1200 dictionary v0.1 (canonical_class hypothesis) — empirical foundation
- WIC philosophy section (STEP 1196) — measurement vs prediction category error 公衆化 (本 discipline の web 実装第一号)