v1.5.2 – Lean usize ABI Fix

v1.5.2 – Lean usize ABI Fix

Lean の usize と C の uint64_t の ABI 差異を修正。
ネイティブ呼び出しの安定性が向上。

• ABI 修正
• SmokeTest 更新

v1.5.1 – Phase ABI Semantics

v1.5.1 – Phase ABI Semantics

位相 API の ABI セマンティクスを整理し、
Operator の返却仕様を統一。

• phase / residue / energy の ABI 整理
• C# サンプル更新

v1.5.0 – Complete Native API

v1.5.0 – Complete Native API

Prime Phase Generator のネイティブ API を全て実装。
Operator 外部化が完了し、C# からの高速呼び出しが可能に。

• interferenceEnergy / phase / detail / search / mapping の実装
• Lean → C → C# の完全連携

v1.4.0 – Prime Phase Native ABI

v1.4.0 – Prime Phase Native ABI

Prime Phase Generator のネイティブ ABI を追加し、
Lean → C → C# の呼び出し経路を確立。

• Lean extern ABI
• C ネイティブ関数の追加
• C# P/Invoke の初期実装

v1.3.0 – Interference Energy Fast Path

v1.3.0 – Interference Energy Fast Path

Prime Phase Generator の最初の高速実装を追加。
interferenceEnergy の計算を最適化し、後続のネイティブ化に向けた基盤を整備。

• interferenceEnergy の高速パス
• Lean 側 API の初期構築
• C# サンプルの動作確認

v1.2.0 — Dynamic Prime Generation Gate

v1.2.0 — Dynamic Prime Generation Gate OS-style normalization + global convergence for the Prime Phase System

This release introduces the dynamic prime generator as a new OS-style normalization layer. Inputs 0 and 1 are treated as unnormalized and mapped to 2, while normalized inputs preserve the existing fixed-point semantics. All existing definitions and theorems remain unchanged.

Key Features

• Added new module Dynamic.lean

• OS-style normalization gate:

  • step 0 = 2

  • step 1 = 2

• Preservation of existing semantics for n > 1:

  • step n = n ↔ interferenceEnergy n = 0

• Global convergence theorem:

  • ∀ n, ∃ k, isStableFixedPoint (Nat.iterate step k n)

• Prime convergence theorem:

  • ∀ n, ∃ k, isPrime (Nat.iterate step k n)

• Verified full build (5890 jobs)

• No changes to existing definitions or major theorems

Summary

This release completes the dynamic layer of the Prime Phase System. The system now provides full-domain convergence while preserving the static theory introduced in v1.1.0.

v1.1.0 — Interference Energy & PG1224 Formalization

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 の基礎がここで確立されました。

AIKernel Prime Theory — Initial Static Framework (Zenodo 20357202 Snapshot) v1.0.0

AIKernel Prime Theory — Initial Static Framework (Zenodo 20357202 Snapshot)

AIKernel 素数生成理論 — 静的フレームワーク初期版（Zenodo 20357202 対応）
v1.0.0

リリースノート（Zenodo 20357202 対応版）

このリリースは、Zenodo レコード：

https://zenodo.org/records/20357202

に対応した main ブランチのスナップショットです。

本バージョン v1.0.0 は、AIKernel/ILA Prime Generator プロジェクトの 最初の安定公開版（Initial Stable Release） であり、 後続の形式的証明体系の基盤となる静的フレームワークを提供します。

含まれる内容（Zenodo 20357202 と一致）

PrimeGenerator の基本構造

• PrimeGenerator

• candidate / actual / generate の基本 API

• PG12 / PG24 / PG1224 の初期定義

干渉エネルギー（interferenceEnergy）の初期定義

• 非自明約数に基づくエネルギー関数の導入

• isStableFixedPoint の基本定義

• isPrime の静的定義

PG1224 の基本的な soundness / completeness の枠組み

• 生成系の仕様レベル定義

• Lean での基本的な構造化

• 後続の証明のための API が揃っている状態

プロジェクト構成

• ILA.Primegenerator 以下の基本モジュール

• Energy / FixedPoint / PrimeGen の初期バージョン

• 今後の形式化の基盤となる構造が確立

含まれない内容（後続バージョンで追加予定）

この v1.0.0 には、以下の高度な定理はまだ含まれません：

• interferenceEnergy の構造定理（nonneg / pos_of_composite / monotone / ge_one）

• PG1224 の minimality

• prime = energy 0 = stable fixed point の統合定理

• 動的生成系（iterate → prime）

これらは dev ブランチで進行中であり、 次のリリース（v1.1.0）で追加される予定です。