Skip to content

v1.1.0 — Interference Energy & PG1224 Formalization

Choose a tag to compare

View all tags
@egumaru egumaru released this 01 Jun 06:55
· 7 commits to main since this release
v1.1.0-interference-energy-formalization
0bfc783
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

AIKernel Prime Phase System — v1.1.0 Release Notes

Interference Energy Formalization & PG1224 Integration

概要（Summary）

v1.1.0 は、AIKernel Prime Phase System における 「Prime = Energy 0 = Stable Fixed Point」 という中心的同値性を Lean 4 上で完全に形式化し、 PG1224 素数候補生成系と統合した 初の安定版リリースです。

本バージョンは、Zenodo に公開された研究ノート：

Sogawa, T. (2026). 位相干渉エネルギーと PG1224 素数生成系の形式的構造 (v0.1.0). DOI: 10.5281/zenodo.20483437

と 1:1 で対応する実装を含みます。

主要変更点（Highlights）

1. interferenceEnergy の正式定義と意味論の確立

  • 非自明約数の個数としての干渉エネルギーを Lean で定義

  • interferenceEnergy n = 0 と「非自明約数の不存在」の同値性を証明

  • 0 と 1 の境界問題を回避するための領域条件 2 ≤ n を導入

新規定理

  • energy_zero_iff_no_nontrivial_divisors

  • interferenceEnergy_nonneg

  • interferenceEnergy_ge_one_of_has_nontrivial_divisor

2. Stable Fixed Point の定義と Prime との同値性

  • isStableFixedPoint n := 2 ≤ n ∧ interferenceEnergy n = 0 を導入

  • 素数との同値性を自然数全域で安全に証明

新規定理

  • prime_iff_energy_zero_of_two_le

  • prime_iff_stable_fixed_point

3. PG1224 素数候補生成系の形式化

  • 基数 12 / 24 の residue-class filtering を Lean で定義

  • PG1224 の soundness / completeness を証明

  • 候補生成と素数性検証の責務境界を明確化

新規定義

  • candidate12

  • candidate24

  • candidate_PG1224

  • generatesImpl_PG1224

新規定理

  • pg1224_sound

  • prime_implies_candidate_PG1224

  • pg1224_complete

4. Prime = Energy 0 = Stable Fixed Point = PG1224 の統合定理

研究ノートの中心命題を Lean で完全に形式化。

新規定理

  • pg1224_unified_equivalence

    コード

    Nat.Prime n ↔
  generatesImpl_PG1224 n ∧
  isStableFixedPoint n ∧
  interferenceEnergy n = 0

🛠 内部構造の改善（Internal Improvements）

  • ファイル構成を論文構造に合わせて整理

  • Theorems.lean に主要定理を集約

  • PG1224.lean を候補生成器として独立化

  • InterferenceEnergy.lean を意味論モジュールとして確立

  • import の循環を解消し、ビルドを安定化

  • main/dev の履歴を rebase によりクリーン化

研究ノートとの同期（Zenodo DOI）

本リリースは以下の研究ノートと完全に同期しています：

DOI: 10.5281/zenodo.20483437 https://zenodo.org/records/20483437

テストと検証

  • Lean 4 (v4.9+) で全ファイルがビルド通過

  • interferenceEnergy の境界条件（0,1,2）を含むユニットテスト

  • PG1224 の residue-class filtering の検証

  • prime_iff_stable_fixed_point の両方向の証明を確認

インストール / ビルド

コード

lake update
lake build

バージョンタグ

コード

v1.1.0 — Interference Energy & PG1224 Formalization

次のステップ（v1.2.0 以降）

  • PG1224 completeness の完全証明（残りの sorry の除去）

  • interferenceEnergy の高速化（List → Finset）

  • PG1224 の residue-class 最適化

  • 英語版研究ノート（v0.2.0）

  • AIKernel Trajectory Governance への応用モデルの拡張

まとめ

v1.1.0 は、 「素数 = 干渉エネルギー 0 = 安定固定点」 という新しい意味論的視点を Lean 4 上で完全に形式化し、 PG1224 と統合した初の安定版です。

Zenodo の研究ノートと実装が完全に同期し、 AIKernel Prime Phase System の基礎がここで確立されました。

Assets 2
Loading