chat-Claude 2026-08-16 late arc Turn 9 「幾何学 超えないか」 pushback 応答で 提示された 具体 research direction:
「SELF⟲ = Fix(R) を FDE から分離する問題も、 値の一覧としてではなく、 不動点の周りのループ構造 — loop space の π₁ が非自明かどうか — として見ると、 別の分離基準が 出てくる可能性があります。 真理値表では区別できないものが、 恒等の構造では 区別できるかもしれない。」
藤本さん Phase B GO で Rei stack 側 の 骨格 scaffold を Lean 4 上で 実装 (STEP 1338 Antihydra Bridge 姉妹 pattern)。
Truth-table 分離 (axiom-free provable): SELF⟲ は FDE image に 含まれない = 任意 FDE truth-table 関数 f : FDE → Bool で SELF⟲ に 到達不能。
Loop-structure 分離 (Turn 9 hypothesis、 未証明): SELF⟲ を 特徴づける Fix(R) の loop 構造 (HoTT π₁ 非自明性) が 存在するかもしれない。 「真理値表では区別できない」 という phrasing は 実 は 「FDE embedding 経由の truth-table では 区別できない」 と 読める。 「恒等の構造では 区別できる」 = fixed point の 周りの loop witness (path/homotopy 構造) 経由で 区別できるかもしれない。
-- Section 1: inductive types
inductive FDE | trueF | falseF | bothF | neitherF
inductive DFUMT8 | trueD | falseD | bothD | neitherD
| infinityD | zeroD | flowingD | selfD
def embedFDE : FDE → DFUMT8 -- FDE ↪ D-FUMT₈
-- Section 3: Fix + orbit
def isFixedPoint (R : X → X) (x : X) : Prop := R x = x
def iterate (R : X → X) : Nat → X → X
-- Section 4: truth-table
def TruthTableFn := FDE → Bool
-- Section 5: loop-witness placeholder
def LoopWitness (X : Type) := X → Type
def hasNonTrivialLoop (W : LoopWitness X) (x : X) : Prop := Nonempty (W x)
-- Section 6: Turn 9 hypothesis formal
def selfCharacterizationHypothesis : Prop :=
∃ W : LoopWitness DFUMT8,
hasNonTrivialLoop W DFUMT8.selfD ∧
∀ y : FDE, ¬ hasNonTrivialLoop W (embedFDE y)
def truthTableVsLoopStructureSeparation : Prop :=
(∀ (_f : TruthTableFn) (y : FDE), embedFDE y ≠ DFUMT8.selfD) ∧
selfCharacterizationHypothesis
embedFDE_injective — FDE ↪ D-FUMT₈ 単射性self_not_in_fde_image — ∀y:FDE, embedFDE y ≠ SELFinfinity_not_in_fde_image — INFINITY 対称的 lemmaextended_values_not_in_fde_image — 拡張 4 値全 (∞/〇/→/⟲) FDE image 外iterate_at_fixed_point — 不動点 x で ∀n, R^n(x) = x (★ no-axiom)selfD_not_reachable_via_fde_truth_table — ★ 主 lemma: truth-table 分離extended_values_not_reachable_via_fde_truth_table — 対称的 lemmaexists_weak_separating_loop_witness — 弱形 separator 存在 (decidable equality 経由)selfCharacterizationHypothesis_weak_form — hypothesis 弱形 は Rei stack で provable#print axioms)| Theorem | Axiom profile | 状態 |
|---|---|---|
embedFDE_injective | [propext] | Mathlib base 未満 |
self_not_in_fde_image | [propext] | Mathlib base 未満 |
infinity_not_in_fde_image | [propext] | Mathlib base 未満 |
extended_values_not_in_fde_image | [propext] | Mathlib base 未満 |
iterate_at_fixed_point | does not depend on any axioms | ★ 完全 axiom-free |
selfD_not_reachable_via_fde_truth_table | [propext] | Mathlib base 未満 |
extended_values_not_reachable_via_fde_truth_table | [propext] | Mathlib base 未満 |
exists_weak_separating_loop_witness | [propext] | Mathlib base 未満 |
selfCharacterizationHypothesis_weak_form | [propext] | Mathlib base 未満 |
★★★ STEP 1338 (Antihydra Bridge) より 更に強い state: STEP 1338 は 6 定理 `[propext, Quot.sound]` + 1 no-axiom、 本 STEP は 8 定理 `[propext]` only (Quot.sound すら 抜き) + 1 no-axiom。 sorryAx / native_decide / user axiom / Classical.choice / Quot.sound **全 0**。
root build regression: lake build CollatzRei 7945/7946 (STEP 1291 BrownawellMasser 既存 intentional sorry のみ、 本 STEP 追加分 warning 0)、 18s。
W x := if x = selfD then Unit else Empty)。 実 mathematical content は薄く、 単なる型 level separator。
本 STEP の position: 弱形 は 骨格 evidence (Rei stack が 扱える形)、 強形 は Turn 9 提案 の 「受け皿」 (defer せず 骨格 だけ 用意)、 実 mathematical validity は Mathlib HoTT 到達後に judgment。