# 3-4-5 三角形：1000 个随机初始配置

该实验检验从随机坐标开始的局部非线性求解行为，单独统计成功、停滞、迭代上限及错误。它独立于 [400 模型配置套件](VALIDATION.md)，不将其计入原有 400 个案例，也不以截图中的示例数字代替实测结果。

## 模型与初值

- 三条约束：AB=3、BC=4、AC=5；例如 A=(0,0)、B=(3,0)、C=(3,4) 是一个解析解。
- A、B、C 的六个初始坐标分别从 (-10,10) 生成。所有初值在求解前确定，不从已知解附近加扰动，也不按结果筛选种子。
- 不添加固定点、水平或角度约束。位置、方向和镜像分支均不指定，非退化解保留平移与旋转的 3 个局部自由度。因此核对三条边长，不要求坐标等于上述解析解。
- 固定基础种子 20261022；第 i 项种子为 `20261022 + 97*i`，i=0…999。使用 Park–Miller / Schrage 整数生成器，预热五步后，按 A.x、A.y、B.x、B.y、C.x、C.y 顺序抽样。
- 使用默认 `SolveOptions`：长度容差 1e-7、角度容差 1e-8、数值秩阈值 1e-9、最多 200 次迭代。每项只求解一次，不重启、不修正初值、不替换失败样本。

[MoonBit 程序](../cmd/random_triangle/main.mbt) 使用公开 API 建模和求解；[Node 脚本](../scripts/random_triangle.cjs) 复算全部初始坐标，并从返回坐标独立计算三条边长。报告为 `Satisfied` 时，最大独立残差比必须不超过 1.00001（给独立浮点计算保留 1e-5 的比值裕量），与报告的逐项误差比及最大值相符，局部自由度为 3，保存的几何与结果相同。

未达标结果按原样统计为 `Stalled` 或 `IterationLimit`，并核对保存的几何没有改变；`Err` 统计为 `Invalid`，保留错误原文。这一标签包含输入或求值错误，不表示已证明模型无解。输入不符、虚假成功、非有限输出、诊断不符或保存几何异常会导致检查脚本失败；正常的停滞本身不会被当成检查器错误或隐藏。

每次另执行 3 项定向故障注入，确认检查器可拒绝虚假成功、非有限坐标和失败时改变几何。这些不计入 1000 个随机配置。

## 2026-10-22 实测结果

JS 后端；Windows x64；MoonBit 0.10.15。

| 求解状态 | 数量 |
| --- | ---: |
| Satisfied | **1000** |
| Stalled | 0 |
| IterationLimit | 0 |
| Invalid | 0 |
| 总计 | **1000** |

1000 个成功结果全部通过独立边长检查，未发现虚假成功或诊断 / 几何应用不符。迭代次数最少 3、中位数 4、最多 24；最大独立残差比约 0.939。三项检查器故障注入均通过。

完整环境、参数和源码 SHA-256 见[汇总快照](validation-results/random-triangle-js.json)；全部 1000 个初值、候选坐标、保存坐标、边长、状态、迭代次数和诊断见[逐案例 CSV](validation-results/random-triangle-js.csv)。CSV 的 SHA-256 记录在汇总中，换行按 LF 规范化核对。

这是这个固定语料和三条边长模型的实测统计，不承诺任意初值、不同坐标范围、奇异配置、更多约束或其他后端均有同样成功率；也没有据此声明全局收敛。该实验的 3 个自由度与固定基线的三角形测试不同，不能直接混为同一成功率指标。

## 轻量复现

需要 MoonBit 0.10.15+、Node.js 18+，仅使用标准库。

```sh
moon check cmd/random_triangle --target js --deny-warn
node scripts/random_triangle.cjs --check --target js
# 仅输出原始记录：
moon run cmd/random_triangle --target js
```

脚本生成 `_build/random-triangle/js.jsonl`、`js.json`、`js.csv` 和 `js.stderr.log`，保留真实结果及逐案例检查。用 CSV 中的 index 和 seed 可从生成规则精确重建指定初值。`--check` 核对 CSV 完整性，并报告快照是否对应当前源码，不要求其他平台逐位复现同一统计。

修改实验或核心源码后，应审阅真实数据，再用 `node scripts/random_triangle.cjs --write --target js` 更新快照及 CSV。脚本不会要求 1000 项全部成功才能写入统计；停滞及错误会照实保留，只有检查器发现的正确性异常才阻止写入。

本次按轻量验证要求只进行了目标包 JS 编译检查、脚本语法检查和这项 1000 配置实验；未重跑全量回归、四后端矩阵、400 配置套件或源码包消费验证。本次提交跳过自动全量 CI；工作流已加入该实验，维护者显式选择完整验证时会执行并保存原始结果，默认轻量 CI 不执行该实验。

类型化错误升级后，以上数据保留为历史测量，本次未重跑。`--check` 独立验证本次新运行的结果，并在源码指纹不同时明确提示历史快照；不会重写已提交测量。加 `--require-current-snapshot` 可要求快照必须对应当前源码，不符即失败。CSV 完整性及当前结果正确性检查仍保留。需要刷新证据时，审查完整实测结果后显式使用 `--write`。