---
name: Paper 128 公開完了 (Davenport Lean 4 初形式化)
description: 2026-04-22 Paper 128 を 11 platform 全公開。Davenport 定数 D(ℤ_n) + D(ℤ₂×ℤ₂) Lean 4 初形式化。DOI 10.5281/zenodo.19687156
type: project
originSessionId: ea0eb1f8-f659-4461-a674-df3f98cba941
---
# Paper 128 公開完了 (2026-04-22)

## 要約
Paper 128 「First Lean 4 Formalization of the Davenport Constant D(ℤ_n) and D(ℤ₂×ℤ₂): native_decide Certificates with EGZ Bridge」を 11 platform に全公開。Paper 127 (Schur + EGZ) の companion として、Gao 1996 の EGZ-Davenport bridge E(G) = D(G) + |G| − 1 を小値で閉じる。

## Lean 4 内容 (Step969DavenportComputational.lean)
- **11 theorems zero sorry**, 2 honest axioms
- **VERIFIED** (A.1): D(ℤ₃)=3, D(ℤ₄)=4, D(ℤ₅)=5 (Davenport 1966) + D(ℤ₂×ℤ₂)=3 (Olson 1969)
- **EMPIRICAL** (A.2): 3,472 native_decide 列挙ケース + witness
- **AXIOMATIC** (A.3): 2 axioms (davenport_cyclic_general, davenport_olson_pp)
- EGZ-Davenport bridge は `decide` で n ∈ {3,4,5} 検証

## 先行研究との関係
- Mathlib v4.27: Cauchy-Davenport (|s+t| 下界) 有 / Davenport 定数 D(G) 自体は **欠落** → 4 件すべて Lean 4 初
- Narváez-Song-Zhang formal_ramsey (CICM 2024): 2024 年以降 maintenance-only (last commit 2026-04-05)
- Paulson ITP 2025 Isabelle Diagonal Ramsey: 直交 (漸近, arXiv:2501.10852)
- Heule 2018 Schur Number Five: ACL2/Coq (Lean 4 ではない)
- **結論**: Paper 127 + 128 は 2024 CICM 境界以降の小値零和組合せ論における Lean 4 初の前進

## 公開 URL (11 platform)
| # | Platform | URL |
|---|----------|-----|
| 1 | Zenodo | https://doi.org/10.5281/zenodo.19687156 |
| 2 | Internet Archive | https://archive.org/details/rei-aios-paper-128-1776810422866 |
| 3 | Harvard Dataverse | https://doi.org/10.7910/DVN/KC56RY |
| 4 | dev.to | https://dev.to/fc0web/first-lean-4-formalization-of-the-davenport-constant-dzn-and-dz2-x-z2-nativedecide-204c |
| 5 | Hatena | https://fcwebfujimoto.hatenablog.com/entry/2026/04/22/072742 |
| 6 | HackMD | https://hackmd.io/@zCUv2P2UQHGmAOJFPLL_-A/S1hyqdBT-l |
| 7 | Notion | https://www.notion.so/Paper-128-First-Lean-4-Formalization-of-Davenport-Constant-D-_n-D-Klein-349dd371e6d9819b85a1e53572ffb6f7 |
| 8 | livedoor | https://fcwebfujimoto.livedoor.blog/archives/12887646.html |
| 9 | Scrapbox | https://scrapbox.io/rei-aios/Paper%20128 (long slug) |
| 10 | Zenn | rei-zenn repo main 7828ee7 (articles/paper-128-davenport-lean4-formalization.md) |
| 11 | Mastodon | https://mathstodon.xyz/@Fujimoto/116445054074904339 |

## コミット
- rei-aios: `3f5029d` Paper 128: First Lean 4 Davenport constant D(Z_n) + D(Klein) formalization
- rei-zenn: `7828ee7` Add Paper 128

## 並行制作
- Paper 129 (Quantum Measurement × D-FUMT₈) は draft 完成・**未公開** (藤本さん次回判断待ち)
  - papers/paper-129-quantum-measurement-dfumt8.md
  - src/axiom-os/quantum-measurement-dfumt8-engine.ts (8 解釈 ↔ D-FUMT₈ 全単射)
  - test/step970 54 passed, 0 failed
  - Copenhagen→TRUE / GRW-Penrose→FALSE / MWI→BOTH / Complementarity→NEITHER / QBism→INFINITY / Decoherence→ZERO / Bohmian→FLOWING / Wigner→SELF

## Template v3 inaugural に続く
- Paper 127 = Template v3 第 1 号
- Paper 128 = Template v3 第 2 号 (Verified 11 / Empirical 3,472 / Axiomatic 2 の三分離を継承)