# WSFC Round 10
## Certificate Soundness：從 Event Polynomial 到 Open-Ball Safety

**English Title:** *Certificate Soundness: From Event Polynomials to Open-Ball Safety in the WSFC Geometry Runtime*  
**文件代號：** `WSFC-R10-v0.1`  
**版本：** v0.1  
**日期：** 2026-09-23  
**作者：** Neo.K  
**AI 協力研究者：** Aletheia / OpenAI GPT-5.6 Sol  
**系列：** Worm Sequence Freedom Closure  
**前置：** `WSFC-R09-v0.1`  
**狀態：** `CERTIFICATE SOUNDNESS CORE / EXACT ALGEBRA / FORMAL COMPOSITION OPEN`  
**Canonical Source：** UTF-8 Markdown

---

# 摘要

Round 09 建立 `WSFC Geometry State IR v0.1`，使 endpoint slide、interior support shift、tangency、collision 與 lower-stage merge 都能以 finite state transition 表示。

Round 10 進一步問：

> runtime 接受一張 certificate，究竟能推出什麼幾何命題？

本輪首先建立 `LineExteriorDisc` 的 soundness core。

令：

$$
L:
ax+by=c,
$$

disc center：

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

radius：

$$
r>0.
$$

對 line 上任意點：

$$
P=(p_x,p_y),
$$

令：

$$
u=P-C,
$$

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

以及：

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

由 $P\in L$：

$$
n\cdot u=s.
$$

runtime line certificate 的 quantitative condition 是：

$$
\boxed{
s^2-r^2\|n\|^2\ge0.
}
$$

在二維，不必使用 distance-to-line formula，也不必先呼叫 Cauchy–Schwarz。直接用 Lagrange identity：

$$
\boxed{
\|n\|^2\|u\|^2
-
(n\cdot u)^2
=
\operatorname{cross}(n,u)^2.
}
$$

所以：

$$
\boxed{
\|n\|^2
(
\|u\|^2-r^2
)
=
\operatorname{cross}(n,u)^2
+
\left[
s^2-r^2\|n\|^2
\right].
}
$$

右邊兩項都 nonnegative。因：

$$
\|n\|^2>0,
$$

得到：

$$
\boxed{
\|P-C\|^2\ge r^2.
}
$$

故 line 上任何點都不進 open disc。

此 identity 已由 SymPy exact polynomial expansion machine-check。

因此：

$$
\boxed{
\texttt{LineExteriorDisc}
+
\texttt{PointOnLine}
\Rightarrow
\texttt{PointOutsideOpenDisc}.
}
$$

只差一個很薄的 metric API bridge，將 squared-distance statement接到 `Metric.ball` membership。

Segment safety則更直接：如果 segment 是該 line 的 subset，line 全體安全，自然推出 segment安全。

Endpoint Slide 的 event polynomial也在本輪一般化。

令：

$$
v(t)=v_0+t d,
$$

以及：

$$
w=C-P_0.
$$

若：

$$
A_0
=
\operatorname{cross}(v_0,w),
$$

$$
A_1
=
\operatorname{cross}(d,w),
$$

$$
B_0=\|v_0\|^2,
$$

$$
B_1=v_0\cdot d,
$$

$$
B_2=\|d\|^2,
$$

則：

$$
F(t)
=
\operatorname{cross}(v(t),w)^2-r^2\|v(t)\|^2
$$

exactly 為：

$$
\boxed{
F(t)
=
C_0+C_1t+C_2t^2,
}
$$

其中：

$$
C_0=A_0^2-r^2B_0,
$$

$$
C_1=2A_0A_1-2r^2B_1,
$$

$$
C_2=A_1^2-r^2B_2.
$$

所以：

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

Round 10 exact symbolic checker已確認 coefficient identity。

canonical endpoint test：

$$
F(t)
=
7t^2-20t+12
=
(t-2)(7t-6).
$$

在：

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

有：

$$
t-2\le0,
$$

$$
7t-6\le0,
$$

所以：

$$
\boxed{
F(t)\ge0.
}
$$

且：

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

因此：

```text
SAFE INTERVAL  [0,6/7]
TERMINAL EVENT LINE_TANGENCY
```

是 exact factor-sign certificate。

Support Shift canonical event 同理：

$$
G(\delta)
=
\delta^2-12\delta+11
=
(\delta-1)(\delta-11),
$$

在：

$$
0\le\delta\le1
$$

nonnegative，而：

$$
G(1)=0.
$$

本輪新增 `WSFC Certificate v0.2`，固定 certificate type：

```text
LINE_EXTERIOR
QUADRATIC_SAFE_INTERVAL
EXACT_EVENT_ROOT
LOWER_STAGE_MERGE
```

並實際重播：

```text
WSFC-R10 CERTIFICATE SOUNDNESS RUNTIME: PASS
```

Round 10 因此第一次建立：

$$
\boxed{
\text{Polynomial Sign}
\rightarrow
\text{Line Exterior}
\rightarrow
\text{Segment Safety}
\rightarrow
\text{Transition Soundness}
}
$$

的 formal responsibility chain。

---

# 1. Certificate Validity 與 Soundness

Certificate validity：

$$
\boxed{
\text{JSON / arithmetic checks pass}.
}
$$

Certificate soundness：

$$
\boxed{
\text{checks pass}
\Rightarrow
\text{claimed mathematical property is true}.
}
$$

Round 10 處理第二層。

---

# 2. `LineExteriorDisc`

IR 使用：

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

並要求 oriented gap：

$$
s\ge0.
$$

quantitative certificate：

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

orientation sign不是 squared-distance soundness 必需，但對 state 的 support side semantics仍保留。

---

# 3. Exact 2D Lagrange Identity

對：

$$
n=(a,b),
\qquad
u=(x,y),
$$

有：

$$
\boxed{
(a^2+b^2)(x^2+y^2)
=
(ax+by)^2
+
(ay-bx)^2.
}
$$

此式完全 polynomial。

SymPy exact expansion residual：

$$
0.
$$

---

# 4. Soundness Identity

由：

$$
n\cdot u=s,
$$

得到：

$$
\boxed{
(a^2+b^2)
(
\|u\|^2-r^2
)
=
(ay-bx)^2
+
s^2-r^2(a^2+b^2).
}
$$

所以只要：

$$
a^2+b^2>0,
$$

以及 certificate：

$$
s^2-r^2(a^2+b^2)\ge0,
$$

就可推出：

$$
\|u\|^2-r^2\ge0.
$$

---

# 5. 為什麼不用 Cauchy–Schwarz

目前 mathlib 有 Cauchy–Schwarz，例如 `inner_mul_inner_self_le`。但 WSFC 已在 coordinate IR 中儲存 $(a,b)$，直接使用二維 polynomial identity更短，也更適合 rational certificate。  

Lean draft因此以：

```text
ring
sq_nonneg
mul_le_mul_left
```

作為預期核心。

---

# 6. Segment Safety

若：

$$
[P,Q]\subset L,
$$

且：

$$
L\cap\operatorname{int}D=\varnothing,
$$

自然：

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

所以 certificate soundness不必再建立 segment-to-disc optimization。

需要的只是 formal `SegmentOnLine` predicate 與 subset composition。

---

# 7. General Endpoint Polynomial

令：

$$
v(t)=v_0+t d.
$$

cross：

$$
\operatorname{cross}(v(t),w)
=
A_0+A_1t.
$$

norm-square：

$$
\|v(t)\|^2
=
B_0+2B_1t+B_2t^2.
$$

因此：

$$
\boxed{
F(t)
=
(A_0^2-r^2B_0)
+
(2A_0A_1-2r^2B_1)t
+
(A_1^2-r^2B_2)t^2.
}
$$

Round 10 exact symbolic comparison全部 residual $0$。

---

# 8. Degree Certificate

Current mathlib 提供：

```text
Polynomial.natDegree_quadratic_le
```

因此一旦 geometry coefficient bridge建好：

$$
F
=
C_2X^2+C_1X+C_0,
$$

degree：

$$
\le2
$$

直接交給 polynomial library。

---

# 9. Canonical Endpoint Certificate

$$
F(t)
=
(t-2)(7t-6).
$$

safe interval：

$$
I=
\left[
0,\frac67
\right].
$$

在 $I$：

$$
t-2\le0,
$$

$$
7t-6\le0.
$$

所以：

$$
F(t)\ge0.
$$

終點：

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

Lean draft已寫出預期 no-`sorry` proof body：

```text
linarith
mul_nonneg_of_nonpos_of_nonpos
norm_num
```

---

# 10. Canonical Support Certificate

$$
G(\delta)
=
(\delta-1)(\delta-11).
$$

在：

$$
0\le\delta\le1
$$

兩 factors同為 nonpositive：

$$
G(\delta)\ge0.
$$

終點：

$$
G(1)=0.
$$

所以 Support Shift 可以使用與 Endpoint Slide 相同的 certificate interface。

---

# 11. v0.2 Certificate Schema

每張 certificate：

```text
type
status
claim
payload
depends_on
```

type：

```text
LINE_EXTERIOR
QUADRATIC_SAFE_INTERVAL
EXACT_EVENT_ROOT
LOWER_STAGE_MERGE
```

這讓 arithmetic、geometry、transition composition 的責任明確分離。

---

# 12. Machine Runtime

本輪：

```text
wsfc_round10_certificate_verify.py
```

實際執行：

```text
WSFC-R10 CERTIFICATE SOUNDNESS RUNTIME: PASS
```

它 exact replay：

- line point soundness；
- Lagrange decomposition；
- endpoint factorization；
- endpoint exact root；
- support factorization；
- support exact root。

---

# 13. Lean Draft

本輪建立：

```text
WSFC_R10_Certificate_Soundness_DRAFT.lean
```

預期 no-`sorry` candidates：

```text
lagrange2
lineExterior_sqDist_ge_radius_sq_TARGET
quadPoly_degree_le_two_TARGET
endpointEvent_coefficients_TARGET
endpointExample_safeInterval_TARGET
endpointExample_eventRoot_TARGET
supportExample_safeInterval_TARGET
```

目前仍未編譯，因本 execution runtime沒有 Lean toolchain。

---

# 14. Remaining Thin Bridges

真正 open 的已縮成：

## B1 — Metric Bridge

$$
r^2\le\|u\|^2
\Rightarrow
\|u\|\ge r
$$

對：

$$
r\ge0.
$$

再轉：

$$
u\notin\operatorname{Metric.ball}(0,r).
$$

## B2 — Set Bridge

$$
\text{segment}\subset\text{safe line}
\Rightarrow
\text{segment safe}.
$$

## B3 — Geometry Coefficient Bridge

從：

$$
P_0,P_1,P_2,C,r
$$

formal 推出 $A_i,B_i,C_i$ 的 polynomial object。

## B4 — Certificate Composition

把：

```text
QUADRATIC_SAFE_INTERVAL
LINE_EXTERIOR
SEGMENT_ON_LINE
EXACT_EVENT_ROOT
```

組成：

```text
SAFE SLIDE UNTIL LINE TANGENCY
```

---

# 15. Line Tangency 與 Segment Contact

Round 10 特別保留：

$$
\boxed{
\text{LINE_TANGENCY}
\neq
\text{SEGMENT_CONTACT}.
}
$$

$F(t_\star)=0$ 證的是 supporting line tangent。

若未來 theorem要求 actual tangency point nằm inside finite segment，需新增：

```text
TANGENCY_POINT_IN_SEGMENT
```

certificate。

目前 Endpoint Shortcut只需要 line constraint active，所以不偷升級 claim。

---

# 16. Certificate Dependency DAG

Endpoint transition目前可寫：

$$
\boxed{
\begin{aligned}
&\text{Quadratic Safe Interval}\\
&+
\text{Nondegenerate Supporting Line}\\
&\Downarrow\\
&\text{Line Exterior on }[0,t_\star]\\
&\Downarrow\\
&\text{Supported Segment Safe}\\
&+
F(t_\star)=0\\
&\Downarrow\\
&\text{Safe Slide Until Line Tangency}.
\end{aligned}
}
$$

這是 Runtime certificate第一次具有明確 theorem dependency graph。

---

# 17. 下一步

Round 11 應只做：

$$
\boxed{
\textbf{Formal Certificate Composition}.
}
$$

先關：

1. squared-distance bridge；
2. segment subset bridge；
3. endpoint coefficient bridge；
4. canonical $t=6/7$ end-to-end theorem target。

一旦這條 canonical transition整條接起來，WSFC 就會有第一個：

$$
\boxed{
\text{runtime certificate}
\Rightarrow
\text{formal geometric transition}
}
$$

的完整 prototype。

---

# 結論

Round 10 的核心不是又多一個 verifier。

而是第一次把：

$$
\boxed{
\text{runtime arithmetic}
}
$$

與：

$$
\boxed{
\text{geometry semantics}
}
$$

之間寫出 soundness theorem。

最核心 identity：

$$
\boxed{
\|n\|^2(\|P-C\|^2-r^2)
=
\operatorname{cross}(n,P-C)^2
+
\operatorname{clearance}(L,D).
}
$$

使 WSFC line certificate成為真正有數學語義的證書。

接著 degree-$2$ event polynomial把 transition 時間問題壓成 finite algebra。

所以目前 certificate chain 已經是：

$$
\boxed{
\text{Polynomial Sign}
\rightarrow
\text{Line Safety}
\rightarrow
\text{Segment Safety}
\rightarrow
\text{Event Soundness}.
}
$$

===END===