# WSFC Round 17
## Generic Transition Algebra：Multi-Footprint Frame Rule、Normalization 與 Sequential Composition

**English Title:** *Generic Transition Algebra: Multi-Footprint Frame Rules, Normalization, and Sequential Composition*  
**文件代號：** `WSFC-R17-v0.1`  
**版本：** v0.1  
**日期：** 2026-09-23  
**作者：** Neo.K  
**AI 協力研究者：** Aletheia / OpenAI GPT-5.6 Sol  
**系列：** Worm Sequence Freedom Closure  
**前置：** `WSFC-R16-v0.1`  
**狀態：** `GENERIC TRANSITION ALGEBRA / FRAME RULE / COMPOSITION MVP`  
**Canonical Source：** UTF-8 Markdown

---

# 摘要

Round 16 已完成兩個 canonical geometry-state transitions：

1. Endpoint Shortcut：
   $$
   S_2
   \rightarrow
   S_2
   \rightarrow
   S_1.
   $$
2. Interior Support Shift：
   $$
   S_3
   \rightarrow
   S_3.
   $$

但兩者仍由不同的手工 proof chain 組裝。

Round 17 的目標是：

> 哪些 proof objects 是所有 WSFC transition 的共同代數？

第一個重要結論是：

$$
\boxed{
\text{不存在單一、全用途的 affected component set。}
}
$$

例如 Endpoint Shortcut：

- feasibility 方面，主 segment 是 dynamic；trailing segment 可由 subsegment frame rule 保護；
- objective 方面，兩條 segment 的長度都變，所以兩條都屬 local objective footprint；
- stage 方面，motion 本身 stage不變，但 terminal normalization會改 stage。

所以一個 transition需要的是：

$$
\boxed{
\textbf{channel-specific footprints}.
}
$$

本輪定義 channels：

```text
FEASIBILITY
OBJECTIVE
COMBINATORIAL
EVENT
STAGE
```

對每個 channel $c$：

$$
\boxed{
E
=
A_c
\sqcup
F_c,
}
$$

其中：

- $A_c$：local dynamic footprint；
- $F_c$：framed footprint。

因此 generic frame rule：

$$
\boxed{
\text{LocalProof}(A_c)
+
\text{FramePreserved}(F_c)
+
\text{InterfaceCompatible}
\Rightarrow
\text{GlobalInvariant}_c.
}
$$

這是 Round 17 的核心 abstraction。

---

# 1. Why Multi-Footprint

Endpoint Shortcut說明單一 affected set不夠。

### Feasibility footprint

```text
dynamic:
  first moving segment

framed:
  trailing segment
  via SUBSEGMENT_INHERITANCE
```

### Objective footprint

```text
dynamic:
  first segment
  trailing segment
```

因兩段長度都變。

### Stage footprint

motion phase：

```text
stage framed / unchanged
```

normalization phase：

```text
stage local / changed
```

所以：

$$
\boxed{
A_{\rm safe}
\neq
A_{\rm objective}
\neq
A_{\rm stage}.
}
$$

這是 generic transition algebra必須顯式表示的資訊。

---

# 2. Transition Primitive 1 — Motion

`MOTION` primitive：

$$
T:
S_0
\leadsto
S_\star.
$$

其要求：

```text
before_valid
channel footprints
local feasibility proofs
frame preservation proofs
interface compatibility
objective decomposition
local objective monotonicity
preterminal event-free proof
terminal event proof
stage preservation
terminal family-state validity
```

第一版 motion primitive要求：

$$
\boxed{
n_{\rm after}=n_{\rm before}.
}
$$

若 stage改變，交由 normalization primitive處理。

---

# 3. Transition Primitive 2 — Normalization

`NORMALIZATION`不是連續 motion。

它是 representation rewrite：

$$
N:
S
\rightarrow
\widehat S.
$$

要求：

$$
\boxed{
\operatorname{Trace}(\widehat S)
=
\operatorname{Trace}(S)
}
$$

以及：

$$
\boxed{
J(\widehat S)
\le
J(S).
}
$$

並：

$$
\boxed{
\operatorname{stage}(\widehat S)
<
\operatorname{stage}(S).
}
$$

所以 lower-stage merge不應混在 motion proof內。

它是一個獨立 semantic-preserving normalization。

---

# 4. Endpoint Shortcut 的 Algebraic Decomposition

Round 16 bundled：

```text
ENDPOINT_SHORTCUT_THEN_MERGE
```

Round 17拆成：

$$
\boxed{
T_{\rm endpoint}
=
N_{\rm duplicate}
\circ
M_{\rm shortcut}.
}
$$

其中：

### Motion

$$
M_{\rm shortcut}:
S_2(0)
\rightarrow
S_2(1).
$$

證：

- full-domain feasibility；
- objective nonincrease；
- no earlier actual event；
- terminal vertex collapse；
- stage仍為 $2$。

### Normalization

$$
N_{\rm duplicate}:
[P_0,P_2,P_2]
\rightarrow
[P_0,P_2].
$$

證：

- trace exact equality；
- objective exact equality；
- stage：
  $$
  2\rightarrow1;
  $$
- after state valid。

這使：

$$
\boxed{
S_2
\xrightarrow{M}
S_2
\xrightarrow{N}
S_1
}
$$

成為真正的 sequential composition，而不是一個特殊 hard-coded transition。

---

# 5. Support Shift

Interior Support Shift不需要 normalization：

$$
\boxed{
T_{\rm support}
=
M_{\rm support}.
}
$$

stage：

$$
3\rightarrow3.
$$

所以同一 generic algebra同時能容納：

- same-stage strict improvement；
- terminal degeneration + stage compression。

---

# 6. Channel Frame Rule

設 state components集合：

$$
E.
$$

對 channel $c$：

$$
E
=
A_c
\sqcup
F_c.
$$

如果：

1. $A_c$ 上的 local invariant已證；
2. $F_c$ 在 transition中由某 frame relation保留；
3. local / frame interface相容；

則：

$$
\boxed{
I_c(S_\tau)
}
$$

全域成立。

這是幾何 transition版的 locality principle。

---

# 7. Feasibility Frame

例如 Endpoint Shortcut trailing segment：

$$
[P_1(t),P_2]
\subseteq
[P_1,P_2].
$$

因此：

$$
\boxed{
\operatorname{Safe}
([P_1,P_2])
\Rightarrow
\operatorname{Safe}
([P_1(t),P_2]).
}
$$

這是 frame proof，不需要重新跑 whole-domain point-to-segment compiler。

因此 future transition可使用不同 frame relations：

```text
UNCHANGED
SUBSEGMENT
TRACE_SUBSET
RIGID_TRANSFORM_INVARIANT
CERTIFIED_EQUIVALENT
```

---

# 8. Objective Frame

若：

$$
J(S_\tau)
=
J_A(S_\tau)
+
J_F,
$$

且：

$$
J_F
$$

在 transition中 constant，

那麼：

$$
J_A(\tau_2)
\le
J_A(\tau_1)
$$

直接推出：

$$
\boxed{
J(S_{\tau_2})
\le
J(S_{\tau_1}).
}
$$

所以 local objective proof足以升級 global objective monotonicity。

Lean draft中的這條已經可以寫成單純 `linarith` theorem candidate。

---

# 9. Combinatorial Frame

對不在 local combinatorial footprint中的：

- vertices；
- supports；
- segment indices；

應保證 index / adjacency relation不變。

local motion只需要證：

```text
affected adjacency valid
interface endpoints compatible
no premature zero segment
no support-order violation
```

而不是重新驗整條 chain。

---

# 10. Event Footprint

event channel也應局部化。

例如 support shift：

```text
event footprint:
  middle support only
```

Endpoint Shortcut：

```text
event footprint:
  moving vertex
  adjacent two segments
```

first-event certificate只需要涵蓋可能由 local footprint產生的 events，再加上 frame preservation保證 framed區域不會偷偷生成新 event。

---

# 11. Stage Footprint

stage change不應由普通 motion偷改。

Round 17 第一版規則：

```text
MOTION:
  stage_after = stage_before

NORMALIZATION:
  stage_after < stage_before
```

這使 stage semantics非常乾淨。

未來若需要 refinement：

$$
n\rightarrow n+1,
$$

則可新增第三個 primitive：

```text
REFINEMENT
```

而不扭曲 MOTION / NORMALIZATION 定義。

---

# 12. Normalization 是 Representation Compression

這一點與 WSFC 最早的 sequence-freedom問題直接相關。

Endpoint terminal state：

$$
[P_0,P_2,P_2]
$$

與：

$$
[P_0,P_2]
$$

不是同一 representation。

但其 geometric trace相同：

$$
\boxed{
\operatorname{Trace}
[P_0,P_2,P_2]
=
\operatorname{Trace}
[P_0,P_2].
}
$$

所以 stage decrease不是物體突然改變。

而是：

$$
\boxed{
\text{representation freedom 被壓縮}.
}
$$

因此：

$$
\boxed{
n
}
$$

本身不應被視為純幾何 ontology。

它同時帶有 representation-stage semantics。

---

# 13. Sequential Composition

若：

$$
T_1:
S_0\rightarrow S_1
$$

sound，

以及：

$$
T_2:
S_1\rightarrow S_2
$$

sound，

且中間 state ID / invariant匹配，

則：

$$
\boxed{
T_2\circ T_1
}
$$

sound。

objective：

$$
J(S_2)
\le
J(S_1)
\le
J(S_0).
$$

所以：

$$
J(S_2)\le J(S_0).
$$

Endpoint closed loop就是第一個 composition實例。

---

# 14. Transition Certificate v0.2 Direction

Round 17建立：

```text
WSFC-TALG-0.1
```

primitive certificate包含：

```text
primitive_kind
before_state_id
after_state_id
stage_before
stage_after

channel_footprints
proof_objects
objective_relation
```

這比 Round 16 v0.1 的 hard-coded channel payload更接近 reusable proof protocol。

---

# 15. Generic Validator

本輪建立 generic validator。

它不理解 broadworm geometry。

它只檢查 algebra responsibility：

### MOTION

- 五 channel footprints齊全；
- local / framed disjoint；
- local feasibility存在；
- framed feasibility都有 frame proof；
- before / terminal validity；
- objective proof；
- event proof；
- stage保持。

### NORMALIZATION

- required proof objects存在；
- trace exact equality；
- objective equality / nonincrease；
- stage strict decrease；
- after state valid。

### COMPOSITION

- 每個 primitive sound；
- previous `after_state_id` 等於 next `before_state_id`。

---

# 16. Validation Result

Endpoint：

```text
MOTION
+
NORMALIZATION
```

得到：

```text
COMPOSITE_TRANSITION_SOUND
stage 2 -> 1
```

Support：

```text
MOTION
```

得到：

```text
COMPOSITE_TRANSITION_SOUND
stage 3 -> 3
```

---

# 17. Negative Mutation Tests

為避免 validator只是一個「永遠 PASS」的 schema checker，本輪刻意破壞 certificates。

測試：

```text
missing frame proof
motion illegally changes stage
normalization loses trace
normalization does not drop stage
state-chain mismatch
missing terminal event
missing objective relation
missing local feasibility
footprint overlap
after-state invalid
```

結果：

$$
\boxed{
10/10
}
$$

全部被拒絕。

這不是 formal proof，但證明 validator至少真的執行 responsibility rules。

---

# 18. Multi-Footprint Transition Algebra

Round 17 最終形式可寫：

$$
\boxed{
\mathcal T
=
(
S_0,
S_1,
I,
\{A_c,F_c\}_{c\in\mathcal C},
\Pi,
E_\star,
R
)
}
$$

其中：

$$
\mathcal C
=
\{
\mathrm{safe},
\mathrm{objective},
\mathrm{comb},
\mathrm{event},
\mathrm{stage}
\}.
$$

$\Pi$ 為各 channel proof objects。

$E_\star$ 為 terminal event。

$R$ 為 optional normalization / representation rewrite。

---

# 19. 與 Sequence Freedom 的關係

現在 sequence freedom 的 state evolution有三種不同含義：

### Motion

$$
S_n
\rightarrow
S_n.
$$

representation freedom數不變，但 state位置改變。

### Normalization

$$
S_n
\rightarrow
S_m,
\qquad
m<n,
$$

trace/task semantics不變，但 representation freedom被壓縮。

### Future Refinement

$$
S_n
\rightarrow
S_m,
\qquad
m>n.
$$

增加 representation / support resolution。

所以未來更精確的 freedom dynamics不是：

$$
n\rightarrow n+1
$$

單一路線。

而是：

$$
\boxed{
\text{Motion}
+
\text{Compression}
+
\text{Refinement}.
}
$$

這比最初「segment count sequence」完整得多。

---

# 20. Formalization

Lean draft建立：

```text
Channel
Footprint
TransitionFootprints
MotionTransition
NormalizationTransition
```

下一步真正值得形式化：

```text
channel_frame_rule_TARGET
normalization_sound_TARGET
transition_compose_TARGET
```

其中 objective frame rule已經只是基本 order arithmetic。

---

# 21. Current Status

```text
SEGMENT SAFETY                     CORE CLOSED
WHOLE-DOMAIN SAFETY                IMPLEMENTED
CANONICAL TRANSITIONS              INTEGRATED
MULTI-FOOTPRINT ALGEBRA            DEFINED
GENERIC VALIDATOR                   IMPLEMENTED
ENDPOINT COMPOSITION                PASS
SUPPORT MOTION                      PASS
NEGATIVE MUTATIONS                  10/10 REJECTED
GENERIC FORMAL THEOREM              OPEN
```

---

# 22. 下一步

Round 18 最自然的是：

$$
\boxed{
\textbf{Refinement Primitive}.
}
$$

因目前 algebra已有：

```text
MOTION
NORMALIZATION
```

而 WSFC最初的 sequence自由度真正還缺：

```text
REFINEMENT
```

也就是：

$$
S_n
\rightarrow
S_{n+k}
$$

如何增加 representation freedom，同時建立：

- trace approximation relation；
- task residual upper bound；
- new support-cell activation；
- parent-child certificate；
- refinement consistency。

當這第三個 primitive加入後：

$$
\boxed{
\text{Motion}
+
\text{Normalization}
+
\text{Refinement}
}
$$

就會形成完整的 sequence-freedom transition algebra。

---

# 結論

Round 17 把 canonical state transitions抽象成 reusable algebra。

最重要的兩個新觀念：

$$
\boxed{
\textbf{Multi-Footprint Frame Rule}
}
$$

以及：

$$
\boxed{
\textbf{Normalization as Representation Compression}.
}
$$

所以未來一個新的 worm freedom action不必重新證整個 world。

只要交：

$$
\boxed{
\text{local proofs}
+
\text{frame proofs}
+
\text{interface proof}
+
\text{event/stage proof}.
}
$$

這就是 WSFC transition layer開始真正模組化的地方。

===END===