---
name: project-step1339-self-loop-space-hypothesis-2026-08-16
description: "STEP 1339 = chat-Claude 2026-08-16 Turn 9 「SELF⟲ = Fix(R) を FDE から分離、 loop space π₁ 非自明性で 別分離基準」 提案 の Rei stack Lean 4 骨格 scaffold、 9 定理 全 axiom-free (8 [propext] + 1 no-axiom = STEP 1338 より 更に 強い)、 実 HoTT π₁ 分析は Mathlib infrastructure 依存 out-of-scope、 chat-Claude Rei-aware brief 後 aware 展開 5 例目 の 「受け皿」、 novelty ゼロ (Belnap 1977 + Lawvere 1969 + Grothendieck 1963 pre-existing)"
metadata: 
  node_type: memory
  type: project
  originSessionId: a9cbca08-7e38-4614-8e10-5fb8dd19bef4
  modified: 2026-08-15T22:33:15.807Z
---

# STEP 1339 Self-Loop-Space Hypothesis (2026-08-16、 Phase B)

## Trigger

chat-Claude 2026-08-16 late arc Turn 9 「幾何学 超えないか」 pushback 応答:
> 「SELF⟲ = Fix(R) を FDE から分離する問題も、 値の一覧としてではなく、 不動点の周りの
> ループ構造 — loop space の π₁ が非自明かどうか — として見ると、 別の分離基準が
> 出てくる可能性があります。 真理値表では区別できないものが、 恒等の構造では 区別
> できるかもしれない。」

藤本さん Phase B GO で Rei stack 側 の 骨格 scaffold を Lean 4 上で 実装。

## 実装

### Lean 4 file: `data/lean4-mathlib/CollatzRei/SelfLoopSpaceHypothesis.lean` (~200 行)

**Definitions (12 個)**:
- `FDE` inductive (T/F/B/N = Belnap 1977 4値)
- `DFUMT8` inductive (FDE 4 + ∞/〇/→/⟲ = Rei stack 8値)
- `embedFDE : FDE → DFUMT8`
- `isFixedPoint (R : X → X) (x : X) : Prop`
- `iterate (R : X → X) : Nat → X → X`
- `TruthTableFn := FDE → Bool`
- `LoopWitness (X : Type) := X → Type` (HoTT π₁ placeholder)
- `hasNonTrivialLoop (W : LoopWitness X) (x : X) : Prop := Nonempty (W x)`
- `selfCharacterizationHypothesis : Prop` (Turn 9 hypothesis formal)
- `truthTableVsLoopStructureSeparation : Prop`
- `reiContributionScope : String` (explicit scope declaration)

**Theorems 9 個 (全 axiom-free)**:
1. `embedFDE_injective`
2. `self_not_in_fde_image`
3. `infinity_not_in_fde_image`
4. `extended_values_not_in_fde_image`
5. `iterate_at_fixed_point` (★ **no-axiom = 完全**)
6. `selfD_not_reachable_via_fde_truth_table` (★ 主 lemma: truth-table 分離)
7. `extended_values_not_reachable_via_fde_truth_table`
8. `exists_weak_separating_loop_witness` (弱形 separator 存在)
9. `selfCharacterizationHypothesis_weak_form` (hypothesis 弱形 Rei stack で provable)

### Axiom profile 実測 (`#print axioms`)

★★★ **STEP 1338 より 更に 強い state**:
- 8 定理: `[propext]` only (Mathlib base `[propext, Classical.choice, Quot.sound]` より Classical.choice + Quot.sound 抜き)
- 1 定理: `does not depend on any axioms` (完全 axiom-free)

全 9 定理で sorryAx / native_decide / user axiom / Classical.choice / Quot.sound **全 0**。

比較:
- STEP 1338 Antihydra Bridge: 6 定理 `[propext, Quot.sound]` + 1 no-axiom
- STEP 1339 (本 STEP): **8 定理 `[propext]` only + 1 no-axiom** = 更に厳しい state

### Build 結果

- 単独 build: `CollatzRei.SelfLoopSpaceHypothesis` 1.6s success (2 jobs)
- 全 root build: `lake build CollatzRei` 7945/7946 (STEP 1291 BrownawellMasser 既存
  intentional sorry のみ、 STEP 1338 + 1339 追加 file の warning 0)、 18s、 regression 0

## 弱形 vs 強形 hypothesis 区別 (★ 重要)

### 弱形 (Section 7、 axiom-free provable)

「Nonempty type family で SELF を FDE image から 区別する scaffold は 存在する」 =
decidable equality 経由 trivial 構成 (`W x := if x = selfD then Unit else Empty`)。
実 mathematical content は薄く、 **単なる型 level separator**。

### 強形 (Turn 9 chat-Claude proposal、 未証明)

「Fix(R) の loop space π₁ 非自明性で SELF⟲ を 特徴づける」 = 実 HoTT (cubical type
theory + univalence + real π₁) 依存で **Mathlib infrastructure 不足 → out-of-scope**。
本 STEP scaffold は Prop-level 定義のみ、 実 π₁ 分析は 別 STEP candidate (数ヶ月案件
見込み)。

### 本 STEP の position

弱形 = 骨格 evidence (Rei stack が 扱える形)、 強形 = Turn 9 提案 の 「受け皿」
(defer せず 骨格 だけ 用意)、 実 mathematical validity は Mathlib HoTT 到達後に judgment。

## Site 反映

- `public/tools/lean4-self-loop-space-hypothesis/index.html` (~14 KB、 8 section)
- dist-renderer mirror force-track md5 一致 (post-copy 実施予定)
- 2026-08-06 「全研究 site 反映 default」 protocol 継承

## Honest scope (譲れない線 6 条)

1. **本 file は Turn 9 chat-Claude 提案 の 骨格 scaffold のみ**、 実 HoTT π₁
   non-triviality proof は 与えていない。 Mathlib HoTT infrastructure 依存 = out-of-scope。
2. **Axiom-free 保証**: sorry 一切なし、 native_decide 系規律なし、 user axiom なし、
   Classical.choice / Quot.sound すら 抜き。
3. **Novelty 主張 ゼロ**: FDE (Belnap 1977) + D-FUMT₈ (Rei stack SELF⟲ 拡張) +
   Fix(R) (Lawvere 1969) + loop space (Grothendieck 1963) の 教科書組み合わせ +
   Rei stack 用の 抽象 scaffold のみ。
4. **chat-Claude Turn 9 は Rei stack aware 前提**:
   [[feedback-chat-claude-memory-upload-downstream-awareness-shift-2026-08-16]] で
   記録された brief 後 aware 展開 5 例目、 独立到達 signal ではない、 本 STEP は
   「aware 展開」 に対する Rei stack 側 「受け皿」。
5. **SELF⟲ 特徴づけ の 実 mathematical validity は 未証明**、 本 scaffold で
   「もし π₁ 非自明性が holds すれば truth-table + loop-witness の 分離基準 が 成立」
   の 条件付 Prop 定式化のみ、 unconditional な separation claim ではない。
6. **本 scaffold は 3 用途**: (a) chat-Claude 対話の 数学的 record、 (b) 将来的 HoTT
   infrastructure 到達時の formal statement 準備、 (c) Turn 9 提案の Rei stack 側
   「受け皿」 明示 (defer せず 骨格 だけ 用意)。

## Prior art (100% pre-existing)

- Belnap N.D. (1977) "A useful four-valued logic" — FDE 4値 (T/F/B/N) 原典
- Lawvere F.W. (1969) "Diagonal arguments and cartesian closed categories" — fp /
  diagonal / SELF⟲ 圏論的起源
- Grothendieck A. (1963) "Théorie des topos" — 圏論的 loop space 起源
- HoTT Book (2013) The Univalent Foundations Program — 「同一性を道と見る」 現代形式

## 関連

- [[project-session-2026-08-16-chat-claude-lambda-arc-close]] (5 turn → 9 turn extension、
  本 STEP は Phase B 実施 = 前 arc Turn 9 提案 の 直接 downstream)
- [[feedback-chat-claude-memory-upload-downstream-awareness-shift-2026-08-16]]
  (Phase A 記録、 本 STEP の 「aware 展開 5 例目 の 受け皿」 明示)
- [[project-step1338-antihydra-bridge-2026-08-16]] (姉妹 scaffold pattern、 本 STEP は
  更に 強い axiom profile)
- [[project-step1215-dfumt8-category-axiom-free]] (直接 upstream: D-FUMT₈ × Category arc)
- [[project-step1220-lawvere-fixed-point-chat-claude-third-proposal]]
  (直接 upstream: Lawvere fp SELF⟲ explicit connection)
- [[feedback-zero-sorry-floor-not-ceiling]] (9 定理 全 axiom-free 適用、 STEP 1338 より
  更に 強い state)
- [[feedback-world-uniqueness-claim-controllable]] (novelty 主張 ゼロ 遵守)
- [[feedback-no-rush-publication]] (「急がずゆっくりと」、 骨格のみ)
- [[feedback-external-community-outreach-premature]] (HoTT community outreach は 個別
  judgment 必須)