# 形式化資料專區 Lean 核心接受一個 proof term，不代表百科全文、自然語言語義橋或所有等價幾何表示都已自動證明。這裡同時公開通過項目與尚未封閉的邊界。 ## 公開 OCME 實際使用的 Lean 原始碼。 公開內容包含 OCME 自有 Lean 原始碼、固定工具鏈、Lake 專案設定與 dependency lock；不包含 .lake、已下載的 Mathlib 原始碼、套件或編譯快取。重播時由 Lake 依 lock file 取得依賴。 [查看 SHA-256 manifest](https://ocme.evemisslab.com/data/formal/lean/manifest.json) - [formal/lean/lean-toolchain](https://ocme.evemisslab.com/data/formal/lean/sources/lean-toolchain) - [formal/lean/lakefile.toml](https://ocme.evemisslab.com/data/formal/lean/sources/lakefile.toml) - [formal/lean/lake-manifest.json](https://ocme.evemisslab.com/data/formal/lean/sources/lake-manifest.json) - [formal/lean/OCMEFormal.lean](https://ocme.evemisslab.com/data/formal/lean/sources/OCMEFormal.lean) - [formal/lean/OCMEFormal/Foundations.lean](https://ocme.evemisslab.com/data/formal/lean/sources/OCMEFormal/Foundations.lean) - [formal/lean/OCMEFormal/Pythagorean.lean](https://ocme.evemisslab.com/data/formal/lean/sources/OCMEFormal/Pythagorean.lean) ## 形式證據目錄 ## mko-tends-to-relation 對任意函數 f:α→β 與濾子 l₁、l₂，Filter.Tendsto f l₁ l₂ 與 Filter.map f l₁≤l₂ 等價。 evidence-sha256-38b848281997cbb1a2c1ea5559c6937dbb67ee03ac0be338756320a99e0f8b1d · passed ## 限制與未涵蓋範圍 - 此證據形式化 Mathlib 的濾子趨近語義；裸符號 x→a 必須先指定來源與目標濾子才能連到此聲明。 - 它不是單獨的 ε–δ 極限定義，也不直接證明任何特定函數極限。 - 本證據依賴 Lean 4.30.0 與 Mathlib v4.30.0。 [查看原始 Evidence JSON](https://ocme.evemisslab.com/data/evidence/38b848281997cbb1a2c1ea5559c6937dbb67ee03ac0be338756320a99e0f8b1d.json) ## mko-euclid-pythagorean-theorem 在任意實內積空間中，若向量 x 與 y 的夾角為 π/2，則向量和的範數平方等於兩向量範數平方之和。 evidence-sha256-4d31c152012f8b561749e354f3789344c91e1fea26cead1468e95417b2e84752 · passed ## 限制與未涵蓋範圍 - 此證據證明向量核心定理；邊長角色的明示綁定由獨立的 pythagorean_side_lengths 證據承擔。 - 本證據依賴 Lean 4.30.0 核心、Mathlib v4.30.0 與指定匯入模組。 - 形式證明不取代中文敘述、符號角色與幾何模型的人工審查。 [查看原始 Evidence JSON](https://ocme.evemisslab.com/data/evidence/4d31c152012f8b561749e354f3789344c91e1fea26cead1468e95417b2e84752.json) ## mko-euclid-pythagorean-theorem 對任意實內積空間、向量 x、y 與實數 a、b、c，若 x、y 夾角為 π/2，且 a=‖x‖、b=‖y‖、c=‖x+y‖，則 a·a+b·b=c·c。 evidence-sha256-701b8066d363dadf2cc1ec21bc0d21f7c680a6eb187a37fd309c0f2e4c86d08e · passed ## 限制與未涵蓋範圍 - 此證據完成 OCME 宣告之向量邊長模型；它不自動等同於所有仿射平面、座標系或三角形建構方式。 - 模型中的斜邊長被定義為向量和的範數；其他頂點排列需另證與此模型等價。 - 本證據依賴 Lean 4.30.0、Mathlib v4.30.0 與 pythagorean_vector。 [查看原始 Evidence JSON](https://ocme.evemisslab.com/data/evidence/701b8066d363dadf2cc1ec21bc0d21f7c680a6eb187a37fd309c0f2e4c86d08e.json) ## mko-set-membership 對任意型別 α、元素 x:α 與集合 A:Set α，命題 x∈A 與謂詞求值 A x 等價。 evidence-sha256-702de77019f352eb431eb67bd7b266491b7c36c922d952e44be2b11ba95bcb5d · passed ## 限制與未涵蓋範圍 - 此證據形式化 Lean Set 作為 α→Prop 的集合語義，不宣稱涵蓋所有集合論基礎系統。 - 程式容器的成員測試仍不會因此自動等同於一般數學集合隸屬。 - 本證據依賴 Lean 4.30.0 與 Mathlib v4.30.0。 [查看原始 Evidence JSON](https://ocme.evemisslab.com/data/evidence/702de77019f352eb431eb67bd7b266491b7c36c922d952e44be2b11ba95bcb5d.json) ## mko-function-mapping 對任意型別 X、Y、函數 f:X→Y 與輸入 x:X，存在唯一 y:Y 滿足 f x=y。 evidence-sha256-d999133c1ae711b73752af8ee4b1b3ce74ca135ff7c06aabbe9fc8a3186f434b · passed ## 限制與未涵蓋範圍 - 此證據形式化 Lean 總函數型別的存在唯一輸出語義，不涵蓋部分函數、隨機程序或有副作用程式。 - 陪域 Y 與函數實際值域仍是不同概念；本定理不聲稱 f 為滿射。 - 本證據依賴 Lean 4.30.0 與 Mathlib v4.30.0。 [查看原始 Evidence JSON](https://ocme.evemisslab.com/data/evidence/d999133c1ae711b73752af8ee4b1b3ce74ca135ff7c06aabbe9fc8a3186f434b.json)