源码核查、测量与证伪方法
研究总览 · 2026-09-20
2026-09-20 的源码/构件快照和历史测量；整理未重新运行实验，未知项仍为未知。
11. 实际代码落点与已证实差距
Section titled “11. 实际代码落点与已证实差距”| 当前接线点 | 已有能力 | 新设计所需差异 |
|---|---|---|
packages/aira-contracts/src/exact-cad-plan-types.ts 与 schema |
当前计划、要求、AMIR 类型 | 设计问题、变量开放域、结构选择、结果范围；同一契约 |
packages/aira-contracts/src/exact-cad-plan-schema/requirements.ts |
要求的机器可读定义 | 非规则孔集合的最小净距/边距等关系；不固定求解后的中心作为原要求 |
apps/web/src/authoring/exact-cad-plan-assertions.ts |
要求与几何修改同 Patch | 设计关系的编译和 requirement ID 对应 |
packages/aira-geometry-kernel/src/aira/exact-product-solve/ |
CasADi/IPOPT、显式句柄释放、装配检查 | 同一内核内使用成熟 HiGHS 绑定的会话适配、关系分类、稀疏行来源和硬约束 |
apps/web/vite-sealed-exact-runtime.ts |
CasADi 核心与 IPOPT 的静态发布 | HiGHS 独立按需构件；禁止发布 CasADi 的重复 HiGHS 插件及闲置 solver |
apps/web/src/authoring/program-compilers/program-builder.ts |
build/replace program、参数及 Patch | authoring 只改源设计；求解产生的具体构造进入 Realization，不覆盖源关系 |
packages/aira-geometry-kernel/src/aira/program-compartment/executor.ts |
私有 WASM Worker、SES、资源与输入归属 | 继续复用，禁止第二执行器 |
apps/web/src/feature-graph/exact-feature-graph-assertion-checker-v0.4.ts |
solid/bounds/holeArray 等实际检查 | 关系所需的实际测量与三态语义 |
packages/aira-cad-tools/src/tools.ts |
唯一 AI SDK 工具清单 | 同一计划契约的语义编辑；求解接入共享候选求值，UI 与直接 Patch 均不得绕过 |
apps/web/src/operations/phase1-exact-operation-session/ |
propose/preview/validate/commit/discard | 源候选不可变，Realization、验证与 revision/head 原子持久化 |
tools/capability-explorer/ |
固定输入、原生 MCP、同输入对照和独立 STEP 回读 | 关系设计族、连续编辑链和与要求对应的独立检查 |
此表是源码差距快照；实际改动与依赖只维护在当前实施方案，尤其包括原表未列全的 Rust 修订身份、资源存储及恢复链。真实需求是结构自适应、持续意图和可解释排除；上游设施是已有 OCCT/PlaneGCS/CasADi，以及选定的独立 HiGHS 绑定。语义编译、持久会话、检查范围与事务接线由 Aira 承担，不复制上游算法和绑定。
当前 holeArray requirement 为 world-Z 贯通圆孔的规则 x/y 阵列，包含 fixed-centers/fixed-edge-margins。它不能直接表达一般 3–2–3 集合的所有关系。numericRange 只检查声明值，并不自动证明某个自编测量程序正确。
12. 本机实验与性能证据
Section titled “12. 本机实验与性能证据”12.1 环境和版本
Section titled “12.1 环境和版本”- 研究时 HEAD：
0ced0556f8db5e02c4edcafea9439da480b77a15；工作区有用户已有未提交修改，本文不将 HEAD 当作全部工作区身份。 - 定稿核验时 HEAD 为
493ad5e851c50bfe4bad93e373e898e538815cf6；期间已有探索器与文档改动由外部工作提交，本研究未创建提交。两次 HEAD 间未改变本文所测 CasADi/HiGHS 二进制；其身份以以下文件哈希为准。 - Windows 11 专业工作站版 10.0.26200；Intel Core i7-13700F；Node v24.19.0，win32 x64。
- CasADi 3.8.0；IPOPT 身份记录为 3.14.19。
- 实际二进制 banner/API 核验：HiGHS 1.13.1，git
1d267d97。不以 CasADi 源码默认版本代替此核验。 libcasadi_conic_highs.so：3,768,306 bytes；SHA-25624c2465fc8443b075189205c28961290ac67f5a8362f2658e51829488d2b744a。casadi_wasm.wasm：8,558,430 bytes；SHA-256eaee01de435674570aa0fa47aaa54086b1b7050574c541f2dcb056bf62d4dac5。- 现有 IPOPT 侧模块：7,902,597 bytes。以上均为原始文件大小，不是压缩下载、初始化耗时或峰值内存。
12.2 功能探针
Section titled “12.2 功能探针”| 输入 | 实测结果 | 证明了什么 |
|---|---|---|
| 连续 x，0≤x≤5，2x=5 | Optimal，2.5 | 当前插件可求 LP |
| 连续 x，0≤x≤2，2x=5 | Infeasible | 返回不可行状态；单此状态不是独立证书 |
| 整数 x，0≤x≤5，2x=5 | Infeasible | 当前插件支持整数变量；松弛可行不能拿 LP ray 证明整数矛盾 |
| 整数 x，0≤x≤5，2x≥5，min x | Optimal，3 | 当前插件可求 MILP |
| x≥3 与 x≤2 的辅助 LP | λ=[0.5,0.5]，bᵀλ=-0.5 | 精确二进制分数证书推出 0≤-0.5 |
| 同一侧模块原生接口 | create/run/update/getBasis/setBasis/getDualRay 实际可调用 | 此路线技术可行；最终因加载成本和现成绑定选择独立部署，不能将“已有二进制”自动等同最佳部署 |
12.3 同核增量对照
Section titled “12.3 同核增量对照”固定 xorshift seed=1831565813，稀疏有界 min LP，每行 6 个正系数，变量在 [0,1]，构造已知可行起点 0.5。每次修改一行上界和一列成本。每条轨迹预热 5 次，记录连续 35 次修改；模式交替执行，避免永远让同一模式先运行。不是 35 个独立随机工业模型。
| 规模；presolve=choose | 完整 passLp 中位/P95 ms | 增量修改中位/P95 ms | 重载后恢复 basis 中位/P95 ms |
|---|---|---|---|
| 24 变量、48 行、288 非零 | 0.5531 / 0.9225 | 0.0528 / 0.2367 | 0.1142 / 0.1896 |
| 240 变量、480 行、2880 非零 | 24.2222 / 27.9911 | 0.5221 / 1.3118 | 3.2249 / 3.9733 |
大规模三组中位 simplex 迭代分别为 674、1、1；最大目标差 1.71e-11，最大独立数值违反 3.57e-11。presolve=off 对照中，三组中位耗时分别 22.9776、0.2591、1.6138 ms；最大目标差 2.16e-10、违反 1.89e-10。
小规模默认模式的增量求解均为 0 pivots，表示这一小修改轨迹未改变最优基；大规模出现 0–9 pivots。由此选择增量接口，但不据此固定全产品关闭 presolve，也不推导整个 CAD 快 46 倍。 测量比较的是同一 HiGHS 的接入策略，不是不同求解库排行榜。
12.4 证据提取对照
Section titled “12.4 证据提取对照”120 行负差分环，系数为整数，每条约束为 (x_{j+1}-x_j\le-1)。原生 ray 给出全 1 乘子，左端精确消去、右端 -120，是直接可核验的证据。
| 方法，35 次记录 | 中位 ms | P95 ms | 计时范围 |
|---|---|---|---|
| 原生 getDualRay | 0.5158 | 0.6238 | 已完成主问题无解求解后的取证调用 |
| 同库辅助 LP | 0.3670 | 0.8620 | 创建、传模型、求解、提取、销毁；不含预构矩阵 |
辅助乘子约 1/120，各分量相同，左端残差为零。上述计时不含最终有理核验；这是研究探针，不是端到端产品性能。两种方式的不同时间分布阻止“原生 ray 恒定最快”的断言。
12.5 分发形态与冷初始化对照
Section titled “12.5 分发形态与冷初始化对照”研究单独读取 npm highs@1.15.3 发布包到 TEMP，没有安装到项目。实际 API 返回核心 HiGHS 1.15.1，git 04024d7；研究源码对应 highs-js 提交 96981da1d88bbf657d81f7f3027377ba6a7e81bf。JS SHA-256：0bd23843c9795753f2276e9901eb2a1e66288547b6bcba84fa0665dc037b5c7c；WASM SHA-256：528be4365bea1d4188988646b244263f50320df55782e14d6af5bce7cd45c840。发布包
| 主构件原始大小，bytes | CasADi + HiGHS 侧模块 | 独立 highs |
|---|---|---|
| JS | 1,201,596 + 11,728,212 | 168,432 |
| WASM | 8,558,430 + 3,768,306 | 3,531,385 |
| 合计 | 25,256,544 | 3,699,817 |
| 本机 gzip9 压缩合计 | 4,351,915 | 1,258,706 |
| 本机 Brotli11 压缩合计 | 2,978,830 | 880,416 |
压缩列只是对这些文件逐个重新压缩，不是部署服务器的真实下载。列表记录研究加载的主要构件，未计全部可能的动态依赖。不能将 880 KB 的特定压缩文件组合说成“HiGHS 一定只有几百 KB”；也不能仅比较两份 WASM 而遗漏 CasADi JS 胶水。
各用 9 个全新 Node 进程，交替执行顺序，未丢弃预热；计时从 require 前到 factory 完成，CasADi 额外包括 load_conic('highs')。不含进程创建、网络、浏览器；未清操作系统文件缓存。
| 初始化指标 | CasADi + HiGHS | 独立 highs |
|---|---|---|
| 中位 / P95 ms，n=9 | 367.8385 / 420.7256 | 23.3430 / 26.9228 |
| RSS 增量中位，bytes | 109,948,928 | 15,458,304 |
P95 在这 9 个样本中为最大次序统计量，样本量不足以描述稳定长尾。RSS 增量不是峰值、WASM live allocation 或长期泄漏测量。本证据支持 LP-only 使用独立构件；即使已有任务加载了 CasADi，独立 HiGHS 也只保留一份生产部署，避免维护两个调用后端。
12.6 独立分发的功能与热更新
Section titled “12.6 独立分发的功能与热更新”在所选独立分发中实际验证 LP 2x=5 得 2.5；整数 2x=5 返回 infeasible；整数 2x≥5、min x 得 3；连续凸 QP (x^2-5x) 得 2.499999875（数值结果）。MIQP 的 run() 报 HighsError -1，与核心源码明确拒绝 MIQP 一致；不能因为模型类型同时允许 Hessian 与 integrality 就宣称可求 MIQP。HiGHS 1.15.1 实现
同 §12.3 的大规模矩阵和编辑轨迹，重新在独立绑定中比较三种模式；presolve=choose，5 次预热、35 次计时。下表采用最后一次记录，对应附录 C 源码；不挑选多次运行中的最小值。
| 所选分发内部策略 | 中位 / P95 ms | 中位 / 最大 simplex 迭代 |
|---|---|---|
| 完整 passModel 重载 | 27.7629 / 31.2372 | 674 / 778 |
| 修改一行 bounds 和一列 cost | 0.5313 / 1.1700 | 1 / 9 |
| 重载再恢复 basis | 3.3217 / 5.0802 | 1 / 9 |
最大独立数值违反 3.5632830019949324e-11，模式间最大目标差 1.7053025658242404e-11。120 行负环的原生 ray 取证中位/P95 为 0.4410/0.8178 ms，候选全 1，左端为 0、右端 -120。ray 同样在主问题求解完成后计时。
与 CasADi 附带版本相比，核心版本、绑定和测量时刻都不同，不能把跨表热耗时差归因为某个算法升级。独立分发内部的对照支持持久增量策略；冷初始化对照与现成 API 支持独立分发的选择。
12.7 没有测到的内容
Section titled “12.7 没有测到的内容”尚未完成新架构的浏览器冷加载、Worker 中断时延、长期内存增长及完整产品原生链上的 AI 对照与跨产品族成功率测量。§12.10 已有真实 OCCT 隔离构造，§17.9 已有封闭契约 AI 首答试用；二者都不等于完整产品验证。架构与选库已经确定，这些未获得的经验结论不写成已通过，也不据此自动启动实施。
12.8 同一 3–2–3 结构域：展开坐标、降维与解析判定
Section titled “12.8 同一 3–2–3 结构域：展开坐标、降维与解析判定”环境同 §12.1，Node 24.19.0、i7-13700F、当前 CasADi 3.8.0/IPOPT 3.14.19。固定 seed=20260920，48 个实例覆盖明显可行、明显不可行、精确边界与邻近边界。最小中心距归一为 D=1；P、T 为允许的最大半跨度。两种数值模型都使用零目标、初始 p=1/h=0.75，A 的初始圆心由相同参数展开。每个模型只构建一次，预热两次，随后复用参数化 Function。
- A：16 个圆心坐标，加 p、h，共 18 变量；16 条线性坐标定义、28 条孔间距离、32 条板边不等式，共 76 约束，另有 p/h 非负列界。
- B：仅 p、h；(p\ge1,h\ge1/2,p^2/4+h^2\ge1,p\le P,h\le T)，共 5 约束。
- C：用精确有理数检查 (P\ge1,T\ge1/2,P^2/4+T^2\ge1)，可行时数学见证为 p=P/h=T。
三者在固定居中对称族的纯可行性上等价，依据见 §13.1。C 不解决附加的最小移动等优化目标。A/B 用返回的 binary64 p、h 精确转成有理数，按相同结构回代全部圆心，再检查所有 28 对距离与 32 条板界；不修正参数、不用残差阈值将微小越界算通过。A 原始圆心与回代坐标的残差单列。C 的有理见证与 A/B 的浮点参数见证有不同交付表示；本实验没有检查 B-Rep。
| 指标 | A：18 变量 / 76 约束 | B：2 变量 / 5 约束 |
|---|---|---|
| 符号模型构造，单次观察 | 12.510 ms | 0.398 ms |
| solver 构建，单次观察 | 24.067 ms | 1.631 ms |
| 48 次调用延迟 P50 / P95 | 12.488 / 59.454 ms | 8.938 / 18.130 ms |
| 明显可行 16 例的调用 P50 / P95 | 5.761 / 7.703 ms | 3.577 / 5.442 ms |
| 明显可行 16 例严格参数见证 | 16 pass | 16 pass |
| 全 48 例严格参数见证 | 21 pass / 27 unknown | 22 pass / 26 unknown |
调用延迟包括函数返回或抛异常之前的时间，不含参数 DM 分配、输出提取和核验。模型构造各只测一次且 A 先 B 后，不能用于严格的编译性能排名。C 的有理条件计算 P50/P95 为 0.0047/0.0192 ms，不含十进制解析与几何见证构造；26 例判数学可行、22 例判不可行，不能写成产品交付全通过，更不应报成完整 CAD 的数千倍加速。
当前 WASM 在 A 的 18 例、B 的 20 例抛出 WebAssembly.Exception，即使 error_on_fail=false；异常后的 stats 可以保留前次 Solve_Succeeded，探针明确隔离为旧诊断，不视为本次状态。stderr 的 getrusage 不支持诊断保留于 TEMP。A 正常返回含 29 次 Solve_Succeeded、1 次 Maximum_Iterations_Exceeded，B 含 28 次 Solve_Succeeded；正常返回子集不同，不能直接算两路速度比。异常及未通过精确候选核验均记 unknown，不提升为已证无解。
一个实质边界是 (P,T)=(1.2,0.8)：按十进制有理语义为 (6/5,4/5)，上角点恰有 (P^2/4+T^2=1)。严格单调性迫使任何可行参数都等于 p=P、h=T，而两者均不能由 binary64 精确表示。因此零容差下根本不存在能够通过本探针严格核验的浮点参数见证；两路候选 unknown 不能归因于迭代不够。A/B 在装载端点时也采用浮点近似。“同域”等价针对数学模型，不能当成相同的有限精度交付域，更不能由该边界证明 C 的求解算法优于一切浮点方法。实际契约必须明确尺寸、容差与可交付表示之间的关系。
在 (1.2,0.800000001)，A 虽到迭代上限，返回参数经独立回代核验却可行。因此纯可行性候选的接受依据是检查结果，不是优化收敛标签。两种模型都没有将 C 判不可行的样本误核验为可行。
该边界的表示域证明及通用交付处理现由数值交付规约明确；此处原始输入、统计和 unknown 分类保持不变，不把补充推导写成探针已经交付成功。
结论：语义明确的等式消元与约束类归并，在这个同域问题中确实降低了数值工作；单调性又使数值搜索本身消失。边界交付误差和 WASM 异常仍是必须处理的真实工程问题，解析判定不能掩盖它们。完整源码见附录 D。
12.9 同一链式凸 QP：变量数减半，矩阵变稠密，实测仍更快
Section titled “12.9 同一链式凸 QP：变量数减半，矩阵变稠密，实测仍更快”求解 §5.6 的链问题，增加 (-0.4\le u_k\le0.4)。seed=8675309，目标 (t_k=2\sin(0.09k)+0.7\cos(0.13k)+0.05(rand-0.5))。每个 N 使用 5 次预热、15 次计量；每次输入相同、两路次序交替、每次重新创建和销毁 HiGHS 1.15.1 模型。比较原始 2N 变量的稀疏表示与消去全部 x 的 N 变量表示；均使用相同盒界和数学目标。
| N | 稀疏 / 消元变量数 | 稀疏 / 消元 Hessian 存储非零数 | 稀疏总时间 P50 / P95 | 消元总时间 P50 / P95 |
|---|---|---|---|---|
| 16 | 32 / 16 | 32 / 136 | 1.271 / 2.093 ms | 0.452 / 0.779 ms |
| 64 | 128 / 64 | 128 / 2080 | 3.584 / 5.797 ms | 1.191 / 1.795 ms |
| 128 | 256 / 128 | 256 / 8256 | 9.047 / 11.373 ms | 3.670 / 4.813 ms |
“总时间”在本表只包括 JS 装配、native 模型装载与求解，排除 WASM 初始化、结果恢复核验和销毁，也没有几何工作。N=128 时，稀疏表示求解 P50 为 8.619 ms，消元为 2.540 ms；装载则从 0.204 增至 0.863 ms。可见求解收益与表示开销确实在竞争，不能只选其中一项。
全部实例正常最优返回；从原始 x/u 重算目标、链残差和盒界，跨表示最大目标差 (1.434\times10^{-12})，最大 x 差 (2.652\times10^{-7})，最大约束违反 (6.34\times10^{-15})。这是浮点数值核对，未给出精确最优性证书。P95 每格只有 15 次样本，在本定义下接近样本最大值，不能外推稳定尾延迟。
这个实验否定了“只要消元变稠密就应拒绝”的简单规则，也没有证明完全消元在更大规模、其他求解器或更频繁编辑中最佳。它支持的裁决是：同域比较真实总成本，并保留部分消元这一中间选择。 完整源码见附录 D。
12.10 已知截面直接构造与一次复合刀具布尔的真实 OCCT 对照
Section titled “12.10 已知截面直接构造与一次复合刀具布尔的真实 OCCT 对照”使用当前 OCCT WASM，SHA-256=218e80a3fb69d62de4b44b613f64c0d99f3f8d2ad5cb5ce3aeea568805fcdcfa。输入为 80×30×4 mm 平板、8 个半径 3 mm 的贯通孔，中心为 {10,30,50,70}×{10,20}。每种方法预热 3 次、计量 20 次，执行次序交替。
A 构造 Box 与复合圆柱刀具，调用一次当前 airaNonDestructiveCut，不 simplify；与现有 holeArray 使用的几何策略一致。B 构造矩形外环、8 个反向圆内环，生成 Face 并做一次 Prism。两者均复用当前原生 API；未计入产品 AMIR、lineage、事务和完整产品检查，也没有另建几何库。
| 计时范围 | A：一次复合 cut，中位 / P95 | B：内环 Face + Prism，中位 / P95 |
|---|---|---|
| 构造及中间句柄释放 | 12.503 / 15.641 ms | 0.700 / 1.307 ms |
| 检查及结果句柄释放 | 3.804 / 6.571 ms | 6.113 / 9.007 ms |
| 每个样本两项之和 | 16.497 / 23.412 ms | 6.594 / 9.968 ms |
分位数用 nearest-rank。构造的中位耗时约减少到 1/17.85，计入同一检查集后约为 1/2.50；不能把前一倍数当端到端 CAD 加速。检查成本在 B 中更高，说明几何表示与构造途径也可能影响验收成本，不能只测 builder。
全部 40 条记录的检查包括：BRepCheck_Analyzer 的 exact method 开启且有效；1 solid/1 shell/14 faces；8 个完整圆柱孔壁的中心、半径、轴方向绝对值、U 跨度 2π、V 跨度 4；平面 wire 数量为 [1,1,1,1,9,9]；体积与 (80\cdot30\cdot4-8\pi\cdot3^2\cdot4) 的误差小于 1e−7 mm³。实际最大体积差约 3.64e−12 mm³；记录中均为 36 edges/24 vertices，包络为 [0,0,0] 到 [80,30,4]。边/点数和包络在原探针记录但未列为 pass 的必要条件。OCCT 的 exact method 名称不等于对任意实体提供精确代数证明。
B 的圆柱参数轴为 −Z，A 为 +Z，已经观察到参数化差异。因此点集/要求一致不等于持久名字和构造历史相同。§9.5 的替代范围仍需遵守，不能静默改写已有引用。
一次新 Node 进程的 JS 导入、WASM 读取与初始化合计为 124.468 ms，OS 文件缓存未控制，不能作为浏览器冷启动结论。上述热对照固定一个几何输入，没有覆盖退化、相切、大量孔或其他尺寸分布。
结论：在已证明的几何域内，数学结构能够实际消除通用三维布尔工作；这一收益不需要换库，也不需要让 AI 模仿更多操作。完整源码见附录 D。
12.11 部分消元：校准与独立留出中的实际平衡
Section titled “12.11 部分消元：校准与独立留出中的实际平衡”继续使用 §12.9 的相同凸链模型，比较 B=1、4、16、64、N。每个块起点保留为变量，末端 xN 不保留；因此 B=1 为 2N−1 变量/N−1 等式，与上节完整稀疏模型不是同一种数值表示。两者覆盖的数学问题相同。正式装配使用 §5.6 的块内闭式，时间与存储均按非零量 O(NB) 增长，不用 O(NB²) 的逐项外积装配人为惩罚大块。6 组小问题含短末块，闭式与独立外积构造的 Hessian 完全相等，线性项最大差 1.39e−16。
校准使用 seed=8675309，每个 N 每种 B 为 3 次预热、9 次计量，轮换并反转方法次序；每轮同输入、模型新建。表为装配＋原生装载＋求解的 P50/P95（ms），不含恢复、核验、销毁和初始化。
| N | B=1 | B=4 | B=16 | B=64 | B=N |
|---|---|---|---|---|---|
| 128 | 7.05 / 9.07 | 4.76 / 6.64 | 4.18 / 4.95 | 4.77 / 5.84 | 2.78 / 3.39 |
| 256 | 27.44 / 30.85 | 19.73 / 20.19 | 17.70 / 19.45 | 18.50 / 20.10 | 15.29 / 15.73 |
| 512 | 145.35 / 166.11 | 110.92 / 120.13 | 103.31 / 116.69 | 106.18 / 106.79 | 102.39 / 115.81 |
N≤256 时完全消元在这组计量中最快；N=512 时多种表示接近。每格只有 9 个计量样本，P95 就是最大值，不能据校准中 B64 的尾部优势宣布稳定交叉点。校准全部 180 次调用（含预热）均 optimal，原始等式/盒界最坏残差 4.03e−13，跨表示最大目标差 5.54e−12，x/u 差 2.65e−7。
为避免只报告校准中有利排序，固定 N=512/B∈{16,64,512}，更换独立 seed=20260921，另作 5 次预热＋24 次计量。未用留出结果继续调参，旧结果不覆盖。
| B | 变量 / 等式 | Hessian 下三角非零数 | 总时间 P50 / P95 | 原控制空间 KKT 诊断最大值 |
|---|---|---|---|---|
| 16 | 543 / 31 | 4,879 | 118.78 / 168.96 ms | 2.29e−7 |
| 64 | 519 / 7 | 17,095 | 127.56 / 170.55 ms | 6.76e−7 |
| 512 | 512 / 0 | 131,328 | 129.86 / 170.35 ms | 2.92e−8 |
全消元的 native 求解 P50 为 111.37 ms，比 B64 的 125.36 ms 少，但其装配/装载 P50 为 2.40/12.61 ms，高于 B64 的 0.41/1.71 ms，抵消了数值求解收益。各分项中位数的和不等于合计中位数，不能用舍入分项重造总数。
全部 87 次调用（含预热）optimal，原约束最大残差 4.12e−13；B16/B64 对全消元最大目标差分别 1.50e−13/1.96e−13，原 x/u 差分别 1.111e−7/9.587e−8。各模型沿用 HiGHS 默认 qp_regularization_value=1e−7；其扰动依赖坐标表示，故不能仅凭相同 options 宣称精度完全相同。表中 KKT 诊断在原 u 空间计算梯度与盒界符号条件，活跃界识别阈值为 1e−7；它是数值诊断而不是精确最优证书。
由数据能确定的平衡：完全消元仅比 B64 少 7 个变量，却需要约 7.68 倍 Hessian 系数存储；留出中二者总耗时和尾延迟接近。B16 的存储约为全消元的 1/26.92，留出中位更低；校准与留出的速度排序变化，不能冻结“所有问题最佳 B”。这里测的是显式 Hessian 非零量，不是求解器峰值 RSS，后者尚未测量。
因此本研究选择按关系块保留少量连接变量，允许小块与完全消元两种有限表示，结合原空间误差和总成本选择。任务很小时可直接全消元；连锁依赖增长时不强制追求最小变量数。块宽不是交给用户或 AI 手调的建模参数。该链是表示取舍的数学实验，不是大型 CAD 装配的性能数据；不把它换算成产品吞吐。完整源码见附录 D。
14. 经验主张的证伪方法
Section titled “14. 经验主张的证伪方法”本节规定主张经验收益时需要什么证据，不是当前新增试用任务；架构裁决以 §18 与 §22 的推导为依据，不以遍历产品或不断扩样作为开工前置。
本节定义比较方法，不声称实验已执行。所有产品行为验证继续使用现有 capability explorer 和原生 Interface，不创建第二建模执行器或 test/spec 框架。
14.1 需求分布与对照
Section titled “14.1 需求分布与对照”冻结语法、误差、环境和预算后，参数化任务包括孔数 2–16、行数上限 4、板宽 14–120 mm、板高 14–80 mm、孔径 2–10 mm、净距 0.5–6 mm、边距 1–8 mm，区分可行、可靠无解、近边界和未知。该范围是研究分布定义，不是产品已支持能力。
对照使用相同原生工具契约、候选语法、必要条件预处理、数值容差与总预算：
- B：结构与参数求解，已有成熟求解器的正常预处理。
- B-cache：B 加普通缓存、basis/解热启动。
- C-fixed：B-cache 加同结构的参数化证书复用。
- C-transport：C-fixed 加经过核验的角色映射与跨结构证书搬运；使用独立结构留出区分已有对偶复用与所提贡献。
- D：C-transport 加受契约限制的领域抽象；候选域按展开后程序与其余组保持相同。
另在同一求解策略下对照全量重算与语义分隔符局部修复，包含新增对象改变查询全集、分隔符必须扩大的编辑链。这隔离 §10.2 的收益，避免把普通缓存收益归给新的局部机制。
不能让 B 重复尝试已知公式否定的单排、再把 C 的相同公式缓存叫学习突破。LLM 重试基线只有在模型版本、token、工具及预算固定且获授权调用时单独测量；当前没有该结果。
14.2 必须包含的反例
Section titled “14.2 必须包含的反例”变更孔径后旧根号界失效；删除证书支持的一条要求；从单行改错排；同名不同角色；面分裂或合并；新增对象改变碰撞查询全集；IPOPT 成功但几何检查失败；内近似无解但外近似可行；MILP 因整数性不可行但松弛可行；模型在求解时被另一编辑修改；取消和超时；撤销/重做及重开文档。
连续编辑链作为一个样本执行，中途不恢复空模型。现有 explorer 每样本恢复空模型的机制应作用在整条链之间，避免把“持续意图”测成若干独立建模。
14.3 指标和判定
Section titled “14.3 指标和判定”报告可行交付率、已证无解数、unknown、错误接受/错误排除发现数、真实几何调用数、求解/编译/核验/提交的分项时间、完整任务 P50/P95、冷启动和峰值内存。证书生成、匹配、核验和库学习成本都计入，不能只展示缓存命中后的毫秒数。
先冻结探索与独立留出样本；看过并用于修复的留出样本不再视为独立。有限实验发现零错误不能证明全域零错误。
当前独立 STEP 回读侧重实体有效性、体积、包络，不能替代孔中心/直径/净距等关系检查；新增关系必须有相应的实际几何判据。
这里的“独立”指另一个进程和锁定构件回读：现有探索器使用 OCP 7.8.1.1，仍属于 OCCT 系，不是另一种几何算法的交叉认证。当前探索器
14.4 首要验收：AI 能否发现、理解并正确使用
Section titled “14.4 首要验收：AI 能否发现、理解并正确使用”在相同模型、初始设计信息、接受域、精度和可比交付预算下，比较 §17 的核心表示、能力组合与编辑方案，接口说明质量单独控制。AI 不预装 Aira 专用技能、不读取实现源码；通过候选系统的原生发现入口取得所需契约。分别记录：
| 要验证的能力 | 可观察结果 |
|---|---|
| 首次发现 | 在预算内找到适用能力，或正确识别当前不支持；记录无关能力尝试与需要读取的契约量 |
| 语义理解 | 首次有效调用比例，以及单位、引用、前提和修改范围错误；用参数变化后的实际行为核验理解，不能只看文字复述 |
| 组合与迁移 | 用同一组概念完成未展示过的关系组合和连续修改，实际要求通过且锁定项保持；不以记住一个固定模板代替 |
| 诊断与恢复 | 根据原生诊断定位冲突、做出合法修复并重新验证；记录修复轮次、错误放宽要求与人工介入 |
同时记录 AI 必须补出的施工决策、临时参数和引用数量、输入输出 token、工具往返、完整任务成功率及正确拒绝率。失败、超时、能力不足和缺失证据保留在统计中。真实设计偏好不算多余负担；为了绕过接口缺口而补写施工代码则必须计入。发现与理解是首要产品验收，几何正确性、能力范围和 §2.3 的总成本共同约束方案选择。
同时记录内核内部搜索、候选几何构造、检查和计算成本，防止只将复杂度隐藏到更昂贵且低成功率的后台。一次调用也可能包含几百行施工代码，因此调用次数不得单独作为“简单”的证据。对超出自动语法而需要人工提供实现的样本单列，不混入意图求解成功率。
§17.9 已执行四种封闭契约的 AI 首答试用；尚未执行本节定义的完整产品发现、连续编辑与同预算对照。这些实验不能证明显著的 AI 成功率或总成本改善，也不否定 §18/§22 已完成的架构职责裁决。本节不授权新增付费调用。
附录 A：本地证据定位
Section titled “附录 A：本地证据定位”本文使用现有 Graphify 图谱（23,008 节点）定位，再用当前文件核验；未初始化或更新图谱。主要原始文件：
- CasADi/IPOPT 身份
- 当前数值求解
- 当前加载器
- 运行时发布
- OCCT 锁定构建
- AMIR 当前 schema
- 原生工具执行
- 实际要求检查
- 已有复用审计
- 草图历史对照：其日期和临时状态不能当当前生产状态。
- 现有原生能力探索
上游实现证据：
- CasADi 3.8.0 HiGHS 接口
- CasADi 3.8.0 HiGHS runtime
- CasADi 整数支持声明
- HiGHS 1.13.1 源码
- HiGHS 官方 IIS 范围：当前文档明确 IIS 仅 LP，不能混同整数证明。
- Stitch 锁定研究源码