# WSFC Round 07
## Machine-Checkable Lemma Layer：從研究證明鏈到 Exact Symbolic Certificate 與 Lean Formalization Targets

**English Title:** *Machine-Checkable Lemma Layer: Exact Symbolic Certificates and Lean Formalization Targets for WSFC*  
**文件代號：** `WSFC-R07-v0.1`  
**版本：** v0.1  
**日期：** 2026-09-23  
**作者：** Neo.K  
**AI 協力研究者：** Aletheia / OpenAI GPT-5.6 Sol  
**系列：** Worm Sequence Freedom Closure  
**前置：** `WSFC-R06-v0.1`  
**狀態：** `MACHINE-CHECKED ALGEBRA / FORMALIZATION TARGET LAYER / GEOMETRY KERNEL OPEN`  
**Canonical Source：** UTF-8 Markdown

---

# 摘要

Round 06 已經停止擴張 general-$n$ 結論，轉入 adversarial verification，並找到一個真實 plateau boundary gap，再以一般 lemma 修復。

Round 07 的目的不是繼續「再證一次」，而是建立不同 authority level：

$$
\boxed{
\text{research derivation}
\neq
\text{symbolic machine check}
\neq
\text{interval certificate}
\neq
\text{proof-assistant proof}.
}
$$

本輪在目前可用 runtime 中完成兩種真正 machine-check：

1. **Exact symbolic certificates**：以 SymPy 對核心 derivative、Hessian determinant、stationary polynomial 與 continuum cubic 做 exact simplification，所有指定 residual 均化為 $0$。
2. **Interval certificate**：以 80-digit interval arithmetic 重驗 $q=0$ boundary lower envelope 與 explicit four-segment competitor 的嚴格 separation。

另一方面，本執行環境沒有 `lean` 或 `lake`，所以本輪明確不宣稱 Lean compilation。取而代之的是建立：

```text
WSFC_R07_Formalization_DRAFT.lean
```

它對應 2026-09 mathlib 的現行 API，把 derivative / Jensen / convexity 與 geometric kernel 的 theorem targets固定成可移植 source draft。

本輪的核心進展不是增加 theorem，而是把 Round 06 的證明責任切成：

$$
\boxed{
\text{Machine-Checked Algebraic Core}
+
\text{Lean-Open Geometric Kernel}.
}
$$

目前 exact symbolic layer 已覆蓋：

- perspective function $g(q,s)$ 的 Hessian rank-one identity；
- one-side $J_d(q,a)$ 的 Hessian determinant factorization；
- general $q$ one-sided plateau branch derivative；
- $q=0$ continuum lower-envelope stationary polynomial；
- continuum endpoint stationary cubic；
- one-segment derivative endpoint identity。

interval layer則重新 certificate：

$$
\boxed{
\min B_\infty
-
L_4(53/50)
>0.
}
$$

但以下仍沒有 machine-check：

- endpoint shortcut 的 disc-feasibility；
- open-chain support-line derivative；
- lower-stage absorption 的完整 state-space formalization；
- full equal-angle tangent-chain geometry；
- global finite-$n$ support-tangent reduction。

因此 Round 07 的最重要結果是一張 **Proof Authority Ledger**，防止後續把不同強度的 evidence 混為一談。

---

# 1. 為什麼 Round 07 不再推 theorem

Round 05 已經形成：

$$
\Gamma_n^\star
\in
\mathcal T_n
$$

的研究 proof draft。

Round 06 又找到一個真 gap，再修復。

此時最危險的行為是：

> 因為 proof 越來越漂亮，所以開始追加更多 corollary。

相反，Round 07 強制：

$$
\boxed{
\text{freeze claims}
\rightarrow
\text{raise verification authority}.
}
$$

---

# 2. Authority Ladder

本文使用：

```text
L0  NUMERICAL OBSERVATION
L1  RESEARCH DERIVATION
L2  EXACT SYMBOLIC MACHINE CHECK
L3  INTERVAL / OUTWARD-BOUND CERTIFICATE
L4  PROOF-ASSISTANT COMPILED
L5  INDEPENDENT FORMAL REPLAY
```

Round 07 只允許把實際做到的節點升級。

---

# 3. Exact check A：Perspective Hessian

令：

$$
g(q,s)
=
2q\tan\frac{s}{2q}.
$$

SymPy exact differentiation 得：

$$
g_s
=
\sec^2\frac{s}{2q},
$$

$$
g_{ss}
=
\frac{
\tan(s/(2q))
}{
q\cos^2(s/(2q))
},
$$

$$
g_{qq}
=
\frac{
s^2\tan(s/(2q))
}{
q^3\cos^2(s/(2q))
},
$$

$$
g_{qs}
=
-
\frac{
s\tan(s/(2q))
}{
q^2\cos^2(s/(2q))
}.
$$

機器 exact simplification：

$$
\boxed{
g_{qq}g_{ss}-g_{qs}^2
=
0.
}
$$

所以 Round 04 使用的 perspective Hessian rank-one identity 升級為：

```text
MACHINE-CHECKED-EXACT
```

---

# 4. Exact check B：One-Side Joint Hessian

令：

$$
\Delta_d(a)
=
\frac\pi2
-
\arccos\frac1d
-
2\arctan a.
$$

機器確認：

$$
\Delta_a
=
-\frac{2}{1+a^2},
$$

$$
\Delta_{aa}
=
\frac{4a}{(1+a^2)^2}.
$$

而：

$$
J_d(q,a)
=
\sqrt{d^2-1}
+
a
+
g(q,\Delta_d(a)).
$$

直接 chain-rule Hessian：

$$
J_{qq}=g_{qq},
$$

$$
J_{qa}=g_{qs}\Delta_a,
$$

$$
J_{aa}
=
g_{ss}\Delta_a^2
+
g_s\Delta_{aa}.
$$

SymPy exact check：

$$
\boxed{
\det\nabla^2J_d
-
g_{qq}g_s\Delta_{aa}
=
0.
}
$$

也就是：

$$
\boxed{
\det\nabla^2J_d
=
g_{qq}g_s\Delta_{aa}.
}
$$

Round 04 的 factorization 沒有 algebraic transcription error。

---

# 5. Exact check C：General Plateau Branch

Round 06 修補的 general branch：

$$
T_q(c)
=
\csc c
+
2(q+1)
\tan\frac{c}{2(q+1)}.
$$

machine differentiation確認：

$$
\boxed{
T_q'(c)
=
-\frac{\cos c}{\sin^2c}
+
\sec^2
\frac{c}{2(q+1)}.
}
$$

因此 derivative formula 本身升級到 L2。

但：

$$
T_q'(c)>\frac13
$$

仍使用 trigonometric order inequalities，尚未在 Lean 編譯。

其 status：

```text
FORMULA: MACHINE-CHECKED-EXACT
INEQUALITY: ANALYTIC-PROOF / LEAN-OPEN
```

---

# 6. Exact check D：$q=0$ Stationary Polynomial

令：

$$
B_\infty(c)
=
\csc c
+
2\cot c
+
3c-\pi.
$$

machine check 將：

$$
B_\infty'(c)\sin^2c
$$

exactly 化為：

$$
\boxed{
1-\cos c-3\cos^2c.
}
$$

因此 stationary equation：

$$
B_\infty'(c)=0
$$

在：

$$
\sin c\neq0
$$

下等價於：

$$
\boxed{
3z^2+z-1=0,
\qquad
z=\cos c.
}
$$

並 exact 驗證：

$$
z_\star
=
\frac{\sqrt{13}-1}{6}
$$

滿足 polynomial。

---

# 7. Exact check E：Continuum Stationary Cubic

Round 03 continuum endpoint condition 經平方後：

$$
4(y-1)(y+4)^2
=
y(4-y)^2.
$$

exact polynomial expansion 得：

$$
\boxed{
3y^3+36y^2+16y-64=0.
}
$$

此 algebraic reduction 亦升級至：

```text
MACHINE-CHECKED-EXACT
```

注意：

> 這只 certificate algebraic transformation；平方以前的 sign conditions 仍屬 analytic proof responsibility。

---

# 8. Exact check F：One-Segment Boundary Endpoint

Round 05 使用：

$$
h(x)
=
\frac{x}{\sqrt{1+x^2}}
+
1
-
\frac{2}{1+x^2}.
$$

machine exact substitution：

$$
x=\frac1{\sqrt3}
$$

得：

$$
\boxed{
h(1/\sqrt3)=0.
}
$$

其 interval 上：

$$
h(x)\le0
$$

仍需 order proof，不因 endpoint identity 而自動成立。

---

# 9. Interval Certificate

Round 07 重新獨立執行 80-decimal interval arithmetic。

對：

$$
z_\star
=
\frac{\sqrt{13}-1}{6}
$$

計算：

$$
B_\infty(c_\star),
$$

並計算 explicit competitor：

$$
L_4(53/50).
$$

最後：

$$
B_\infty(c_\star)-L_4(53/50)
$$

的完整 interval strictly positive。

此 certificate 存於：

```text
WSFC_R07_machine_certificate.json
```

及 runnable：

```text
wsfc_round07_machine_verify.py
```

並已由另一個 Python process 實際執行：

```text
WSFC-R07 MACHINE CERTIFICATE: PASS
```

---

# 10. Lean Toolchain Reality

本輪檢查目前 execution container：

```text
lean    NOT FOUND
lake    NOT FOUND
elan    NOT FOUND
```

所以不允許寫：

```text
LEAN VERIFIED
```

本輪只建立：

```text
WSFC_R07_Formalization_DRAFT.lean
```

這是 formalization target source。

---

# 11. Current mathlib API Mapping

依目前 mathlib4 documentation，可使用：

```text
Real.hasDerivAt_tan
convexOn_of_deriv2_nonneg
StrictConvexOn.map_sum_lt
StrictConvexOn.map_sum_eq_iff
Real.cos_pi_div_three
Real.sin_pi_div_three
Real.tan_pos_of_pos_of_lt_pi_div_two
```

所以 analytic formalization 不需要自建整個 trigonometric calculus。

---

# 12. Lean Layer 的第一批 Targets

## 12.1 Plateau derivative

目標：

$$
\boxed{
\operatorname{deriv}T_q(c)
=
-\frac{\cos c}{\sin^2c}
+
\frac{1}{
\cos^2(c/(2(q+1)))
}.
}
$$

## 12.2 Plateau derivative lower bound

在：

$$
q\ge1,
$$

$$
\frac\pi3
\le
c
\le
\frac\pi2,
$$

證：

$$
\boxed{
T_q'(c)>\frac13.
}
$$

預計只需：

$$
\cos c\le\frac12,
$$

$$
\sin^2c\ge\frac34,
$$

及：

$$
\sec^2\theta\ge1.
$$

## 12.3 Stationary polynomial

formalize：

$$
B_\infty'(c)=0
\Rightarrow
3\cos^2c+\cos c-1=0.
$$

這一層最適合先進 Lean。

---

# 13. Geometry Kernel 尚未 Machine-Check

真正困難的不是上面 algebra。

而是：

```text
EndpointShortcutOrCollapse
InteriorSupportRadiusMonotone
AllSurvivingSideLinesTangent
ZeroSegmentAbsorbs
CollinearSegmentsAbsorb
SupportOrderSwapPassesThroughCollision
```

它們需要正式資料結構：

- 2D point；
- segment；
- polygonal chain；
- segment count；
- Euclidean length；
- unit disc；
- segment/disc avoidance；
- convex normal order；
- support line；
- tangent relation。

因此 Round 07 不再把「幾何直覺」包進 scalar formulas 裡。

---

# 14. Proof Authority Ledger

本輪建立：

```text
WSFC_R07_Proof_Authority_Ledger.csv
```

目前最關鍵分類：

```text
Perspective Hessian              MACHINE-CHECKED-EXACT
J determinant factorization      MACHINE-CHECKED-EXACT
Plateau derivative identity      MACHINE-CHECKED-EXACT
q=0 stationary polynomial        MACHINE-CHECKED-EXACT
q=0 numerical separation         MACHINE-CHECKED-INTERVAL
Continuum cubic algebra           MACHINE-CHECKED-EXACT

Plateau derivative > 1/3         ANALYTIC / LEAN-OPEN
Endpoint shortcut                RESEARCH / LEAN-OPEN
Interior support monotonicity    RESEARCH / LEAN-OPEN
Equal-angle geometric theorem    ANALYTIC / LEAN-API-MAPPED
Global reduction                 RESEARCH THEOREM CHAIN
```

---

# 15. 這輪最重要的認識

Round 07 顯示：

$$
\boxed{
\text{machine-checkable}
}
$$

不是一個二值標籤。

真正狀態是：

$$
\boxed{
\text{symbolic core checked}
+
\text{interval facts checked}
+
\text{geometry kernel open}.
}
$$

這比把整篇論文標成：

```text
FORMAL / NOT FORMAL
```

更準確。

---

# 16. 下一步

Round 08 應該只做 **Geometry Kernel Formalization**，不碰新的 broadworm corollary。

最低目標不是一次完成 main theorem。

而是先讓一個 theorem prover 真正 compile：

$$
\boxed{
\text{EndpointShortcutOrCollapse}
}
$$

與：

$$
\boxed{
\text{InteriorSupportRadiusMonotone}.
}
$$

一旦這兩個 geometry lemmas machine-check，Support-Class Necessity 的最大不確定層會再大幅縮小。

---

# 結論

Round 07 把 WSFC verification 從：

$$
\text{「這個推導看起來對」}
$$

推進到：

$$
\boxed{
\text{哪些式子已被機器 exact 驗過，
哪些數值已被 interval certificate 包住，
哪些幾何還只是研究證明。}
}
$$

目前：

$$
\boxed{
\text{Algebraic Core}
}
$$

已開始真正 machine-check。

而下一階段最重要的工作不是更多數值，而是：

$$
\boxed{
\text{formalize the geometry kernel}.
}
$$

===END===