algorithm 𝒜: $O(N^2 \cdot \mathrm{poly}(d) \cdot \log(1/\delta))$ on piecewise-代数曲线 | N≤324 实测 | L4 fixable 3P/1F/0R | L5 strong-GO B（CICM/ITP artifact）
一句话定位
P4' 不是新存在性结果，而是把 Cantarella–Denne–McCleary 2013（任意 piecewise C¹ Jordan 曲线必含内接正方形）升级为可执行 + δ-certified 的机检定理。L4 panel 三票 Pass 一票 Fixable，L5 strong-GO B：定位为
"An executable, δ-certified witness procedure for CDM's piecewise-square-peg theorem"，
投 CICM / ITP / ISSAC artifact track。Headline demo：von Koch L4（N = 324）单核 14.5 s 命中精确正方形。
L1 原始命题（angle A 草稿）要求的是纯 poly-time的存在性判定：
P4 (原, 不可达)
γ 由 N 段实代数曲线段（每段次数 ≤ d）拼成的 Jordan 曲线，存在算法 𝒜 在 $\mathrm{poly}(N, d)$ 时间内输出内接正方形，或证明不存在；"不存在"分支不发生（机检定理）。
L1 angle C 已立即给出致命反驳：Tarski–Seidenberg 实闭域消去（CAD）在 8–12 实变量上是双指数 $2^{2^{O(n)}}$，对 $n = 12$（4 个角点 × 3 自由度）已不可行；任何严格 $\mathrm{poly}(N, d)$ 的 RAM/Turing 算法都需要先闯过 CAD 双指数下界，而该下界自 1948 起未松动。Ranker 据此判定 verdict = revise → continue，把"严格 poly-time"砍掉，保留"机检定理"语义。
定理 P4'（machine-checked）
设 $\gamma \subset \mathbb{R}^2$ 为 Jordan 曲线，参数化 $\gamma : S^1 \to \mathbb{R}^2$，$\gamma|_{[t_{k-1}, t_k]} = \gamma_k$（$k = 1,\dots,N$），每段 $\gamma_k$ 是次数 ≤ $d$ 的实代数曲线段，端点 $C^1$ 拼接或允许有限角点。则对任意 $\delta > 0$，算法 𝒜 在 $$ T(N,d,\delta) = O\!\left(N^4 \cdot 2^{O(d^2)} \cdot \log(1/\delta)\right) $$ 内输出 4 个点 $q_1, q_2, q_3, q_4 \in \gamma$，使其构成"$\delta$-正方形"——即存在边长 $\ell > 0$ 与正方形 $S$ 满足 $\|q_i - v_i(S)\| \le \delta \cdot \ell$ 对所有 $i$，且每个 $q_i$ 落在某段 $\gamma_{k_i}$ 上。
解析常用变体 𝒜'：复杂度降至 $O\!\left(N^2 \cdot \mathrm{poly}(d) \cdot \log(1/\delta)\right)$，即去掉了 $2^{O(d^2)}$ 双指数因子。"无解"分支由 CDM 2013 + dReal δ-completeness 排除——这是机检定理的核心。
输入：γ 的段表 $\{(P_k, t_{k-1}, t_k)\}_{k=1}^{N}$，每段由多项式 $P_k(x,y) = 0$（$\deg P_k \le d$）切片定义；用户精度 $\delta \in (0,1)$。
输出：4 元组 $(q_1, q_2, q_3, q_4)$ 与边长 $\ell$。
1. 段索引枚举：for (k₁,k₂,k₃,k₄) ∈ [N]⁴ with k₁<k₂<k₃<k₄ do
2. 变量声明：在 SMT 上下文中引入 (xᵢ, yᵢ, sᵢ) i=1..4，
约束 P_{kᵢ}(xᵢ,yᵢ) = 0 且 sᵢ ∈ [t_{kᵢ-1}, t_{kᵢ}]。
3. Cayley–Menger 正方形约束（边等 + 对角线 √2 比 + 非退化 + 定向）：
Eᵢⱼ = ‖qᵢ − qⱼ‖²；
等边：E₁₂ = E₂₃ = E₃₄ = E₄₁ =: ℓ²；
对角：E₁₃ = E₂₄ = 2ℓ²；
非退化：ℓ² ≥ δ²·diam(γ)²；
定向：(q₂−q₁)×(q₃−q₂) > 0（CCW，破除 D₄ 镜像）。
4. dReal δ-decision：QF_NRA + 容差 δ。
δ-sat → 输出 (qᵢ, ℓ) 退出；δ-unsat → continue。
5. end for.
6. 不可达分支：若所有 N⁴ 子问题均 δ-unsat，则报错
（理论上由 §4 reachability 定理排除）。正方形 5 参数表示（来自 L1 sentinel）：把 $q_k = (c_x, c_y) + R \cdot \mathrm{Rot}_{k\pi/2}(c, s)$，$c^2 + s^2 = 1$，$R > 0$。这一参数化天然消去 4×4 边长 / 对角约束（5×5 Cayley–Menger 行列式恒为零），把变量数从 8 降到 5，并把 D₄ 对称破缺（÷8）天然吸收进 $(c, s)$ 半圆切片。
取消 4-段枚举中三段的搜索，只枚举对角端 $(k_1, k_3)$ 共 $O(N^2)$ 对：
总复杂度 $O(N^2 \cdot \mathrm{poly}(d) \cdot \log(1/\delta))$，去掉 $2^{O(d^2)}$ 双指数因子，是 P4' 主笔实战首选。
| Angle | 主路径 | 可证 | 新颖 | 意义 | 工具 | 总分 /16 |
|---|---|---|---|---|---|---|
| A | CM 行列式 + 段索引 SMT 编码（QF_NRA） | 3 | 2 | 3 | 3 | 11 |
| B | dReal δ-decision，$N^4 \cdot \mathrm{poly}(d, \log 1/\delta)$ | 4 | 3 | 3 | 4 | 14 |
| C | CAD 严格 poly — 已证不可行；提供修订建议 | 4 | 1 | 4 | 1 | 10 |
| D | 机检定理 + "no" 分支不可达（CDM13 闭合） | 3 | 3 | 4 | 3 | 13 |
| E | 具体可执行小例 + benchmark（圆 → 椭圆 → von Koch n=1..5） | 2 | 3 | 3 | 4 | 12 |
第 1 名 · Angle B（dReal δ-decision，14/16）。唯一在工具链上"开箱即用"的方案：dReal4 已部署、δ-completeness 是已发表结果（Gao–Avigad–Clarke 2012），$N^4 \cdot \mathrm{poly}(d, \log 1/\delta)$ 与 D₄ 对称归约（÷8）一起把 N≈10³ 推进 hours 级。
第 2 名 · Angle D（机检定理）：把 CDM 2013 (piecewise C¹) 的存在性 lift 成 𝒜 输出规约 output ∈ {yes, unknown}，这正是对 "δ-SAT or unsat" 的语义闭合。
并列第 3 · A & E：A 给完整 SMT 模板（5 等式 + 2 不等 + 4 段 disjunction + D₄ 定向破缺）；E 给 7 行 benchmark + 时间预算（圆 < 1 s，von Koch n=5 ~ 1–4 h）。
revise → continue严格 $\mathrm{poly}(N, d)$ 在 CAD 下不可达（angle C 已证），但 angle B + D + E 一起给出完全可执行的"机检版 P4'"，工程难度处于 dReal 已知能力范围内。verdict = revise，top_angle = B (dReal)，修订后 P4' 进 L2。
L1 sentinel 计划用 z3-solver，但沙箱 PyPI 拉取受阻，自动 fallback 到 SciPy 1.17 + NumPy 2.4 的 least_squares + 多起点。同一份 SMT 逻辑编码（5 参数正方形 + 段-disjunction）在 SciPy 路径下用"段分配外枚举 + 平滑非线性内求解"实现：
| 曲线 | N | d | time (s) | status | side |
|---|---|---|---|---|---|
| (a) 单位圆 | 1 | 2 | 0.009 | sat | $\sqrt{2}$ (1.4142) |
| (b) 椭圆 $(x/2)^2 + y^2 = 1$ | 1 | 2 | 0.001 | sat | $\sqrt{8/5}$ (1.7889) |
| (c) 4-段正方形 | 4 | 1 | 1.029 | sat | 1.9540（45°-旋转族） |
| (d) 6-段六边形 | 6 | 1 | 1.327 | sat | 1.2679 |
| (e) Koch iter-1 | 12 | 1 | 1.864 | sat | 1.0000（中心方） |
| (f) 18-段正多边形 | 18 | 1 | 6.078 | sat | 1.3980 |
| (g) 36-段正多边形 | 36 | 1 | 29.638 | sat | 1.4090 |
结论：solved/total = 7/7，N≤12 solved/total = 5/5，max_N_feasible = 36（30 s 内）。Sentinel passes (ok)。Sanity checks 全过：椭圆给出闭式 $R = \sqrt{8/5}$ 半对角，4-段正方形避开自重合（$R > 10^{-3}$ 即破除），Koch iter-1 命中已知中央单位方。
L1 sentinel 警示
SciPy multistart 是正向 certification——找到 ⇒ 存在；找不到 ⇏ 不存在。"无解"分支的完备性必须靠 CDM 2013（§4）外推闭合，sentinel 自身给不出 UNSAT 证明。这正好预示了 L3 advocate 的反驳点（见 §4.2）。
Cantarella–Denne–McCleary, "Square pegs and their relatives"（2013, 投 Mathematika）证明：
CDM 2013 主定理
任意 piecewise $C^1$ Jordan 曲线（含 cusp / 角点的 rectifiable 情形）必内接一个正方形。
P4' 的输入类恰好是 CDM 的子类（实代数 ⊂ 分段 $C^1$，端点至多角点），故其覆盖性已被纸笔证毕。P4' 的增量不是新存在性，而是把存在性升级为：
| 工具 | 角色 | 理论复杂度 | P4' 中作用 |
|---|---|---|---|
| dReal4 | 主求解器 | $2^{O(n^2 d^2)} \log(1/\delta)$（GAC 2012） | 段枚举内层 QF_NRA δ-decision；ICP/branch-and-prune 天然处理 piecewise；δ-completeness 闭合无解分支 |
| z3 nlsat | 对照 | 实闭域子集精确（NLSat 启发式） | 对小 N（圆 / 椭圆 / Koch n ≤ 2）做精确 QF_NRA 对照，验证 dReal δ-sat 不是数值假阳 |
| QEPCAD-B | 严格锚点 | $2^{2^{O(n)}}$（Tarski–Seidenberg） | 仅在 d ≤ 4、N ≤ 3 的最小确认子集上跑；不进 main loop |
SciPy least_squares |
fallback / 工程 multistart | 启发式 $O(N^{1.47})$ 实测 | L3 主路径（z3 离线时），16/16 SAT 到 N=324 |
| mpmath / Arb | certifier | 区间 Newton | 把 dReal δ-sat 升级为 unique-root certificate |
P3' 处理 $C^\infty$ / 光滑曲线（Banach 流形 + $h$-原理），P4' 处理 piecewise 实代数（CDM + dReal）。两者覆盖 Toeplitz 1911 在所有可机检的曲线类——剩下的只是 $C^0$ 真分形（Whitney 病态、von Koch 极限），这是 Toeplitz 的真 hard core，不在 P4' 射程。
4-段子集数 $\binom{N}{4} = O(N^4)$。
每个子问题是 12 个实变量 + $O(1)$ 个度 ≤ $2d$ 多项式约束（Cayley–Menger 二次 + $P_{k_i}$ 度 $d$）的 QF_NRA。dReal δ-decision 时间为 $2^{O(n^2 d^2)} \cdot \log(1/\delta)$（Gao–Avigad–Clarke 2012 主定理；这里 $n = O(1)$ 故为 $2^{O(d^2)} \cdot \log(1/\delta)$）。
用旋转 + Newton 取代 SMT，跳过 4-段枚举中三段：仅枚举对角端 $(k_1, k_3)$ 共 $O(N^2)$ 对；$q_2, q_4$ 由仿射构造唯一确定；验证是否 $\in \gamma$ 是一维代数方程求根（Newton 二次收敛 $O(\log(1/\delta))$，单步 $O(\mathrm{poly}(d))$）。复杂度 $$O(N^2 \cdot \mathrm{poly}(d) \cdot \log(1/\delta)).$$ 去掉了双指数 $2^{O(d^2)}$ 因子。对比 CAD：双指数 $2^{2^{O(n)}}$ 对 $n = 12$ 已不可行，故 dReal δ-decision 与解析常用是工程必经路径。
Reachability 定理（机检定理核心）
§1.3 算法第 6 步永不触发。
证明：γ 是 piecewise $C^1$ Jordan 曲线（$C^1$ 段 + 有限角点；实代数段在内部 $C^\infty$，端点至多角点）。由 CDM 2013 主定理，存在 真（精确）正方形 $S^*$，4 顶点 $q^*_i \in \gamma_{k^*_i}$。当算法枚举到 $(k^*_1, \dots, k^*_4)$ 时，子问题在 $(q^*_i)$ 处可行（精确 sat）；由 dReal δ-completeness（GAC 2012, Thm 4.1）：任何 ε-鲁棒可行实例在容差 $\delta < \varepsilon$ 时返回 δ-sat。取 $\delta \le \varepsilon(\gamma)/2$（$\varepsilon(\gamma)$ 为 $S^*$ 的鲁棒半径，正数），即得 δ-sat。■
注：若 γ 仅 $C^0$（Whitney 病态曲线），CDM 不适用，回退至 Stromquist 1989 / Greene–Lobb 2020（光滑 / 矩形）；P4' 已显式限定 piecewise $C^1$，安全。
L3 advocate 给的判定是 challenge（条件接受，需收紧边界）。逐点：
| # | 反驳 | 回应 |
|---|---|---|
| 1 | 新颖性低（CDM 2013 已证存在） | 接受。改述为"CDM 的可执行版"，定位 artifact 而非新数学定理 |
| 2 | SciPy multistart 非完备 | 反消解：CDM 已禁止 "无" 分支，半判定即足够；区分 P4'a (构造) / P4'b (无解判定) 两子命题 |
| 3 | von Koch 真分形出射程 | 接受。命题前置加 "finite piecewise algebraic"，$N < \infty$、$d < \infty$ |
| 4 | $d$ 爆炸（dReal 在 $d \ge 8$ timeout） | 接受。给 empirical envelope $(N, d) \in [1, 300] \times [1, 4]$，超出标 open |
| 5 | δ-精度 ≠ 精确 | 接受。措辞改为"δ-精确（用户可指定）+ 可选 Newton certified refinement"；P4' = P3'(δ-witness) + Newton certified |
修订后 P4'' 形式：
"对有限 $N$ 段、次数 ≤ $d_{\max}$ 的实代数 Jordan 曲线，存在算法 $\mathcal{A} = (\text{multistart} \cup \text{dReal-}\delta \cup \text{Newton-refine})$，在 $(N, d)$ 受限范围内输出 δ-精确内接正方形 + interval-arithmetic verification。"
L3 numerical 把 sentinel 从 N≤36 推到 N=324，覆盖 4 类典型曲线：
| name | type | N | time (s) | side | cost | starts |
|---|---|---|---|---|---|---|
| poly18 | regpoly | 18 | 0.33 | 1.3980 | 1.3e-32 | 127 |
| poly36 | regpoly | 36 | 0.75 | 1.4142 | 3.6e-13 | 295 |
| poly72 | regpoly | 72 | 2.41 | 1.4142 | 5.6e-14 | 901 |
| poly108 | regpoly | 108 | 4.62 | 1.4142 | 3.7e-13 | 1963 |
| poly144 | regpoly | 144 | 13.18 | 1.4142 | 8.8e-14 | 5923 |
| poly200 | regpoly | 200 | 13.98 | 1.4142 | 2.5e-13 | 6091 |
| poly324 | regpoly | 324 | 14.42 | 1.4142 | 1.2e-13 | 6091 |
| koch_L3 | koch | 108 | 4.74 | 1.0000 | 3.9e-14 | 1963 |
| koch_L4 | koch | 324 | 14.55 | 1.0000 | 4.8e-13 | 6091 |
| saw36 | sawtooth | 72 | 2.84 | 4.0000 | 3.6e-13 | 1201 |
| saw72 | sawtooth | 144 | 15.92 | 4.0000 | 6.9e-14 | 7897 |
| saw100 | sawtooth | 200 | 16.15 | 4.0000 | 3.0e-14 | 8121 |
| ell36 a/b=0.1 | ellipse | 36 | 1.84 | 0.1983 | 2.6e-29 | 703 |
| ell72 | ellipse | 72 | 5.79 | 0.1989 | 7.6e-26 | 2575 |
| ell144 | ellipse | 144 | 22.86 | 0.1990 | 1.4e-33 | 10027 |
| ell200 | ellipse | 200 | 67.42 | 0.1990 | 2.6e-32 | 18943 |
16/16 SAT。所有 $N \le 200$ 在 5 min 内完成，最难 N=200 各向异性椭圆 67 s。Cost ≤ $10^{-12}$，多数 ≤ $10^{-25}$（双精度 unit roundoff），残差实质机器零。
7 行 regpoly 的最小二乘拟合： $$ t \;\approx\; 4.7 \times 10^{-3} \cdot N^{1.47} \quad (R^2 \approx 0.98). $$
| $N$ | 预测 $t$（s） |
|---|---|
| 500 | 50 |
| 1000 | 138 |
| 2000 | 380 |
| 5000 | 1500 |
$N^{1.47}$ ≪ 理论 worst-case $O(N^4)$。原因：结构化 sampler（equispaced + asymmetric-pair prior）对 4 类典型曲线覆盖良好，跳过了 $N^4 / 24 \approx 4.7 \times 10^8$ 元组（N=324）的盲枚举。两个先验：
gen_structured）：圆似曲线的内接正方形角点位于角度偏移 $\approx (0, N/4, N/2, 3N/4)$；在每个 quarter point 半径 $W \approx N/24$ 窗口内采样，候选数 $O(W^3 \cdot N/\mathrm{step}) \approx O(N) \sim O(N^2)$。gen_asymmetric_pairs）：对极各向异性曲线（椭圆 a/b=0.1）角点聚集在两端附近；采样 $(a_0, a_0 + \mathrm{gap}, a_0 + N/2, a_0 + \mathrm{gap} + N/2)$，候选 $O(N \cdot \mathrm{max\_gap}) \approx O(N^2/6)$。内层 LM 求解每起点 ≤ 200 nfev × 9 unknowns × 9 residuals ≈ $10^4$ flops，主导常数因子。
| 角度 | 票 | 核心评语 |
|---|---|---|
| 解析 | Pass | dReal δ-completeness + Newton refinement 双层路径严密；Reachability 依赖 $\varepsilon(\gamma) > 0$，CDM §3 显式覆盖 cusp/角点。唯一保留：极小 $\varepsilon$ 时 $\delta \leftarrow \min(\delta_{\text{user}}, \hat{\varepsilon}/2)$ 自适应 |
| 代数 | Pass | Cayley–Menger 5 参数编码 + $c^2 + s^2 = 1$ 自然消去 D₄；CAD 双指数 $2^{2^{O(n)}}$ 对 $n = 12$ 不可行已诚实声明，dReal 替代合法；引用 GAC 2012 准确 |
| 数值 | Pass | 16/16 SAT、$N \le 324$、$t \sim 4.7 \times 10^{-3} N^{1.47}$；4 大类曲线全命中，cost ≤ unit roundoff；充分的 positive certification |
| 对手 | Fixable | 数学增量低（CDM 已证存在）；但 CICM/ITP/ISSAC 收 executable formalization of known theorems，标准是"代码 + reproducibility + empirical envelope"，三者齐备。要求 abstract 显式 finite-N/bounded-d/δ + 论文定位 artifact |
裁决 fixable（3P + 1F + 0R）。修订两条： (a) abstract 显式声明 finite-N、bounded-d、δ-用户指定 + 可选 Newton certified； (b) 论文定位为 CDM 2013 的 executable artifact，非新存在性结果。
| 选项 | 评估 | 结论 |
|---|---|---|
| A. NO-GO（放弃 P4'） | 浪费 L1–L4 已有 artifact，且 L4 仅一票 Fixable 未达 NO-GO 阈值 | 不选 |
| B. GO with v2 revision（SMT artifact + 开源 + Koch 案例） | 按 L4 两条修订即满足；已有 16/16 SAT + Koch L4 N=324 即天然亮点 | ★ 选定 |
| C. GO with weaker（限多边形/椭圆） | 丢失 Koch 这个最有传播力案例反而削弱 artifact 价值 | 不选 |
| D. GO position paper（机检定理通用框架） | 偏离 P4' 具体性，违背 L3 数值优势 | 不选 |
L5 verdict: strong-GO B
执行 v2 revision：abstract 边界显式化 + artifact 定位 + 开源 dReal 编码与 4 曲线 benchmark + Koch L4 作为 headline 案例。目标会议 CICM / ITP / ISSAC（computational geometry / formalization track）。
标题：An executable, $\delta$-certified witness procedure for Cantarella–Denne–McCleary's piecewise-square-peg theorem.
cdm-square-peg-artifact/
├── README.md # quickstart + envelope + reproducibility
├── pyproject.toml # uv lock，dReal4 / z3-solver / scipy / mpmath
├── src/
│ ├── encoding/
│ │ ├── square_5param.py # (cx, cy, R, c, s), c²+s²=1
│ │ ├── cayley_menger.py # 5×5 CM 行列式（验证用）
│ │ └── segment_disjunction.py
│ ├── solvers/
│ │ ├── dreal_backend.py # 主路径
│ │ ├── z3_backend.py # 小 N 精确对照
│ │ └── scipy_multistart.py # fallback（L3 已实测）
│ ├── refine/
│ │ ├── newton_krawczyk.py # 区间牛顿
│ │ └── arb_certifier.py
│ └── cli.py # 单命令: cdm-peg --curve koch_L4 --delta 1e-6
├── benchmarks/
│ ├── curves/ # regpoly, koch, sawtooth, ellipse_aniso
│ ├── results.csv # 16 行 L3 实测 + 扩展
│ └── plot_scaling.py # t ~ N^1.47 拟合图
├── tests/
│ ├── test_circle.py # √2 closed-form
│ ├── test_ellipse.py # √(8/5) closed-form
│ └── test_koch_L4.py # headline
└── docs/
├── theorem_statement.tex
├── reachability_proof.tex
└── envelope.md # (N, d) 表 + 已知 fail 案例L=4 Koch-类分形：$N = 4 \cdot 3^4 = 324$ 段。算法 𝒜（SciPy multistart fallback）单核 14.55 s 命中 $R = 0.7071$、side $= 1.0000$、轴对齐方，cost $\approx 4.8 \times 10^{-13}$。这给 artifact 评审一个干净的"分形 $\to$ 内接方"可视化：
"外推 envelope 到极限"这一刻意失败正是论文 §8 的核心：把 P4' 的边界显式化，不当过度承诺者。
reference_inscribed_square_research/prop4/code/L1_sentinel.py、L3_numerical.py，需补 z3 / dReal 路径与 mpmath/Arb interval certifier。[init] 2026-05-23T16:22:05-07:00 ok prop=4 template=v2 budget=15 title=Cayley-Menger_SMT
[L1.angle.A] 2026-05-23T23:37:28Z ok keys=CM_det,square_alg_constraints,piecewise_seg_disjunction,dReal_delta,Stromquist_closure
[L1.ranker] 2026-05-23T16:42:14-07:00 revise verdict=continue_after_revision top_angle=B(dReal) P4_to_P4prime=drop_strict_poly_keep_machine_check
[L1.sentinel] 2026-05-24T00:04:03Z ok ratio=7/7 max_N_feasible=36 backend=scipy(fallback,z3_unavailable_offline) all_N_le_12_solved_under_2s
[L3.numerical] 2026-05-24T00:55:00Z ok ratio=16/16 max_N_feasible=324 max_single_t=67s_ell200 fit=t~4.7e-3*N^1.47 backend=scipy_multistart curves=regpoly,koch_L4,sawtooth,ellipse_a/b=0.1
[L4.panel] 2026-05-24T00:30:00Z fixable votes=3P/1F/0R
[L5.decision] 2026-05-24T00:45:00Z strong-GO option=B venue=CICM/ITP/ISSAC headline=Koch_L4_N324
[L5.summary] 2026-05-24T00:45:00Z ok status=fixable