# WSFC Round 12
## Generic Point-to-Segment Certificate Compiler：自動相位分解、代數根隔離與 First-Event 語義

**English Title:** *Generic Point-to-Segment Certificate Compiler: Automatic Feature Phases, Algebraic Root Isolation, and First-Event Semantics*  
**文件代號：** `WSFC-R12-v0.1`  
**版本：** v0.1  
**日期：** 2026-09-23  
**作者：** Neo.K  
**AI 協力研究者：** Aletheia / OpenAI GPT-5.6 Sol  
**系列：** Worm Sequence Freedom Closure  
**前置：** `WSFC-R11-v0.1`  
**狀態：** `GENERIC COMPILER MVP / EXACT ROOT ISOLATION / SEMANTIC PHASE DECOMPOSITION`  
**Canonical Source：** UTF-8 Markdown

---

# 摘要

Round 11 修正一個重要 semantic bug：

$$
\boxed{
\text{supporting-line tangency}
\neq
\text{finite-segment contact}.
}
$$

因此 Endpoint Slide 的安全性不能由單一 supporting-line polynomial 全域負責，而必須依 finite segment 的 nearest feature 分 phase。

Round 12 將此修正從 canonical example 推廣為 generic compiler。

輸入：

$$
P_0,
\qquad
Q(t)=Q_0+tD,
\qquad
C,
\qquad
r,
\qquad
t\in[t_0,t_1].
$$

其中第一版要求所有 input coefficients為 rational。

定義：

$$
w=P_0-C,
$$

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

compiler exact 生成六個核心 quantity：

$$
A(t)=w\cdot v(t),
$$

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

$$
S(t)=A(t)+N(t),
$$

$$
H_0=\|w\|^2-r^2,
$$

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

$$
H_1(t)
=
\|w+v(t)\|^2-r^2.
$$

nearest feature 由：

$$
A(t),
\qquad
S(t),
\qquad
N(t)
$$

決定。

安全性則依 phase 使用：

```text
FIXED_ENDPOINT
    -> H0

INTERIOR_PROJECTION
    -> L(t)

MOVING_ENDPOINT
    -> H1(t)

DEGENERATE_SEGMENT
    -> point-state branch
```

compiler 收集：

- $A=0$；
- $S=0$；
- $N=0$；
- $L=0$；
- $H_1=0$

在 parameter domain 內的所有 real roots。

因 affine motion 下它們 degree 至多 $2$，roots 可以 exact 求出；irrational roots則保存 algebraic expression 與 rational isolating interval。

所有 roots 加上 domain endpoints 形成：

$$
\boxed{
\text{atomic parameter cells}.
}
$$

每一 open cell 中：

- nearest feature不變；
- active safety polynomial沒有 root；
- safety sign固定。

因此 generic compiler可以自動輸出：

```text
derived polynomials
exact/algebraic roots
isolating intervals
atomic cells
nearest feature per cell
active safety polynomial
safety sign
certificate-only boundaries
actual geometric events
first actual geometric event
proof DAG
```

本輪 compiler 已通過兩種測試。

### Test A — Round 11 canonical example

自動恢復：

$$
\boxed{
t=\frac12
}
$$

nearest-feature switch，

$$
\boxed{
t=\frac67
}
$$

supporting-line tangency only，

以及：

$$
\boxed{
t=1
}
$$

first actual collapse/contact。

### Test B — Irrational endpoint contact

取：

$$
P_0=(3,0),
$$

$$
Q(t)=
\left(
2-t,\frac12
\right),
$$

unit disc at origin，

$$
t\in[0,2].
$$

compiler 自動找到 first actual contact：

$$
\boxed{
t_\star
=
2-\frac{\sqrt3}{2}.
}
$$

這不是 rational root。

輸出同時保存：

```text
exact algebraic expression
decimal approximation
rational isolating interval
```

所以 Round 12 第一次證明 compiler 不依賴「剛好可以因式分解成 rational roots」的 canonical toy case。

---

# 1. Generic Input

第一版：

```text
P0
Q0
D
C
r
parameter_interval
```

其中：

$$
Q(t)=Q_0+tD.
$$

所有 scalar input 使用：

$$
\mathbb Q.
$$

---

# 2. Core Polynomials

## Dot Guard

$$
\boxed{
A(t)=w\cdot v(t).
}
$$

degree：

$$
\le1.
$$

## Segment Norm

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

degree：

$$
\le2.
$$

## Projection Switch

$$
\boxed{
S(t)=A(t)+N(t).
}
$$

degree：

$$
\le2.
$$

## Fixed Endpoint Safety

$$
\boxed{
H_0=\|w\|^2-r^2.
}
$$

constant。

## Interior Safety

$$
\boxed{
L(t)
=
\operatorname{cross}(v(t),w)^2-r^2N(t).
}
$$

degree：

$$
\le2.
$$

## Moving Endpoint Safety

$$
\boxed{
H_1(t)
=
\|w+v(t)\|^2-r^2.
}
$$

degree：

$$
\le2.
$$

所以整個 generic segment certificate compiler只需要處理 quadratic algebra。

---

# 3. Nearest Feature Classifier

當：

$$
N(t)>0,
$$

有：

$$
\boxed{
A(t)\ge0
\Rightarrow
\texttt{FIXED\_ENDPOINT}.
}
$$

若：

$$
A(t)<0,
$$

且：

$$
S(t)\ge0,
$$

則：

$$
\boxed{
\texttt{INTERIOR\_PROJECTION}.
}
$$

若：

$$
S(t)<0,
$$

則：

$$
\boxed{
\texttt{MOVING\_ENDPOINT}.
}
$$

若：

$$
N(t)=0,
$$

則：

$$
\boxed{
\texttt{DEGENERATE\_SEGMENT}.
}
$$

這就是有限 segment 的 feature state machine。

---

# 4. Root Set

compiler 不只找 feature-switch roots。

完整 root set：

$$
\boxed{
R
=
R_A
\cup
R_S
\cup
R_N
\cup
R_L
\cup
R_{H_1}.
}
$$

其中：

- $R_A$：fixed/interior phase boundary；
- $R_S$：interior/moving-endpoint phase boundary；
- $R_N$：segment collapse；
- $R_L$：line-clearance roots；
- $R_{H_1}$：moving endpoint contact roots。

將 domain endpoints 一起加入。

---

# 5. Atomic Cells

排序：

$$
t_0
=
\rho_0
<
\rho_1
<
\cdots
<
\rho_m
=
t_1.
$$

atomic cells：

$$
I_j
=
(\rho_j,\rho_{j+1}).
$$

每一 cell 沒有任何 feature/safety polynomial root。

因此 sign vector固定。

compiler只要取一個 rational sample：

$$
\tau_j\in I_j
$$

即可確定整個 cell 的：

```text
nearest feature
active safety polynomial
safety sign
```

這是 finite algebraic decomposition。

---

# 6. Algebraic Root Isolation

對 quadratic irrational root，不轉成 float authority。

保存：

```text
exact
approx
isolating_interval
```

例如 Test B：

$$
\boxed{
2-\frac{\sqrt3}{2}
}
$$

同時附 rational isolating interval。

所以 root comparison與 phase ordering可以逐步升級到 proof-assistant / interval certified implementation。

---

# 7. Certificate Boundary vs. Actual Event

每個 root 都帶 sources。

例如：

```text
projection_switch
supporting_line_clearance
moving_endpoint_clearance
norm_v_sq
```

compiler 再依 nearest-feature semantics 判斷：

- root 是否只是 certificate boundary；
- 是否為 actual finite-segment contact；
- 是否為 vertex collapse；
- 是否同時為多事件。

因此不再把：

$$
L(t)=0
$$

自動當 segment contact。

---

# 8. Canonical Test A

Round 11 example compiler output恢復：

```text
1/2:
  NEAREST_FEATURE_SWITCH

6/7:
  SUPPORTING_LINE_TANGENCY_ONLY

1:
  VERTEX_COLLAPSE
  MOVING_ENDPOINT_CONTACT
```

first actual event：

$$
\boxed{
t=1.
}
$$

---

# 9. Irrational Test B

取：

$$
P_0=(3,0),
$$

$$
Q(t)=
\left(
2-t,\frac12
\right).
$$

moving endpoint clearance：

$$
H_1(t)
=
(2-t)^2+\frac14-1.
$$

所以：

$$
H_1(t)=0
$$

給：

$$
t
=
2\pm\frac{\sqrt3}{2}.
$$

domain：

$$
[0,2]
$$

內 first contact：

$$
\boxed{
2-\frac{\sqrt3}{2}.
}
$$

compiler 正確標記為：

```text
ALGEBRAIC ROOT
MOVING_ENDPOINT_CONTACT
```

並輸出 isolating interval。

---

# 10. First Actual Event

compiler 不以：

> 最小 polynomial root

作 first event。

而是：

$$
\boxed{
\min
\{
t:
\text{root is active under finite-segment semantics}
\}.
}
$$

因此：

- inactive line tangency不算；
- feature switch不算；
- collapse算；
- active endpoint / interior contact算。

這是 Round 11 semantic correction 的 generic 化。

---

# 11. Proof DAG

compiler output包含：

```text
derive polynomials
isolate roots
partition parameter domain
classify feature per cell
verify active safety sign
classify boundary roots
select first actual event
```

因此每次 compile 都同時生成一個 theorem-responsibility trace。

---

# 12. Reference Compiler

本輪建立：

```text
wsfc_point_segment_certificate_compiler.py
```

輸入 JSON spec。

輸出：

```text
WSFC-SEGCOMP-0.1
```

compiler 本身使用：

```text
SymPy QQ polynomials
real_roots
rational isolating intervals
```

而非 numerical root finder。

---

# 13. Formalization Target

Lean draft新增 generic primitives：

```text
NearestFeature
H
A
N
S
lineClearance
complete_square
classify_nearest_feature_TARGET
interior_phase_safe_TARGET
compiler_output_sound_TARGET
```

其中 `complete_square` 已是 ring-level no-sorry candidate。

真正剩餘 formal challenge是：

> 把 runtime 產生的 atomic-cell root ordering與 sign certificate形式化成可接受的 finite partition。

---

# 14. Compiler 不是 theorem prover

Reference compiler可以：

- exact derive；
- exact root isolate；
- sign sample；
- build DAG。

但 generic soundness theorem仍需要證：

> roots 已完整；
> root-free cell中 sign不變；
> nearest-feature classifier正確；
> active safety sign推出 entire finite segment safe。

所以狀態：

```text
COMPILER IMPLEMENTED
CANONICAL/ALGEBRAIC TESTS PASS
GENERIC FORMAL SOUNDNESS OPEN
```

---

# 15. 下一步

Round 13 最自然的工作不是再新增 geometry。

而是：

$$
\boxed{
\textbf{Compiler Soundness Layer}.
}
$$

優先證：

1. degree-$2$ root completeness；
2. root-free interval sign invariance；
3. atomic-cell nearest-feature invariance；
4. phase safety theorem；
5. exact/algebraic root ordering certificate；
6. output DAG soundness。

這會讓：

$$
\boxed{
\text{compiler output}
\Rightarrow
\text{finite-segment safety theorem}
}
$$

第一次成為一般化的 target。

---

# 結論

Round 12 把 Round 11 的手工修正升級成通用 compiler。

現在 finite-segment transition 不再靠人工判斷：

$$
\boxed{
\text{哪個 feature 最近？}
}
$$

而是由 polynomial signs自動決定。

整體流程：

$$
\boxed{
\text{Affine Motion}
\rightarrow
\text{Quadratic Polynomials}
\rightarrow
\text{Exact Root Isolation}
\rightarrow
\text{Feature Phases}
\rightarrow
\text{Phase Safety}
\rightarrow
\text{Actual Event}
\rightarrow
\text{Proof DAG}.
}
$$

這使 WSFC Geometry State Runtime開始具備真正的 generic certificate compilation能力。

===END===