---
name: reference-toshnotation-6glyph-2026-06-29
description: "ToshNotation = chat-Claude 2026-06-29 設計の 6 glyph proof obligation 体系 (↔ Rev / ⇝ Approx / ↯ Irrev / ⊥ Collapse / ⊢ Entail / ⟲ SelfRef)。 2 軸構造 (情報保存 ↔⊐⇝⊐↯⊐⊥ / 導出再帰 ⊢ ⟲)。 Lean 4 implementation `data/lean4-mathlib/CollatzRei/ToshNotation.lean` で 2 main theorem 完全 zero-axiom verify 済。 Rei 既存 artifact (Paper 61 ZCSG / Paper 168 v0.4 / STEP 1220 Lawvere FP / Paper 173 形は絶対底は空) と integration 済。"
metadata: 
  node_type: memory
  type: reference
  originSessionId: af1ab23c-b41d-4c41-9589-65cdb46779f8
---

# ToshNotation — 6 glyph proof obligation system

## 概要

**ToshNotation** = 藤本 伸樹 (Toshi from 「藤本」 → tosh) 由来命名の 6 glyph 記号体系、 chat-Claude (web session, 2026-06-29) 設計 + Rei (本 session 2026-06-30) Lean 4 axiom-free verify。

## 6 glyph 対応表

| Glyph | 名前 | 質 | Lean 4 proof obligation | Witness |
|---|---|---|---|---|
| **↔** | Rev | 可逆 (情報損失 0) | `structure Rev` with two-sided inverse | `(inv, left, right)` |
| **⇝** | Approx | 近似 (誤差 ≤ ε) | `Approx d f g ε := ∀ a, d (f a) (g a) ≤ ε` | ε と上界証明 |
| **↯** | Irrev | 不可逆 (非単射) | `∃ a₁ a₂, a₁ ≠ a₂ ∧ f a₁ = f a₂` | 相異 (a₁, a₂) と f での衝突 |
| **⊥** | Collapse | 崩落 (像 1 点) | `∃ b, ∀ a, f a = b` | 定点 b と全 a での等式 |
| **⊢** | Entail | 接続 (Curry-Howard) | `P → Q` | 証明項 (proof term) |
| **⟲** | SelfRef | 自己言及 (Lawvere FP) | `∃ a, f a = a` | 不動点 a |

## 2 軸構造

### Axis 1: 情報保存軸

```
↔  ⊐  ⇝  ⊐  ↯  ⊐  ⊥
損失 0 → 有界 → 離散 → 全崩落
```

### Axis 2: 導出・再帰軸

```
⊢ (証明項, Curry-Howard) / ⟲ (不動点, Lawvere)
```

## 軸の閉性 (Lean 4 axiom-free verify 済)

```lean
theorem rev_not_irrev {A B : Type} {f : A → B} (r : Rev f) :
    ¬ Irrev f
-- "Reversible implies not Irreversible" (↔ excludes top)
-- ✅ does not depend on any axioms

theorem collapse_imp_irrev {A B : Type} {f : A → B}
    (hc : Collapse f) (h2 : ∃ a₁ a₂ : A, a₁ ≠ a₂) :
    Irrev f
-- "Collapse + ≥ 2 source points implies Irreversible" (⊥ ⟹ ↯)
-- ✅ does not depend on any axioms
```

両 theorem とも **完全 zero-axiom** (`does not depend on any axioms`) = Rei CollatzRei tree 内最 strict tier (STEP 1241 D-FUMT₈ FDE sub-algebra と同 level)。

## File 配置

| File | 役割 |
|---|---|
| `data/lean4-mathlib/CollatzRei/ToshNotation.lean` | 6 glyph definitions + 2 main theorems (chat-Claude design + Rei verify) |
| `data/lean4-mathlib/CollatzRei/Step1244ZcsgToshNotationBridge.lean` | ZCSG × ToshNotation bridge (10/10 zero-axiom) |
| `data/lean4-mathlib/CollatzRei/Step1245FrameChecksum.lean` | Frame integrity check + rotation litmus (5/7 zero-axiom + 2/7 [propext]) |

## Design 判断 (chat-Claude 2026-06-29)

### ⊢ の Gentzen turnstile 衝突 resolution

⊢ は Gentzen turnstile (標準: 導出可能、 provability) として広く認知。 ToshNotation の 「接続」 とは厳密には別義。 chat-Claude の解決:

> 「接続 = 導出のつながり、 と読めば標準義と矛盾しません」

= **同じ向きで定義し吸収**。 strict 区別が必要な context では別 glyph (例: `⊸` linear logic, `⥬` chain link) 推奨。

### ⊥ の falsum 衝突

⊥ は古典論理 falsum (false / 矛盾) として標準。 ToshNotation の 「崩落」 = 全崩落 = 像が 1 点 = 情報損失 maximum。 これは falsum に近い (1 値に collapse) ため **吸収可能**。

### ⟲ ↯ ⇝ ↔ は標準義緩い

これらは prior art (linear types, effect systems, category theory) で多様な使い方あり、 ToshNotation 義は **自由に定義可能**。

## Rei existing artifact との接続

| Artifact | 接続点 |
|---|---|
| **Paper 61 ZCSG** | ZCSG 中心 0 = SELF⟲ = ⟲ 不動点、 STEP 1244 で `constO_selfref` zero-axiom verified |
| **Paper 168 v0.4 空の器** | śūnyatā field = 関係的 = ToshNotation の relational view |
| **Paper 171 Cotnoir recapture** | Madhyamaka 4-corner ↔ D-FUMT₈ 4 拡張軸 (TRUE/FALSE/BOTH/NEITHER), ToshNotation の D-FUMT₈ 接続 |
| **Paper 39 (本日 publish)** | SELF⟲ Hard Problem of Consciousness、 ⟲ glyph の哲学的 anchor |
| **STEP 1220 Lawvere FP** | ⟲ proof obligation の formal foundation (Lawvere 不動点定理 axiom-free) |
| **STEP 1217 ZCSG SmallCategory** | ZCSG `Zcsg3` inductive type、 ToshNotation の concrete space |
| **STEP 1240/1241/1242 trilogy** | D-FUMT₈ FDE sub-algebra (Cotnoir recapture region)、 ToshNotation の logical context |
| **Paper 173 形は絶対・底は空 (DRAFT)** | ToshNotation 6 glyph + ZCSG + Lawvere FP の **synthesis paper** |
| **Paper 174 型/構造圧縮 (DRAFT)** | ToshNotation を 「spec overhead 圧縮」 framework として articulate |

## Prior art (本 reference 確立時 verify)

- **Linear types** (Wadler 1990) — A ⊸ B 線形含意
- **Effect systems** (Lucassen-Gifford 1988) — monad + effect
- **Session types** (Honda 1993) — !A.T / ?A.T / S ⊕ T
- **Category theory** — ↪ injection / ↠ surjection / ⇒ natural trans / ⊣ adjoint
- **Curry-Howard** (Curry 1934 / Howard 1980) — ⊢ proof term
- **Linear logic** (Girard 1987) — ⊸ / ⊗ / ⅋

→ ToshNotation 6 glyph 選択は **既存 notation 体系から D-FUMT₈ 8 値 + ZCSG 絶対座標 + Lean 4 axiom-free verify と整合する specific combination**。 「世界初」 不可、 「私たちの観測した範囲では 6 glyph 統合 + Lean 4 zero-axiom verify の組合せは見当たらない」 は controllable 表現。

## 「世界初」 不可 articulation

- ❌ 「世界初 proof obligation 表記」 (linear types 1990 で false)
- ❌ 「世界初 直感的 modality glyph」 (effect systems / session types で multiple 体系既存)
- ✅ 「ToshNotation 6 glyph proof obligation + ZCSG 絶対座標 + Lean 4 axiom-free verify + 龍樹空亦復空 articulation の 4 piece 統合 package は、 私たちの観測した範囲では他に完全一致は見当たらない」 = controllable

## Future direction (本 session 範囲外, 別 STEP candidate)

- (a) ⇝ Approx の ρ を ℝ に特殊化、 Mathlib4 `Metric` instance で精度保存則を距離付き formal verify
- (b) ⟲ SelfRef を Lawvere 不動点定理 (`lawvere_fixed_point` STEP 1220) 経由で category-theoretic に深化
- (c) 6 glyph 完備性 verify (modality 網羅性検証、 chat-Claude 提案残)
- (d) ToshNotation × ZcsgVesselV04 (Paper 168 v0.4) の bridge 拡張

## Search context

- Keywords: "ToshNotation 6 glyph", "ToshNotation proof obligation", "Rev Approx Irrev Collapse Entail SelfRef", "chat-Claude 2026-06-29 6-turn arc"
- Related: [[reference-esolang-bench-2026-arxiv-2603-09678]] (LLM 2D 空間 reasoning benchmark)
- Related: [[project-session-2026-06-30-full-arc]] (ToshNotation verify した session)
- Related: [[project-paper168-v04-stable-release-2026-06-25]] (4-party transparent credit precedent)