---
name: project-task20-self-reflexive-preservation-lean4-2026-07-24
description: "Task 20 (Priority H2) 実装完了 — SELF⟲ preservation under Verilog encoding の Lean 4 formal encoding。 STEP 1264 直接拡張、 22 theorem 全 axiom-free、 [propext] 系のみで完成。 Paper 145 v0.9-d §D.3 SELF⟲ 準同型条件 の 学術本命 gap を close。"
metadata: 
  node_type: memory
  type: project
  originSessionId: c8cfa2f8-dec7-4129-956e-9c099830ec42
  modified: 2026-07-24T03:36:58.949Z
---

## Task 20 完了記録 — SELF⟲ preservation under encoding

2026-07-24 (chat-Claude arc 21 turn Phase 1-6 完了後の 直後 arc)、 藤本さん選択 α で **Task 20 = Priority H2 の 最 load-bearing candidate** 着手 → 完成。

## 実装 file

`data/lean4-mathlib/CollatzRei/PhaseC/Dfumt8SelfReflexivePreservation.lean` (~310 行 10 section)

`data/lean4-mathlib/Dfumt8SelfReflexivePreservationAxiomCheck.lean` (axiom profile artifact, Rei convention 準拠)

## 動機 (chat-Claude arc 21 turn 由来)

chat-Claude arc 21 turn (2026-07-24) の 「回路の 表現力 と 一様性制約 の 緊張関係」 精査で、 学術本命 として identified された gap:

> 「意味論的性質 (SELF⟲ の 不動点性 等) が 符号化 の 下で 保存される」 → 準同型条件 として 証明すべき 命題 【仮説】

STEP 1264 (2026-07-09) で AND / OR 64-entry の refinement (準同型) は close 済 (16/18 zero-axiom + 2 [propext])。 SELF⟲ (ADIABATIC) が 残る 3 番目 primitive で、 本 file で close。

## Verilog 対応 (source of truth)

`data/verilog/dfumt8_alu.v` (STEP 1006) の ADIABATIC clause:

```verilog
ADIABATIC: begin
  case (a)
    3'b110: adiabatic_result <= 3'b110;  // SELF -> SELF (explicit)
    default: adiabatic_result <= a;       // others -> passthrough
  endcase
end
```

両 clause は functional に 同 (identity)、 だが **explicit case が SELF⟲ (Fix(R)) の primitive marker**。 本 file は 両 semantic marker + functional refinement 双方 formalise。

## 10 section 構成

| Section | 内容 | 主要 theorem |
|---|---|---|
| 1 | Bit-level ADIABATIC | `aluAdiabaticBits : Nat → Nat` |
| 2 | Refinement square | `aluAdiabatic_refines` — 符号化 が ADIABATIC と commute |
| 3 | SELF⟲ bit-level fixpoint | `aluAdiabaticBits_self : aluAdiabaticBits 6 = 6` + `selfReflexive_refines` |
| 4 | Universal fixpoint | 意味論 + bit-level (per-code 6 theorem + universal with `interval_cases`) |
| 5 | Explicit vs default case discrimination | `AdiabaticCase` inductive (`ReflexiveCase` / `PassThroughCase`) + `aluAdiabaticCase` / `aluAdiabaticCaseBits` |
| 6 | Case-refinement bijection | `adiabaticCase_refines` — marker が encoding 経由で 保存 (**非自明 load-bearing content**) |
| 7 | Composition preservation | `aluAdiabaticBits_idem` + `aluAdiabaticCase_idem` |
| 8 | STEP 1264 pattern 一貫性 | consistency check |
| 9 | 合成 preservation bundle | `self_reflexive_preservation_bundle` + `..._at_SELF` |
| 10 | Smoke tests | 9 example |

## Axiom profile 実測 (`lake env lean Dfumt8SelfReflexivePreservationAxiomCheck.lean`)

- **22 theorem 全**
- **sorryAx / native_decide / user axiom 全 0**
- **1 完全 zero-axiom**: `selfBits_triggers_reflexive` (does not depend on any axioms)
- **19 theorem `[propext]` のみ**: refinement / case discrimination / smoke tests / bundle
- **2 theorem `[propext, Classical.choice, Quot.sound]`**: `aluAdiabaticBits_universal_fixpoint` + `aluAdiabaticBits_idem` (`interval_cases` 使用のため)

= STEP 1264 baseline (16/18 zero-axiom + 2 [propext]) と 同格 強状態。

## Build

```
lake build CollatzRei.PhaseC.Dfumt8SelfReflexivePreservation
✔ [775/775] Built ... (7.4s)
Build completed successfully (775 jobs).
```

## Load-bearing content

3 layer preservation:

1. **Functional refinement** (Section 2): `(aluAdiabatic x).toBits = aluAdiabaticBits (x.toBits)` — 符号化 経由で 値 保存
2. **Semantic marker preservation** (Section 6): `aluAdiabaticCase x = aluAdiabaticCaseBits (x.toBits)` — **explicit case (SELF) vs default (passthrough) の 区別 が 符号化 経由で 保存** (非自明)
3. **Fixpoint universality** (Section 4): 両 level で universal fixpoint (aluAdiabatic は identity)

Section 6 が chat-Claude 指摘の 学術本命。 SELF が **distinguished fixpoint** (Verilog 明示 case) で、 他の値は 「incidentally fixed」 (default fall-through)。 この区別が bit encoding で 保存されることを formal 証明。

## Honest scope

- 意味論的 preservation の formal proof。 Verilog RTL vs silicon 動作 は 別 substrate (Paper 145 §B.8.1 empirical evidence)
- `aluAdiabatic` は 意味論的 identity なので `Fix(aluAdiabatic) = Dfumt8` universe = 値 level では trivial
- **非 trivial content = Section 5-6 の case discrimination** (Verilog case block 構造 の Lean 4 型化)
- Lawvere 1969 fixed-point theorem (SelfLawvereBridge.lean STEP 1203) は 60 年 prior art。 本 file は **implementation-semantics refinement layer** で、 Lawvere theoretical layer と orthogonal
- 「世界初」 不使用、 「SELF⟲ concept の novelty」 も claim せず。 novelty は Verilog explicit-case marker の Lean 4 formalisation のみ

## Paper 145 v0.9-d への 反映 candidate

- §D.3 clone theory の 「SELF⟲ = Fix(R) の FDE からの分離 → clone として 別位置」 の Lean 4 formal encoding = 本 file `AdiabaticCase` + `adiabaticCase_refines`
- §D.4 D-FUMT₈ ESN の 「Fix(R) = リザバー機能条件 = SELF⟲ operational instance」 と bridge (別 STEP candidate)
- v0.9-d full draft で `self_reflexive_preservation_bundle` を §D 主定理として引用可能

## Rei stack 位置づけ

- STEP 1011 unary refinement (aluNot / aluOmega / aluPhi / aluPsi)
- STEP 1264 binary 64-entry refinement (aluAnd / aluOr, F3 closure)
- **本 STEP unary refinement (aluAdiabatic, SELF⟲ preservation)** ← Task 20 完了
- **残 primitive**: aluXor / aluReset は STEP 1011 で refinement 済み (`aluXor_refines` / 明示 refinement は Xor は STEP 1011 内、 Reset は constant law のみ)

## 関連

- STEP 1011 Dfumt8AluRefinement.lean (unary refinement baseline)
- STEP 1264 Dfumt8Binary64Refinement.lean (binary refinement F3 closure, 本 STEP の 直接 pattern 継承)
- STEP 1203 SelfLawvereBridge.lean (SELF⟲ theoretical layer, 本 file の orthogonal counterpart)
- STEP 1215 Dfumt8CategoryExperiment.lean (D-FUMT₈ category axiom-free)
- Paper 145 v0.9-c (Zenodo DOI 10.5281/zenodo.20192813, 現行 stable)
- Paper 145 v0.9-d outline (2026-07-24 §D.3 SELF⟲ 準同型条件)
- chat-Claude arc 21 turn (2026-07-24)
- [[project-chat-claude-arc-21turn-adopt-priority-2026-07-24]] (Priority H2 Task 20 記録)
- [[reference-dfumt8-reservoir-prior-art-audit-2026-07-24]] (Phase 5 audit)
- [[feedback-theory-to-circuit-scope]] (回路 scope 精査)
- Load-Bearing Invention #5 「STEP(t₀) ← EternalRei(t₊∞)」