# WSFC Round 09
## Formal Geometry State Model：從連續幾何直覺到可重播的事件狀態機

**English Title:** *Formal Geometry State Model: A Replayable Event-State Machine for WSFC*  
**文件代號：** `WSFC-R09-v0.1`  
**版本：** v0.1  
**日期：** 2026-09-23  
**作者：** Neo.K  
**AI 協力研究者：** Aletheia / OpenAI GPT-5.6 Sol  
**系列：** Worm Sequence Freedom Closure  
**前置：** `WSFC-R08-v0.1`  
**狀態：** `CANONICAL GEOMETRY IR / EXACT EVENT CERTIFICATES / LEAN STATE MODEL DRAFT`  
**Canonical Source：** UTF-8 Markdown

---

# 摘要

Round 08 已將 geometry kernel 壓成兩個主要 bridge：

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

Round 09 不再直接證 bridge，而先建立它們真正操作的**形式狀態空間**。

核心原則是：

$$
\boxed{
\text{先固定 state semantics，
再讓 Python、Lean、interval runtime 共用同一份語義。}
}
$$

本輪建立：

1. `WSFC Geometry State IR v0.1`；
2. exact-rational Python reference runtime；
3. endpoint-slide event polynomial；
4. support-shift exact replay；
5. transition / event taxonomy；
6. lower-stage merge semantics；
7. Lean 4 state-model draft。

本輪最重要的新點是：

> Endpoint Slide 的 first tangency 不必只寫成抽象「連續滑到第一次碰圓」。

若：

$$
P_1(t)
=
(1-t)P_1+tP_2,
$$

則移動 line：

$$
P_0P_1(t)
$$

與半徑 $r$、中心 $C$ 的 disc tangency，可寫為：

$$
\boxed{
\operatorname{cross}
\left(
P_1(t)-P_0,
C-P_0
\right)^2
-
r^2
\left\|
P_1(t)-P_0
\right\|^2
=
0.
}
$$

因：

$$
P_1(t)-P_0
$$

對 $t$ affine，上式是 degree 至多 $2$ 的 polynomial。

因此 transition 可以攜帶：

```text
EVENT POLYNOMIAL
EXACT ROOT / ISOLATING INTERVAL
SAFE PARAMETER INTERVAL
EVENT KIND
```

而不是靠 floating collision detector。

本輪 canonical rational test vector：

$$
P_0=(2,1),
\qquad
P_1=(2,-1),
\qquad
P_2=(1,0),
$$

unit disc centered at origin。

clearance polynomial exact factorization：

$$
\boxed{
7t^2-20t+12
=
(7t-6)(t-2).
}
$$

所以第一個 event：

$$
\boxed{
t_\star
=
\frac67
}
$$

且該 event 精確為 tangency。

這使：

$$
\boxed{
\text{safe slide}
\rightarrow
\text{event polynomial}
\rightarrow
\text{exact event state}
}
$$

第一次成為機器可重播 transition。

Support Shift 亦建立全有理測試。

三條 lines：

$$
3x-4y=5,
$$

$$
5x=6,
$$

$$
3x+4y=5
$$

圍繞 unit disc。

中央 line 具有 strict slack。

將：

$$
5x=6
$$

移為：

$$
5x=5
$$

得到 tangency。

局部 chain exact length：

$$
\frac{27}{10}
\longrightarrow
\frac52,
$$

因此：

$$
\boxed{
\Delta L
=
-\frac15.
}
$$

整個 state transition 不含 floating geometry。

Round 09 因而把「幾何證明」改寫為：

$$
\boxed{
\text{state}
+
\text{invariant}
+
\text{transition}
+
\text{event certificate}
+
\text{lower-stage map}.
}
$$

這與 WSFC 最初的 Sequence Freedom 問題直接對齊：自由度的「動」現在不再只是概念，而有一個明確的 state-transition semantics。

---

# 1. 為什麼先定義 state，而不是繼續證 lemma

Round 08 已經有 exact finite variation。

真正不穩的地方是：

- 哪些幾何條件是 transition precondition？
- 哪一刻算 support collision？
- 哪一刻算 tangency？
- degeneration 如何進入 lower stage？
- numerical runtime 與 Lean theorem 用的「同一個幾何物件」到底是什麼？

如果不先固定 IR，後續 formalization 很容易產生：

$$
\boxed{
\text{Python semantics}
\neq
\text{Lean semantics}.
}
$$

所以 Round 09 先做 canonical model。

---

# 2. Scalar Encoding

Geometry IR 第一版以：

```text
rational-string
```

為 canonical exact scalar。

例如：

```text
"6/5"
"-7/20"
"1"
```

原因：

1. line intersection 對 rational lines 保持 rational；
2. event polynomial coefficients 可 exact；
3. JSON 可直接交換；
4. Lean 可映射到 $\mathbb Q$ 後再 coercion 到 $\mathbb R$。

未來保留：

```text
algebraic-with-isolating-interval
interval-decimal
```

但不在第一版混進同一個 exact verifier。

---

# 3. Point

點：

$$
P=(x,y)
$$

以：

```text
["x","y"]
```

表示。

canonical runtime 使用：

$$
x,y\in\mathbb Q.
$$

---

# 4. Oriented Line

line 不用 slope-intercept。

定義：

$$
\boxed{
ax+by=c.
}
$$

normal：

$$
n=(a,b).
$$

不要求 unit normalization。

對 obstacle center：

$$
C=(c_x,c_y),
$$

line orientation 固定使：

$$
s
=
c-a c_x-b c_y
\ge0.
$$

---

# 5. Polynomial Disc Certificate

對 radius：

$$
r,
$$

line 與 closed disc 不相交 interior 的 condition：

$$
\frac{s}{\sqrt{a^2+b^2}}
\ge r.
$$

不用開平方，可以寫：

$$
\boxed{
s\ge0
}
$$

以及：

$$
\boxed{
s^2-r^2(a^2+b^2)\ge0.
}
$$

因此 `LineExteriorDisc` 完全是 polynomial / order predicate。

Tangency：

$$
\boxed{
s^2-r^2(a^2+b^2)=0.
}
$$

這是 formalization 很重要的一步：

> 不需要在線的基本資料結構裡儲存 normalized normal 或 square root。

---

# 6. Segment Feasibility

如果 segment：

$$
[P,Q]
$$

整段位於一條 exterior line：

$$
L,
$$

則：

$$
[P,Q]
\cap
\operatorname{int}D
=
\varnothing.
$$

因為整條 affine line 都不進入 open disc。

因此 single-disc support path 的安全證書可以由：

```text
SEGMENT ON LINE
+
LINE EXTERIOR DISC
```

組合。

mathlib 已經有 `segment`、`openSegment`、`Metric.closedBall`、`Metric.ball` 與 convex segment APIs，可直接承接這個資料模型。citeturn903972search1turn903972search3turn903972search4

---

# 7. Support Line Intersection

兩 lines：

$$
a_1x+b_1y=c_1,
$$

$$
a_2x+b_2y=c_2
$$

若：

$$
\Delta
=
a_1b_2-a_2b_1
\neq0,
$$

intersection：

$$
\boxed{
x
=
\frac{
c_1b_2-c_2b_1
}{
\Delta
},
}
$$

$$
\boxed{
y
=
\frac{
a_1c_2-a_2c_1
}{
\Delta
}.
}
$$

rational lines 給 rational vertex。

所以 fixed normal-order cell 可完全 exact replay。

---

# 8. Canonical State

Round 09 state：

$$
\boxed{
S_n
=
(
V,
L,
D,
O,
C,
E
).
}
$$

其中：

- $V$：vertices；
- $L$：support lines；
- $D$：disc obstacles；
- $O$：normal / combinatorial order；
- $C$：certificates；
- $E$：possible next events。

formal record：

```text
schema_version
state_id
stage
obstacles[]
chain.vertices[]
chain.segment_count
chain.support_lines[]
chain.normal_order
certificates[]
next_events[]
```

---

# 9. Invariants

第一版明確拆開，不設一個 opaque `ValidState`。

## I1 — Stage

$$
|V|
=
n+1.
$$

## I2 — Support Count

$$
|L|
=
n.
$$

## I3 — Segment-on-Line

第 $i$ segment：

$$
[V_i,V_{i+1}]
$$

位於：

$$
L_i.
$$

## I4 — Consecutive Intersection

interior vertex：

$$
V_i
=
L_{i-1}
\cap
L_i.
$$

## I5 — Obstacle Exterior

對 relevant support line：

$$
s_i\ge0,
$$

$$
s_i^2-r^2\|n_i\|^2\ge0.
$$

## I6 — Normal Order

consecutive support normals維持指定 orientation。

## I7 — Nonzero Segment

$$
V_i\neq V_{i+1}.
$$

任何 invariant failed，都應明確知道是哪一個，不可只返回：

```text
invalid state
```

---

# 10. Transition Taxonomy

本輪固定四種 transition。

## T1 — Endpoint Slide

$$
P_1
\mapsto
P_1(t)
=
(1-t)P_1+tP_2.
$$

可能事件：

```text
TANGENCY
VERTEX_COLLAPSE
```

## T2 — Interior Support Shift

固定 normal：

$$
(a_i,b_i)
$$

只改：

$$
c_i
\mapsto
c_i-\delta.
$$

事件：

```text
TANGENCY
SUPPORT_COLLISION
```

## T3 — Merge Collision

若：

```text
zero segment
equal support direction
collinear duplicate segment
```

則：

$$
n\mapsto n-1.
$$

## T4 — Safe No-op / Checkpoint

不改 geometry，只更新 certificate / state hash。

---

# 11. Endpoint Event Polynomial

令：

$$
v(t)
=
P_1(t)-P_0.
$$

segment supporting line 與 disc center 的 unnormalized signed-area numerator：

$$
A(t)
=
\operatorname{cross}
(
v(t),
C-P_0
).
$$

line norm-square：

$$
N(t)
=
\|v(t)\|^2.
$$

tangency：

$$
\boxed{
A(t)^2-r^2N(t)=0.
}
$$

因：

$$
v(t)
$$

affine，

所以：

$$
\deg A\le1,
$$

$$
\deg N\le2,
$$

故：

$$
\boxed{
\deg
\left[
A(t)^2-r^2N(t)
\right]
\le2.
}
$$

這就是 Endpoint Slide 的 canonical event polynomial。

---

# 12. Rational Test：First Tangency = $6/7$

取：

$$
P_0=(2,1),
$$

$$
P_1=(2,-1),
$$

$$
P_2=(1,0),
$$

$$
C=(0,0),
\qquad
r=1.
$$

runtime exact 計算：

$$
\boxed{
F(t)
=
7t^2-20t+12.
}
$$

factor：

$$
\boxed{
F(t)
=
(7t-6)(t-2).
}
$$

在：

$$
0\le t\le\frac67,
$$

$F(t)\ge0$，

且：

$$
F(6/7)=0.
$$

所以：

$$
\boxed{
t_\star=\frac67
}
$$

是 exact first tangency certificate。

collapse parameter：

$$
t=1.
$$

因此：

$$
t_\star<1.
$$

第一事件真的是 tangency，而不是 collapse。

---

# 13. Event Certificate

Endpoint transition 不只保存：

```text
event = tangency
```

而保存：

```text
parameter = t
domain = [0,1]
event_polynomial = 7*t^2 - 20*t + 12
factorization = (7*t - 6)(t - 2)
first_event = 6/7
safe_interval = [0,6/7]
terminal_kind = TANGENCY
collapse_parameter = 1
```

這就是：

$$
\boxed{
\text{event}
+
\text{why it is the first event}.
}
$$

---

# 14. Support Shift State

Interior support transition：

$$
L_i:
a_ix+b_iy=c_i.
$$

固定：

$$
(a_i,b_i),
$$

改：

$$
c_i
\mapsto
c_i-\delta.
$$

需要監測兩種 event：

### Tangency

$$
\boxed{
(c_i-\delta-n_i\cdot C)^2
-
r^2\|n_i\|^2
=
0.
}
$$

### Support Collision

例如 intersection 與鄰近 vertex collapse，或 consecutive support directions退化。

event 仍可以用 polynomial / exact coordinate equality certificate。

---

# 15. Rational Support-Shift Test

unit disc：

$$
x^2+y^2\le1.
$$

三條 lines：

$$
3x-4y=5,
$$

$$
5x=6,
$$

$$
3x+4y=5.
$$

左右 lines tangent。

中央 line：

$$
x=\frac65
$$

有 strict slack。

intersections：

$$
V_-=
\left(
\frac65,
-\frac7{20}
\right),
$$

$$
V_+=
\left(
\frac65,
\frac7{20}
\right).
$$

把中央 line 改為：

$$
5x=5,
$$

得到：

$$
V_-'
=
\left(
1,-\frac12
\right),
$$

$$
V_+'
=
\left(
1,\frac12
\right).
$$

中央 line 此時 tangent。

---

# 16. Exact Length Replay

固定 outer points：

$$
U=
\left(
\frac25,-\frac{19}{20}
\right),
$$

$$
W=
\left(
\frac25,\frac{19}{20}
\right).
$$

shift 前 segment lengths：

$$
1,
\qquad
\frac7{10},
\qquad
1.
$$

所以：

$$
L_{\rm old}
=
\frac{27}{10}.
$$

shift 後：

$$
\frac34,
\qquad
1,
\qquad
\frac34,
$$

所以：

$$
L_{\rm new}
=
\frac52.
$$

exact drop：

$$
\boxed{
L_{\rm old}-L_{\rm new}
=
\frac15.
}
$$

這與 Round 08 finite variation formula完全一致。

---

# 17. Lower-Stage Merge

在 state machine 中：

$$
\boxed{
\text{collision}
\neq
\text{failure}.
}
$$

它是一個合法 transition。

例如：

$$
V_i=V_{i+1}
$$

則刪除 zero segment：

$$
S_n
\rightarrow
S_{n-1}.
$$

若 consecutive support lines become identical：

$$
L_i=L_{i+1},
$$

也進行 merge。

所以：

$$
\boxed{
\partial\Gamma_n
\rightarrow
\Gamma_{n-1}
}
$$

現在不是論文敘述，而有明確 transition type：

```text
LOWER_STAGE_MERGE
```

---

# 18. State Machine View

現在一個 local proof 不再寫：

> continuously move the line until it touches the circle.

而寫：

$$
S_0
\xrightarrow{
\operatorname{SupportShift}
}
S(t).
$$

verifier 持續維持 invariants。

下一個 certificate event：

$$
e_\star
=
\min
\{
e_{\rm tangent},
e_{\rm collision}
\}.
$$

若：

$$
e_\star=e_{\rm tangent},
$$

進入 active tangent state。

若：

$$
e_\star=e_{\rm collision},
$$

執行：

$$
\operatorname{Merge}
$$

進入 lower stage。

這正是 WSFC 最早想研究的：

$$
\boxed{
\text{possibility-space state evolution}.
}
$$

---

# 19. Reference Runtime

本輪建立：

```text
wsfc_geometry_state_runtime.py
```

它使用：

```text
fractions.Fraction
sympy exact polynomial
```

不使用 float 作 canonical state。

目前 runtime 已實際重播兩個 canonical tests：

```text
ENDPOINT SLIDE:
    event polynomial = 7*t^2 - 20*t + 12
    first tangency = 6/7

INTERIOR SUPPORT SHIFT:
    central line slack -> tangent
    exact local length drop = 1/5
```

執行結果：

```text
WSFC-R09 STATE RUNTIME: PASS
```

---

# 20. Lean State Model

本輪新增：

```text
WSFC_R09_Formal_Geometry_State_Model_DRAFT.lean
```

它不再先寫主 theorem。

先定義：

```text
P2
OrientedLine
DiscObstacle
signedGap
clearancePoly
LineExteriorDisc
LineTangentDisc
EventKind
PolygonalState
SupportState
EventPolynomialCert
EndpointSlideState
SupportShiftState
Transition
StateInvariant
```

這是 Round 09 最主要的 formalization 成果。

---

# 21. 與目前 mathlib 的對接

目前 mathlib 已存在：

- `segment` / `openSegment`；
- `AffineMap.lineMap`；
- `Metric.closedBall` / `Metric.ball`；
- Euclidean closed ball；
- convex segment subset theorem。citeturn903972search0turn903972search1turn903972search4turn903972search5

因此 WSFC state model 可以把「線、support certificate、event IR」作為自身 layer，而把 metric segment / ball 基礎交給 mathlib。

---

# 22. 第一批 Lean Theorem Targets

Round 09 不再用一個 `True` 代表整個 geometry kernel。

目標拆成：

## G1

$$
\boxed{
\text{LineExteriorDisc}
\Rightarrow
\text{affine line disjoint from open ball}.
}
$$

## G2

support line exterior，segment 又位於 line：

$$
\boxed{
\text{segment avoids open ball}.
}
$$

## G3

Endpoint Slide event polynomial degree：

$$
\boxed{
\deg F\le2.
}
$$

## G4

若 certificate 證：

$$
F(t)\ge0
$$

on：

$$
[0,t_\star],
$$

且：

$$
F(t_\star)=0,
$$

則 slide safe until tangency。

## G5

three support lines 的 ordered intersections under support shift。

## G6

collision：

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

這六個才是 Round 10+ 真正應逐個 compile 的 formal targets。

---

# 23. State Certificate 不等於 Proof Certificate

本輪特別區分：

$$
\boxed{
\text{State Certificate}
}
$$

與：

$$
\boxed{
\text{Theorem Proof}.
}
$$

state certificate 可以證：

- 此 line exterior；
- 此 event polynomial；
- 此 root exact；
- 此 transition 前後 state 一致；
- 此 stage 已 merge。

但它不自動證：

> 此 transition strategy足以到達 global optimum。

後者仍需 theorem layer。

這與前面 Research-Trajectory Certificate 的精神一致：先保留完整 transition responsibility，不把終點 verdict吞掉過程。

---

# 24. Round 09 的新 closure picture

Round 00 的：

$$
\Gamma_n
\rightarrow
\Gamma_{n+1}
$$

現在可以局部細化成：

$$
\boxed{
S
\xrightarrow{\rm safe\ shift}
S'
\xrightarrow{\rm event}
\begin{cases}
S_{\rm tangent},\\
S_{n-1}.
\end{cases}
}
$$

所以 sequence freedom 不再只是一串：

$$
n=4,5,6,\ldots.
$$

每一個固定 $n$ 內部也有自己的 state graph。

整體是：

$$
\boxed{
\text{intra-stage dynamics}
+
\text{inter-stage merge/refinement}.
}
$$

這就是 WSFC 比單純 discretization hierarchy 更完整的地方。

---

# 25. 下一步

Round 10 應該不擴模型。

只做：

$$
\boxed{
\text{Certificate Soundness}.
}
$$

優先：

1. formalize `LineExteriorDisc -> disjoint openBall`；
2. formalize supported segment safety；
3. formalize degree-$2$ endpoint event polynomial；
4. formalize rational exact-root certificate soundness；
5. 把 canonical $t=6/7$ example 變成第一個完整 theorem-prover test target。

這會比直接攻 main broadworm theorem小很多，而且第一次可以把：

$$
\boxed{
\text{geometry runtime certificate}
}
$$

和：

$$
\boxed{
\text{formal theorem}
}
$$

逐項對起來。

---

# 結論

Round 09 完成的不是另一個計算公式。

它建立：

$$
\boxed{
\textbf{WSFC Geometry State IR}.
}
$$

核心 transition現在都有：

```text
STATE
GUARD
INVARIANT
EVENT POLYNOMIAL
FIRST EVENT
TRANSITION
LOWER-STAGE EFFECT
CERTIFICATE
```

而 Endpoint Slide 的 first tangency甚至有完全有理 canonical test：

$$
\boxed{
F(t)
=
(7t-6)(t-2),
\qquad
t_\star=\frac67.
}
$$

Interior Support Shift則有：

$$
\boxed{
\frac{27}{10}
\rightarrow
\frac52
}
$$

的 exact replay。

所以「幾何狀態演化序列」現在已經從研究語言變成真正可序列化、可重播、可驗證的 finite state transition object。

===END===