# WSFC Round 13 ## Compiler Soundness Layer：獨立 Sturm Checker、Root Completeness 與 Atomic-Cell Sign Invariance **English Title:** *Compiler Soundness Layer: Independent Sturm Checking, Root Completeness, and Atomic-Cell Sign Invariance* **文件代號：** `WSFC-R13-v0.1` **版本：** v0.1 **日期：** 2026-09-23 **作者：** Neo.K **AI 協力研究者：** Aletheia / OpenAI GPT-5.6 Sol **系列：** Worm Sequence Freedom Closure **前置：** `WSFC-R12-v0.1` **狀態：** `INDEPENDENT ROOT-COVER CHECKER / STURM-CERTIFIED ROOT COMPLETENESS / FORMAL SOUNDNESS PARTIAL` **Canonical Source：** UTF-8 Markdown --- # 摘要 Round 12 建立 generic point-to-segment certificate compiler，但 compiler 的 atomic-cell strategy 仍依賴一個關鍵假設： > parameter domain 中 relevant polynomial roots 已全部列出。 若漏掉一根，sample 一點不能代表整個 cell。 Round 13 因此加入一個獨立 trusted checker。 架構： ```text COMPILER SymPy exact QQ polynomials root generation isolating intervals ↓ candidate root-cover certificate TRUSTED CHECKER Python stdlib Fraction polynomial long division exact Sturm sequence sign variations ↓ ROOT COVER VERIFIED ``` trusted checker不 import SymPy，也不使用 `real_roots`。 對每個： $$ p(t)\in\mathbb Q[t], $$ certificate只需提供： - polynomial coefficients； - parameter domain； - exact rational roots； - irrational roots的 rational isolating boxes。 對 rational root： $$ r\in\mathbb Q, $$ checker exact 驗： $$ p(r)=0, $$ 再反覆除： $$ X-r $$ 移除全部 multiplicity。 對剩餘 polynomial，每個 isolating box： $$ (a_i,b_i) $$ exact 驗： $$ \boxed{ N_p(a_i,b_i)=1, } $$ 其中 $N_p$ 由 Sturm sequence sign-variation計算。 再驗所有 boxes 之間 gaps： $$ \boxed{ N_p=0. } $$ 所以： $$ \boxed{ \text{claimed roots} + \text{zero-root gaps} = \text{complete real-root cover}. } $$ 本輪 canonical與 irrational案例均通過 trusted checker。 另外隨機生成： $$ 150 $$ 組 rational affine-motion cases，由 compiler產生 root claims，再交獨立 checker 驗證。 結果： $$ \boxed{ 150/150\ \mathrm{PASS}. } $$ 接著是 atomic-cell sign soundness。 若 polynomial在 connected interval： $$ I=(a,b) $$ 沒有 root，由 continuity + Intermediate Value Theorem： $$ \boxed{ \operatorname{sign}p \text{ 在 }I\text{ 不能改變}. } $$ 所以： $$ \boxed{ \text{root-free cell} + \text{one sample sign} \Rightarrow \text{whole-cell sign}. } $$ 這使 Round 12 的 sample-based phase classifier第一次有 theorem-backed foundation。 目前 mathlib 已提供 `Polynomial.sturmSeq`、`List.signVariations`、Intermediate Value Theorem，以及 quadratic discriminant theorem。citeturn923944search1turn923944search0turn848635search3turn848635search2 由於目前 WSFC relevant polynomials degree： $$ \le2, $$ 正式 Lean 第一版可以先走 quadratic-specialized route；runtime trusted checker則保留 Sturm後端。 --- # 1. Trust Separation 核心原則： $$ \boxed{ \text{Generator} \neq \text{Trusted Checker}. } $$ 否則同一個 root algorithm 的 bug 可能同時存在於 producer 與 verifier。 --- # 2. Trusted Polynomial Kernel checker自行實作： ```text evaluation derivative long division rational-root removal Sturm sequence sign variations root count ``` scalar全部為： $$ \mathbb Q. $$ 沒有 floating tolerance。 --- # 3. Rational Root Verification 對 claimed： $$ r\in\mathbb Q, $$ 先 exact 驗： $$ p(r)=0. $$ 再： $$ p\leftarrow p/(X-r) $$ 直到： $$ p(r)\neq0. $$ 所以 repeated rational root 不會污染後續 isolating interval endpoints。 --- # 4. Algebraic Root Isolation 對 irrational root，trusted checker不信 radical display string。 只驗： $$ (a,b)\subset\mathbb Q $$ 滿足： $$ p(a)\neq0, \qquad p(b)\neq0, $$ 以及： $$ \boxed{ N_p(a,b)=1. } $$ 因此： ```text 2 - sqrt(3)/2 ``` 只是 display metadata。 真正 authority 是 rational box + Sturm count。 --- # 5. Root Completeness boxes： $$ (a_1,b_1),\ldots,(a_k,b_k) $$ 之外，checker逐段驗： $$ (t_0,a_1), $$ $$ (b_1,a_2), $$ $$ \ldots, $$ $$ (b_k,t_1) $$ 全部 root count： $$ 0. $$ 所以： $$ \boxed{ \text{沒有未列出的 real root}. } $$ --- # 6. Sturm Sequence $$ S_0=p, $$ $$ S_1=p', $$ $$ S_{j+1} = -\operatorname{rem}(S_{j-1},S_j). $$ 對非 root endpoints： $$ a0, $$ $$ p(y)<0, $$ 由 IVT 必存在： $$ z $$ 使： $$ p(z)=0. $$ 矛盾。 所以： $$ \boxed{ \text{root-free} \Rightarrow \text{sign constant}. } $$ 這是 atomic-cell sampling的 theorem foundation。 --- # 8. Feature Invariance Round 12 nearest feature由： $$ A, \quad N, \quad S $$ signs決定。 safety由： $$ H_0, \quad L, \quad H_1 $$ 決定。 若這些 polynomial在 atomic cell內都 root-free： $$ \boxed{ \text{feature + active safety sign constant}. } $$ --- # 9. Tests ```text canonical root cover PASS irrational root cover PASS random fuzz 150/150 PASS ``` fuzz只壓 generator/checker interface，不替代 general proof。 --- # 10. Runtime 與 Lean 的分工 目前 degree： $$ \le2. $$ 所以 Lean v1 可先利用 quadratic discriminant。 runtime checker則保留 Sturm，為 future higher-degree motion準備。 建議： $$ \boxed{ \text{Runtime = Sturm}, \qquad \text{Lean v1 = Quadratic Specialized}. } $$ --- # 11. Remaining Formal Layer 現在不再需要 formalize： > compiler是否漏 root？ 但需要 formalize： $$ \boxed{ \text{RootCoverSound} \Rightarrow \text{RootFreeCell}, } $$ 以及： $$ \boxed{ \text{RootFreeCell} \Rightarrow \text{SignInvariant}. } $$ 後者主要就是 IVT。 --- # 12. Compiler Soundness DAG $$ \boxed{ \begin{aligned} &\text{Affine Geometry}\\ &\Downarrow\\ &\text{Quadratic Polynomials}\\ &\Downarrow\\ &\text{Compiler Root Claims}\\ &\Downarrow\\ &\text{Independent Sturm Check}\\ &\Downarrow\\ &\text{Complete Root Cover}\\ &\Downarrow\\ &\text{Root-Free Cells}\\ &\Downarrow\\ &\text{IVT Sign Invariance}\\ &\Downarrow\\ &\text{Feature/Safety Invariance}\\ &\Downarrow\\ &\text{Segment Certificate Soundness}. \end{aligned} } $$ --- # 13. 下一步 Round 14 進： $$ \boxed{ \textbf{Phase Safety Formalization}. } $$ 要正式處理： - fixed endpoint phase； - interior projection phase； - moving endpoint phase； - degenerate segment phase； - phase cell如何 compose成完整 parameter-domain safety。 --- # 結論 Round 13 關掉的是： $$ \boxed{ \text{「compiler 有沒有漏 root？」} } $$ 這個 trust gap。 compiler仍可複雜地產生 root claims，但獨立小 checker決定 root cover是否完整。 因此現在開始有： $$ \boxed{ \text{root completeness} \rightarrow \text{sign invariance} \rightarrow \text{phase invariance}. } $$ WSFC compiler已進入真正 proof-carrying compiler 的結構。 ===END===