# WSFC Round 08
## Geometry Kernel Reduction：Endpoint Shortcut 的 Norm Core 與 Interior Support 的精確有限變分

**English Title:** *Geometry Kernel Reduction: A Norm-Core Endpoint Shortcut and Exact Finite Support Variation*  
**文件代號：** `WSFC-R08-v0.1`  
**版本：** v0.1  
**日期：** 2026-09-23  
**作者：** Neo.K  
**AI 協力研究者：** Aletheia / OpenAI GPT-5.6 Sol  
**系列：** Worm Sequence Freedom Closure  
**前置：** `WSFC-R07-v0.1`  
**狀態：** `GEOMETRY KERNEL REDUCED / EXACT ALGEBRA CHECKED / LEAN BRIDGES OPEN`  
**Canonical Source：** UTF-8 Markdown

---

# 摘要

Round 07 已將 WSFC 分離為：

$$
\boxed{
\text{machine-checked algebraic core}
+
\text{formalization-open geometry kernel}.
}
$$

Round 08 不推 general-$n$ 結論，而專攻兩個剩餘幾何核心：

1. Endpoint Shortcut；
2. Interior Support Radius Monotonicity。

本輪的主要進展是發現第二項根本不需要先形式化微分。

在固定 convex normal-order cell 中，取三條 consecutive support lines。中央 line 的相鄰 normal-angle gaps 為：

$$
\alpha,\beta\in(0,\pi).
$$

把中央 support line 向 unit disc 方向平移：

$$
h
\longmapsto
h-\varepsilon,
\qquad
\varepsilon>0.
$$

在沒有 support collision 以前，局部 open-chain length 的變化不是只有一階近似，而是**精確有限式**：

$$
\boxed{
L_{\rm new}
-
L_{\rm old}
=
-\varepsilon
\left[
\frac{1-\cos\alpha}{\sin\alpha}
+
\frac{1-\cos\beta}{\sin\beta}
\right].
}
$$

因：

$$
0<\alpha,\beta<\pi,
$$

有：

$$
\sin\alpha,\sin\beta>0,
$$

以及：

$$
1-\cos\alpha>0,
\qquad
1-\cos\beta>0.
$$

故：

$$
\boxed{
L_{\rm new}<L_{\rm old}.
}
$$

這比 Round 06 使用 derivative：

$$
\frac{\partial L}{\partial h_i}>0
$$

更適合 theorem prover，因為不需先建立 differentiability，只要 formalize line intersections 與 finite displacement。

Endpoint Shortcut 也被拆成兩層。

若：

$$
P_1(t)
=
(1-t)P_1+tP_2,
\qquad
0\le t\le1,
$$

則 exact affine identities：

$$
\boxed{
P_0-P_1(t)
=
(P_0-P_1)
+
t(P_1-P_2),
}
$$

以及：

$$
\boxed{
P_1(t)-P_2
=
(1-t)(P_1-P_2)
}
$$

已由 symbolic machine checker 驗證。

由 norm triangle inequality 與：

$$
\|t v\|
=
t\|v\|
\quad
(t\ge0),
$$

立刻得到：

$$
\boxed{
\|P_0-P_1(t)\|
+
\|P_1(t)-P_2\|
\le
\|P_0-P_1\|
+
\|P_1-P_2\|.
}
$$

因此 Endpoint Shortcut 的**長度層**已降成一般 normed-space theorem；真正尚未形式化的只剩：

> 沿合法 segment 移動 vertex，到 first tangency / collapse event 以前，新的 endpoint-adjacent segment 始終不進入 unit disc。

本輪建立 `WSFC_R08_Geometry_Kernel_DRAFT.lean`。其中：

- endpoint shortcut length theorem 已寫成預期可 `sorry`-free 的 Lean proof body；
- support-drop coefficient positivity亦已寫成預期可 `sorry`-free 的 proof body；
- 兩個真正 geometry bridge 被單獨標出，而沒有用 `True` 假裝主 theorem 完成。

本輪同時對 support finite-variation formula 做 exact symbolic machine check，並以 $2000$ 組隨機 geometry instances 做數值 red-team；Endpoint Shortcut 亦以 $5000$ 組隨機點測試，未發現 violation。

這些 random tests 不是 proof，但提供 implementation sanity。

Round 08 後，真正需要 Lean formalize 的核心已縮成：

$$
\boxed{
\text{Disc Feasibility Bridge}
+
\text{Support-Line Geometry Bridge}.
}
$$

---

# 1. Endpoint Shortcut：先分離 length 與 feasibility

Round 06 的 Endpoint Shortcut 同時混合兩件事：

1. 新 path 比舊 path 短；
2. 新 path 在 unit disc 外仍合法。

Round 08 強制拆開。

第一項其實完全不需要二維幾何。

---

# 2. Affine Shortcut Parameter

令 $E$ 為任意 real normed vector space。

取：

$$
P_0,P_1,P_2\in E.
$$

令：

$$
P_1(t)
=
(1-t)P_1+tP_2,
\qquad
0\le t\le1.
$$

即：

$$
P_1(t)
=
\operatorname{lineMap}(P_1,P_2;t).
$$

mathlib 目前明確提供：

```text
AffineMap.lineMap_apply_module
AffineMap.lineMap_vsub_left
AffineMap.lineMap_vsub_right
lineMap_mem_segment
```

因此不需要自行建立 segment interpolation。

---

# 3. Exact Endpoint Identities

直接展開：

$$
\begin{aligned}
P_0-P_1(t)
&=
P_0
-
(1-t)P_1
-
tP_2\\
&=
(P_0-P_1)
+
t(P_1-P_2).
\end{aligned}
$$

以及：

$$
P_1(t)-P_2
=
(1-t)(P_1-P_2).
$$

本輪 SymPy exact matrix simplification 對兩個 coordinate identities 都得到 zero residual。

---

# 4. Shortcut Length Kernel

由 triangle inequality：

$$
\|P_0-P_1(t)\|
\le
\|P_0-P_1\|
+
t\|P_1-P_2\|.
$$

而：

$$
\|P_1(t)-P_2\|
=
(1-t)\|P_1-P_2\|.
$$

相加：

$$
\boxed{
\|P_0-P_1(t)\|
+
\|P_1(t)-P_2\|
\le
\|P_0-P_1\|
+
\|P_1-P_2\|.
}
$$

所以 shortcut 長度不增，是一個一般 normed-space fact。

mathlib 已提供 `norm_sub_le_norm_sub_add_norm_sub`、`norm_smul_of_nonneg` 與 `norm_smul` 等 API。citeturn149762search0turn149762search1

---

# 5. Endpoint Shortcut 真正剩餘的 Geometry Bridge

需要 formalize：

$$
\boxed{
\text{SafeSlideUntilFirstEvent}.
}
$$

給定 unit disc $D$ 與合法 two-edge subpath：

$$
P_0P_1P_2,
$$

令：

$$
P_1(t)
=
\operatorname{lineMap}(P_1,P_2;t).
$$

定義 safe parameter set：

$$
S
=
\left\{
t\in[0,1]:
[P_0,P_1(t)]
\cap
\operatorname{int}D
=
\varnothing
\right\}.
$$

需要證：

1. $0\in S$；
2. $S$ 在 relevant direction 初始為 interval；
3. 若 $S$ 在 $t<1$ 停止，boundary event 是 tangency；
4. 若到 $t=1$ 都安全，vertex collapse。

這才是 Endpoint Shortcut 尚未 machine-check 的部分。

---

# 6. Interior Support：從 derivative 改成 exact finite variation

Round 06 用：

$$
\frac{\partial L}{\partial h_i}
=
\tan\frac{\delta_{i-1}}2
+
\tan\frac{\delta_i}2.
$$

Round 08 改用 finite displacement。

取中央 support normal 為：

$$
n_i=(1,0),
$$

所以中央 line：

$$
L_i:
x=h.
$$

左鄰 normal 與 $n_i$ 差：

$$
\alpha\in(0,\pi),
$$

可寫：

$$
L_-:
\cos\alpha\,x
-
\sin\alpha\,y
=
h_-.
$$

右鄰：

$$
L_+:
\cos\beta\,x
+
\sin\beta\,y
=
h_+.
$$

---

# 7. Intersections

中央 line 與左鄰交點：

$$
V_-(h)
=
\left(
h,
\frac{
\cos\alpha\,h-h_-
}{
\sin\alpha
}
\right).
$$

右鄰：

$$
V_+(h)
=
\left(
h,
\frac{
h_+-\cos\beta\,h
}{
\sin\beta
}
\right).
$$

令：

$$
h'
=
h-\varepsilon.
$$

machine exact algebra 得：

$$
|V_-(h')-V_-(h)|^2
=
\frac{\varepsilon^2}{\sin^2\alpha},
$$

$$
|V_+(h')-V_+(h)|^2
=
\frac{\varepsilon^2}{\sin^2\beta}.
$$

由：

$$
\sin\alpha,\sin\beta>0
$$

可知 displacement lengths：

$$
\frac{\varepsilon}{\sin\alpha},
\qquad
\frac{\varepsilon}{\sin\beta}.
$$

---

# 8. Central Edge Change

中央 edge length 是：

$$
|V_+(h)-V_-(h)|.
$$

在 normal order / orientation 不變的 cell 裡，其 signed vertical length可直接使用。

machine exact algebra 得：

$$
\boxed{
\ell_i(h-\varepsilon)
-
\ell_i(h)
=
\varepsilon
\left(
\frac{\cos\alpha}{\sin\alpha}
+
\frac{\cos\beta}{\sin\beta}
\right).
}
$$

中央 segment 變長，但兩個 adjacent segments 變短。

---

# 9. Exact Local Total Change

兩個 adjacent segments 分別縮短：

$$
\frac{\varepsilon}{\sin\alpha},
\qquad
\frac{\varepsilon}{\sin\beta}.
$$

所以總 local change：

$$
\begin{aligned}
\Delta L
={}&
\varepsilon
\left(
\frac{\cos\alpha}{\sin\alpha}
+
\frac{\cos\beta}{\sin\beta}
\right)\\
&-
\frac{\varepsilon}{\sin\alpha}
-
\frac{\varepsilon}{\sin\beta}.
\end{aligned}
$$

整理：

$$
\boxed{
\Delta L
=
-\varepsilon
\left[
\frac{1-\cos\alpha}{\sin\alpha}
+
\frac{1-\cos\beta}{\sin\beta}
\right].
}
$$

這個 identity 已由 exact symbolic verifier 檢查。

---

# 10. Positivity 不需要 half-angle

Round 06 寫成：

$$
\tan\frac\alpha2+\tan\frac\beta2.
$$

Round 08 formalization 改用：

$$
\boxed{
C(\alpha,\beta)
=
\frac{1-\cos\alpha}{\sin\alpha}
+
\frac{1-\cos\beta}{\sin\beta}.
}
$$

因：

$$
0<\alpha<\pi
$$

時：

$$
\sin\alpha>0,
$$

且：

$$
\cos\alpha<1.
$$

所以每一項都 strictly positive。

同理 $\beta$。

因此：

$$
\boxed{
C(\alpha,\beta)>0.
}
$$

當：

$$
\varepsilon>0,
$$

得到：

$$
\boxed{
\Delta L<0.
}
$$

這條 formal route 比 half-angle tangent identity 更少依賴 trig rewriting。

mathlib 目前直接提供 `Real.sin_pos_of_pos_of_lt_pi` 與 cosine monotonicity / range API。citeturn666958search0

---

# 11. Interior Support 真正剩餘的 Geometry Bridge

scalar finite-variation theorem還不等於完整 geometric theorem。

Lean 仍需證：

> 在 fixed normal-order cell 中，support line $h_i\mapsto h_i-\varepsilon$ 的實際 open-chain geometry 確實具有第 7–9 節的 intersection ordering，直到第一個 tangency / normal collision event。

因此新 target 不再是：

```text
prove a derivative formula
```

而是：

```text
formalize three support lines
formalize their ordered intersections
formalize the exact finite displacement
formalize the first collision bound
```

這是有限 affine geometry，比 calculus 容易控制。

---

# 12. Machine Certificate

本輪：

```text
wsfc_round08_geometry_verify.py
```

實際獨立執行並輸出：

```text
WSFC-R08 GEOMETRY ALGEBRA CERTIFICATE: PASS
```

exact checks：

```text
central edge increment
left/right intersection displacement squared
local support finite length drop
endpoint shortcut first affine identity
endpoint shortcut second affine identity
```

全部為 symbolic zero residual。

---

# 13. Numerical Red Team

另外做兩組 sanity tests。

## Support Variation

$2000$ 組隨機：

$$
(\alpha,\beta,\varepsilon)
$$

與 local three-line geometries。

最大：

$$
|\Delta L_{\rm measured}-\Delta L_{\rm formula}|
$$

低於 floating tolerance。

## Endpoint Shortcut

$5000$ 組隨機：

$$
P_0,P_1,P_2,t
$$

檢查：

$$
L_{\rm new}
\le
L_{\rm old}.
$$

未發現 violation。

這兩者都不是 proof，只用來抓 implementation/sign mistakes。

---

# 14. Lean Draft v2

`WSFC_R08_Geometry_Kernel_DRAFT.lean` 現在分成：

### A. Endpoint Norm Core

目標 theorem：

```text
endpointShortcut_length_nonincrease_TARGET
```

proof body 已使用：

- `AffineMap.lineMap_apply_module`；
- norm triangle inequality；
- `norm_smul_of_nonneg`；
- scalar ring normalization。

它被標記：

```text
LEAN-NO-SORRY-CANDIDATE / UNCOMPILED
```

因目前 runtime 仍無 Lean toolchain。

### B. Support Coefficient Positivity

```text
supportDropCoeff_pos_TARGET
```

亦有完整 candidate proof body。

### C. Geometry Bridges

真正 `OPEN`：

```text
endpointShortcut_discFeasible_TARGET
support_line_finite_variation_GEOMETRY_TARGET
singleDisc_tangent_kernel_TARGET
```

---

# 15. Proof Responsibility 再次縮小

Round 07：

$$
\boxed{
\text{Geometry Kernel}
}
$$

仍是一整塊。

Round 08 後變成：

$$
\boxed{
\text{Geometry Kernel}
=
\text{two affine/order bridges}.
}
$$

也就是：

1. segment sliding 的 safe-event geometry；
2. three-support-line finite variation 的 intersection-order geometry。

長度不等式與 scalar positivity 已不再是主要風險。

---

# 16. 與 Sequence Freedom 的關係

這一輪看似只做 local lemma，但它其實直接對應 WSFC 的 sequence closure。

support-angle collision：

$$
\alpha\rightarrow0
$$

或：

$$
\beta\rightarrow0
$$

時，

finite drop coefficient：

$$
C(\alpha,\beta)
$$

的一項趨近 $0$，

同時 geometry 進入：

$$
\boxed{
\text{lower-stage segment merge}.
}
$$

所以「cell interior 的 strict shortening」與「cell boundary 的 lower-stage absorption」在同一個 finite-variation picture 中接起來。

這正是有限 freedom stage 之間 transition 的 local formal kernel。

---

# 17. 下一步

Round 09 若仍沿 verification 路線，應做：

$$
\boxed{
\text{Formal Geometry State Model}.
}
$$

不是先攻 main theorem。

需要正式定義：

```text
support line
ordered normal angle
line intersection
open polygonal chain
segment count
unit-disc avoidance
normal-order cell
support collision
lower-stage merge
safe slide interval
first tangency event
```

然後把 Round 08 兩個 geometry bridges填實。

如果本地 Lean runtime 可以接上，優先編譯：

1. `endpointShortcut_length_nonincrease_TARGET`；
2. `supportDropCoeff_pos_TARGET`。

這兩個一旦真的 compile，就會成為 WSFC 第一批 proof-assistant verified kernel lemmas。

---

# 結論

Round 08 的主要成果不是增加一條 broadworm theorem。

而是把幾何 proof debt 從：

$$
\text{「要 formalize 一個看起來很直觀的變分」}
$$

改寫成兩個極小 affine geometry obligations。

最關鍵的新式：

$$
\boxed{
L(h-\varepsilon)-L(h)
=
-\varepsilon
\left[
\frac{1-\cos\alpha}{\sin\alpha}
+
\frac{1-\cos\beta}{\sin\beta}
\right].
}
$$

它是 exact finite variation，而不是 derivative approximation。

因此 Interior Support Radius Monotonicity 可以在沒有 calculus 的情況下完成。

Endpoint Shortcut 的 length layer也已降成一般 normed-space triangle inequality。

現在真正剩下的是：

$$
\boxed{
\text{geometry feasibility and event ordering}.
}
$$

這比 Round 07 的幾何 kernel 小得多。

===END===