工业目标域、逐构造翻译与系统覆盖证明
研究总览 · 2026-09-20
本文把架构 §22.9留下的工业覆盖义务落实为明确条件与翻译证明。结论是：五类系统中满足下述共同语义条件的有限数字工程模型，可以由同一核心完整编码、组合和修改。 覆盖对象包括结构、行为、离散场和跨域要求，不止外形；产品名称本身不证明模型满足这些条件。
这是研究证明与待实现语义规约。本轮未修改产品、安装后端、运行仿真或验证任何整机。原定理 A 的参照域 P 不被追溯扩大；本文明确给出扩展域 Pᴵ、降低规则和独立证明。当前生产契约、关系 AST与Modelica 生成子集分别标明其实际范围。
1. 独立目标域：有限数字工程描述 I
Section titled “1. 独立目标域：有限数字工程描述 I”目标域先按工程信息定义，不查询 Aira 是否已有对应 API。固定一个模型选择 μ，声明所研究系统的对象边界、环境、工况、空间/时间分辨率、允许编辑和验收意义；令 Iμ 为下面规则形成的所有有限、类型正确描述。μ 不能把未知物性、遗漏子系统或未定义要求静默解释为零。
一个描述是 d=(O,G,Q,C,B,F,A,R,E)，各项共享稳定身份：
| 记号 | 独立工程含义 | 信息完整的最低条件 |
|---|---|---|
| O | 零件定义、实例、装配、配置及物料/工艺对象 | 定义与实例不同；共享、父子、版本和配置选择显式 |
| G | 几何、拓扑、坐标和几何引用 | 数值类型、参数域、裁剪、邻接、方向及容差保留 |
| Q | 尺寸、材料量、状态量、离散选择和范围 | 值/未知量/派生量、单位、参考坐标及有效域不同 |
| C | 信号、物理、几何和资源连接 | 连接规律、方向、端口类型和跨部件约束显式 |
| B | 状态、事件、控制和流程 | 初始状态、守卫、更新、并发/优先级、队列和时钟显式 |
| F | 所选有限离散场模型 | 网格/基、自由度、方程、材料、载荷、边界和观测算子齐全 |
| A | 分析求值与外部模型的确定执行协议 | 算法/产物身份、输入、状态、调度、输出和失败语义可解析 |
| R | 工程要求、目标、证据和适用工况 | 受检量、量词范围、比较规则、误差及验收责任明确 |
| E | 允许的参数/结构编辑与保持条件 | 可写对象、共享实例影响、必须保持项和引用失效策略明确 |
“完整”指 d 声明的全系统模型，不是现实世界的全部知识。若系统边界内某个要求依赖的载荷、材料规律或交互没有模型，该 d 是输入不完整；不能靠换一种序列化宣布覆盖。任意中文“安全”“可制造”尚未被形式化时，仅为待澄清要求，不能作为已执行谓词。
采用有限有理数、明确格式的浮点数、Bool、有界整数、有限枚举、定长数组、记录和稳定引用。实数未知量可以有连续域；“有限”约束描述长度及离散结构，不把连续设计变量偷换成有限枚举。几何仍允许 P 中的曲线、曲面、B-Rep 与构造程序。
标量表达式基底为常量、引用、+ − × ÷ sqrt sin cos exp log、比较、布尔和惰性条件；循环、有限和、有限数组查询由有界构造展开。每种数值模式固定定义域、舍入和错误规则；精确代数意义与数值求值分开。物性表给出节点、单位、区间选择、插值公式和越界规则，不能只有材料名字。
有限精度求值按固定数值模式定义；表达式的精确实数意义可以保留，但本文不声称任意含超越函数的精确相等或定义域检查都可判定。无法核验的要求保留 unknown，不通过“表达式有限”偷换成“精确检查必然终止”。
高阶导数可引入辅助状态；连续模型的离散化方法及其参数属于 μ。未给离散化的 PDE 可作为连续模型要求保存，但不属于本文离散场的可求值子域。有限随机实验以分布、具体随机算法/流及运行输入表示；本文不据有限样本证明总体可靠度。
1.1 五类目标域的确切定义
Section titled “1.1 五类目标域的确切定义”令 T产线(μ)、T机器人(μ)、T航空(μ)、T潜航(μ)、T运载(μ) 分别是 Iμ 中具有下列完整对象边界的模型族。这是对本定理适用族的定义，不是“所有现实工业模型均属于 Iμ”的证明。系统数量、实例数和连接形状不固定；有限规模上限属于实际运行预算，不属于产品模板。
| 目标域 | 必须显式承接的系统层语义 |
|---|---|
| T产线 | 设备/工装/输送/工序、物料流、占用和等待、控制及公用工程；关联几何与产能/质量要求 |
| T机器人 | 结构/关节/执行器/传感器/控制/环境、运动与接触模型、能量和热；关联任务与可达性要求 |
| T航空 | 外形/结构/系统安装、材料与制造定义、气动/结构/热/机电模型、控制及工况之间的耦合 |
| T潜航 | 壳体/舱室/设备/管路/机电、浮力/外压/流体/热模型、控制及工况之间的耦合 |
| T运载 | 结构/设备/管线/机电、质量配置/载荷/热/流体与动态模型、阶段事件及接口之间的耦合 |
这里列的是语义类别，不是五个试做任务。每个族的模型必须说明不适用项及依据；例如无接触的模型要明确“接触不在所选工况中”，而不能缺少接触字段后被误判完整。本文不给出载具运行、制造或性能参数。
**边界解决方式：**以前“完整工程描述”没有操作性定义；现在其模型级含义由 O–E 及 μ 固定。输入可以逐项判定结构是否齐全，并定位缺少的语义类别。μ 对真实产品是否充分仍是工程建模判断，不伪装成语法检查能够发现全部遗漏。
一个具体工业描述能否使用该保证，由有限的覆盖判定决定：从 μ 声明的全部对象、接口、工况和要求出发，沿观测量→模型/方程→状态/参数→物性与边界来源追踪；每个叶项必须落入 §2–§3 的明确构造或有完整协议的具体外部模型，所有跨域边都必须有单位、坐标和连接律。循环可按强连通分量保留为联立关系，不要求物理系统无环。遍历对已有有限描述终止；类型、引用和构造匹配可判定，需数学证明的域条件则保留独立义务。
覆盖判定返回已承接源路径与未承接源路径，不把未知子系统排除后仍报告全模型覆盖。它决定“这份完整输入是否可被核心无损承接”，不决定“输入是否遗漏现实需求”。因此获得的是可应用于任意规模描述的充分条件与编译算法，无须遍历产品型号，也没有用子集定义冒充行业穷尽证明。
2. 共同构造基底与确定语义
Section titled “2. 共同构造基底与确定语义”2.1 几何、对象与工程量
Section titled “2.1 几何、对象与工程量”O 是有限有类型引用图；装配包含关系不得无限递归，连接图可有闭环。定义身份和 occurrence 路径分别编码，配置是对已有选择域的显式赋值。G 保存曲线/曲面控制数据、拓扑关联及已指定构造，工程引用指向角色与来源，失效/歧义是结果，不猜新面索引。
几何底座已有独立参照：OCCT 8.0.1 BRep 格式规定几何、拓扑、位置与方向等记录及其读写结构。本文采用其中已说明的资料与构造域，不把“能读 BRep”升级为任意输入都是有效实体。
Q 的绝对温度与温差、角度与无量纲比值、惯量参考点与轴分别有类型。单位变换是显式表达式；坐标变换为带方向约定的刚体映射。关系、物性表和要求读取同一源量，不能建立“用于分析的另一份质量”。
2.2 连接不是一种相等
Section titled “2.2 连接不是一种相等”每条连接先实例化两端类型，再采用以下规则；未声明连接律不属于可翻译输入：
| 连接类别 | 有限展开规则 |
|---|---|
| 信号 | 同型输入取其唯一生产者输出；延迟、采样与保持由 B 明确，代数环保留为联立关系 |
| 势/流 | 同一连接集的势量相等，按端口方向对流量求和为零 |
| 机械 frame | 用各自坐标变换表达位置/姿态关系和力/力矩平衡；关节自由度由关节方程决定 |
| 资源/物料 | 由事件对容量、数量、队列和所有权作原子更新；物料守恒是要求或定义关系 |
| 网格/场接口 | 保留索引映射、插值/投影与守恒关系；不默认两个网格同索引就是同一点 |
势/流的展开来自 Modelica 3.6 §9.2。流体 stream、过约束 frame 等必须采用相应已展开方程或既定组件语义，不能用普通势/流规则替代。本文的 C 可以保存显式方程，因此不以当前组件白名单限制表达域。
机械连接的基础式也可具体给出：R 将部件坐标映到世界坐标，Q 将端口坐标映到部件坐标，r 是部件坐标中的端口位置；世界位置为 p+Rr、世界姿态为 RQ，刚性重合要求两端这两项相等。令 f、τ 均在端口坐标中表达，且 τ 是关于该端口原点的力矩，则世界力为 RQf，关于同一世界点 o 的力矩为 RQτ+(p+Rr−o)×RQf；分别求和为零。若源数据已用部件坐标表达，先显式完成 Q 变换，不能重复旋转。转动/移动关节改用其允许自由度的明确关系，不能照搬刚性锁定式。
跨网格标量传递 vB=T vA 保存 T、两侧自由度与单位；若承诺离散积分守恒，须核验 1ᵀWB T=1ᵀWA，WA/WB 为相应积分权。若不成立，只获得所给插值语义，不获得守恒保证；向量/张量另保留坐标变换。共享未知量仍合并求解，不能把一次传递冒充已经收敛的耦合。
2.3 事件、流程与并发
Section titled “2.3 事件、流程与并发”离散状态为有限记录 s，转移为 (触发条件, 守卫, 读集合, 写集合, 更新, 优先关系)。一次逻辑步读取 s 的约定快照，选择合法转移，计算更新后原子写入；冲突转移如何排队、择一或同时生效属于源模型。更新中允许的顺序依赖用子步骤表示，不能自动改成并行赋值。
事件带 (物理时刻, 微步序号, 稳定事件键)；同一物理时刻可以有多个微步。运行预算限制微步数，达到上限是 unknown，不是正常稳态。异步输入序列、随机流及外部时钟是显式环境输入；相同输入条件下才比较执行迹。
容量为 c 的资源用整数占用 r 和显式拥有者表示：获取的守卫为 r+a≤c，成功更新 r'=r+a；释放须验证拥有者再减量。FIFO 队列为有限有序序列；并发请求保留源模型的仲裁。未知结构搜索不能擅自选择调度规则。
这里 c 为有限非负整数，申请量 a 为正整数，且保持 0≤r≤c。队列容量也必须显式有界，可降低为固定容量数组、有效长度与头尾索引；满队列的阻塞/拒绝策略由源事件定义，不丢弃任务。其读取、搬移或环形索引操作均落到有界分支/重复，因此没有暗中增加无界容器原子。
这已给出等待、拥堵、互斥、并发与控制的计算语义，而非“流程”文本槽。W3C SCXML 的转移选择规则提供成熟状态机语义依据；其附录 D 是说明性解释算法。这里定义有界工程子域，不宣称兼容完整 SCXML 或引入其运行时。
2.4 离散场不是一组无含义数组
Section titled “2.4 离散场不是一组无含义数组”一个场模型写成 F=(K,χ,Dof,M,Rh,Init,BC,Load,Obs)：K 为有限单元/关联图，χ 为坐标映射，Dof 为自由度及位置/单位，M 为材料与本构表达式，Rh 为残差，余项分别为初值、边界、载荷及观测。
每个残差具有有限展开：
[ R_a(u,\dot u,z,t;\theta)= \sum_{e\in S_a} r_{a,e}(u_{I_e},\dot u_{I_e},z_{I_e},t;\theta_e)-f_a=0. ]
S_a/I_e 是确定有限索引表；每个 r 是上述标量表达式或绑定具体执行模型的已声明调用。边界自由度、固定/开放量及约束单独保存，不能在装配矩阵时遗失。对有限时间网格，给定离散格式后可进一步形成 Rh(u₀,…,uN)=0。
有限元/有限体积的输入若采用有限基、积分点与权重，乘加装配就是有限表达式：局部自由度重命名、局部贡献求和、边界代入均有确定规则。对非多项式本构，只覆盖这里有执行定义的函数或物性表。此处规定语义降低，不要求产品自研矩阵装配、求积或线性求解库。
CGNS SIDS 网格约定把单元类型、节点连接和编号作为明确数据；场方程与材料模型章节区分方程类别、模型和有单位参数。它们支持上述信息类别的独立性，不证明 CGNS 文件自带可执行求解器，也不要求 Aira 引入 CGNS 依赖。
覆盖保证针对所给 Rh 及离散观测。离散化相对于连续场的误差、真实材料适用性和网格质量由 μ 与验证证据承担；不能把代数残差小等同于真实结构、流体或热行为正确。
2.5 有状态外部模型的具体接口
Section titled “2.5 有状态外部模型的具体接口”I 的纯表达式子域不需要外部黑盒。确需外部模型时，A 必须含实际内容寻址的模型产物、接口版本、平台/执行环境、输入输出与单位、初始化、状态机、调度、错误和状态保存能力；只有名称、URL 或未来后端计划的输入不属于该可执行子域。
例如已给定 FMI 3.0.2 Co-Simulation 产物时，绑定 XML 的变量/值引用与能力标记，按合法状态顺序实例化、初始化、设置输入、fmi3DoStep、读取输出并释放。检查返回状态、lastSuccessfulTime 和事件/提前返回；不将请求步长当成实际前进量。
其依据是 FMI 3.0.2 的状态机与 Co-Simulation 语义。FMI 不指定整体协同算法，故时间推进、输入保持/插值、事件交换与循环耦合策略仍须在 A 显式给出。模型不支持回滚时，不能编造回滚能力；可丢弃候选实例，历史使用封存输出而不重选设计。
这一规则保留同一具体模型的协议与有限调用迹，不证明模型内部物理正确。当前 Aira 没有在本轮接入或验证 FMI importer；此处不是把 FMI 加入当前产品依赖，也不以“有标准”宣称运行已完成。
3. 从 I 到 Pᴵ，再落到同一 AMIR 的逐构造翻译
Section titled “3. 从 I 到 Pᴵ，再落到同一 AMIR 的逐构造翻译”Pᴵ 在 P 之外显式增加有类型的工程记录、有限索引结构、离散场定义和上述事件/执行协议。它们有 §2 的解释规则；没有 anything、任意 metadata 或宿主 eval。旧 P 原子的含义不变，故这是研究语言的保守扩展，不是维护两套生产版本。
令 Cᴵ 首先用无碰撞编码 (源命名空间, 定义 ID, 实例路径, 局部键) 分配图节点，再逐条执行下表。递归检查所有必需字段和引用，未知构造返回 unsupported 及源路径；不能忽略后成功。
| 独立源构造 | Cᴵ 生成的确定内容 | 到 P/当前 AMIR 规约的对应 |
|---|---|---|
| 定义、实例、配置 | 独立定义与 occurrence 节点，共享引用和配置赋值 | P 的定义/实例；现有 ProductStructure 的相应语义 |
| 带单位量/范围 | 类型、规范值/表达式、源单位及固定/开放角色 | 关系 AST 的 Variable/Expr；新结构类型须统一注册 |
| 有限数组/记录 | 有键成员及形状；访问生成固定引用或带界选择 | 每个叶量降为 P 命名值；逻辑上可标量化，工程上共享存储 |
| 几何/拓扑/构造 | 原控制资料与关联；同 op、参数和失败语义 | P 构造节点；同一 geometry-kernel，不新增 builder |
| 材料/工艺数据 | 值表、单位、适用域与插值/步骤定义 | 表查询降为条件与表达式；工艺步骤进入 B，要求进入 assertions |
| 静态关系与目标 | 完整表达式、域、源要求引用、目标及来源 | design.relationSystem → 现有关系 AST/SolveIR 规约 |
| 端口连接 | 按 §2.2 产生关系、变量映射和方向 | 已支持组件使用 AnalysisDefinition；其他显式式子先类型化 |
| 状态/事件/资源 | 状态量、守卫、仲裁、微步和原子更新 | P 状态转换；Modelica 规约仅接其精确支持子集 |
| 网格与自由度 | K/χ/Dof 及几何关联，稳定局部索引 | Pᴵ 有类型结构；不能误称当前 AMIR 已有完整场结构 |
| 离散场残差 | 按 S_a/I_e 复制局部引用，有限求和生成 Rh |
静态标量子式可进关系 AST；动态方程用专用分析语义 |
| 显式离散时间格式 | 保留 t₀…tN、格式、全部历史状态与边界条件 | 形成有限关系族或已声明前向递推，不改成静态快照 |
| 跨域耦合 | 坐标/单位变换、插值/守恒式及共同未知量 | 联合关系块；动态耦合由 A 保留所选执行协议 |
| 确定外部模型 | 实际产物闭包、端口映射、状态机与调度 | Pᴵ 绑定具体接口；当前 Modelica/FMI 接线范围分开记录 |
| 要求/编辑/证据 | 原 assertion、观测对象、工况、可写域和保持项 | 同一 AMIR 源语义；运行见证进入 Realization，不反写要求 |
有限索引读取 v[i] 在 i 已知时连到对应分量；i 是有限选择时生成完整分支和域检查。有限和按源顺序展开，不擅自重排浮点加法。记录类型及成员语义保留，不能把所有内容编码成一个无法查询的字符串后称 AI 可操作。
场残差的例子是任意有限稀疏系统 Σj∈Ia Kaj uj=fa，不是一个尺寸样本。每个非零项生成 mul，按源次序 fold-add，再生成等式；边界 ub=gb 作为固定定义或完整保留的关系。反向读取各 a 的系数/索引和来源即可还原原系统，不需要猜矩阵含义。
动态离散式如 M(uk+1−uk)/Δtk+K uk+1=fk+1 使用同一规则，保留 Δtk>0、初始/边界与原目标。该翻译保留离散模型，不据此断言连续 PDE 误差有界、M 可逆或时间步稳定。非线性残差按原表达式保留，不因求解器偏好而线性化。
要求中的有限空间/时间量词也可展开：对声明索引集 J 的 ∀j∈J Pj 生成合取，对 ∃j∈J Pj 生成析取。连续时间的“始终”保留为连续量词及其检查义务，不能降低为有限采样后仍标等价。
**AMIR 接线的确定边界：**关系与 Modelica 两篇只规定静态标量/构造，以及有限刚体、被动关节、热网络、方程事件子集。Pᴵ 的网格、一般资源队列和模型执行协议仍需同一权威类型系统接纳；本证明给出了目标表示和算法，不声称当前 schema 已支持。实现时演进现有契约，不长期复制本文结构为另一份执行权威。
4. 有限规则的覆盖、组合与编辑证明
Section titled “4. 有限规则的覆盖、组合与编辑证明”定义 Obsμ 包含被声明可观察的工程量、拓扑、定义/实例身份、端口、状态和事件次序、场自由度、要求与诊断。格式、内存句柄和生成节点编号不作为工程观察；有意义的工艺顺序和引用身份不能从 Obsμ 中删除。
4.1 信息保持定理
Section titled “4.1 信息保持定理”定理 I。 对任意 d∈Iμ，Cᴵ 在有限时间产生类型化图；存在可计算读取器 D，使 D(Cᴵ(d))=d，其中等号允许无意义的序列化顺序及内部命名归一化，不允许丢失工程字段。
构造 D：按保存的源键读取 O–E；逐个恢复记录成员、数组形状、定义/实例引用和几何关联；表达式按 op 与输入边恢复；事件按源优先序恢复；场按 K/Dof 与残差来源恢复；要求只读取源 assertion。单位规范化保留源标签/变换，故可恢复源表示。D 不从结果 B-Rep、矩阵或轨迹逆推设计意图。
证明对有限语法作结构归纳。常量、身份与引用由注入编码保持；记录/数组由对子项的归纳假设恢复；表达式保持标签和有序输入；绑定/共享引用保持别名关系；分支、重复、连接、事件、场与要求均按 §3 对应规则恢复。没有未处理的构造种类，故结论覆盖所有有限合法组合，不需枚举产品。
类型检查与建图仅遍历有限描述并解析引用；紧凑循环的数字上界可以很大，故不宣称展开成本对其数字文本长度线性。若实际预算不足，翻译未完成必须报告 compile-budget，不能交付缺项模型。
4.2 关系与有限执行迹保持定理
Section titled “4.2 关系与有限执行迹保持定理”令 Sμ(d) 为 d 允许的状态/轨迹/见证集合。关系求解仍是查找其中元素，不是表达定理的前提。将环境输入、数值算法、随机流和调度以相同显式条件固定；预算按对应源操作计数，生成内部节点不额外消耗源逻辑步。两种实现墙钟超时可能不同，不属于以下执行等价的保证。
定理 II。 对 Cᴵ 的结构映射 ρ，有 ρ(Sμ(d))=Sμ(Cᴵ(d))；在共同已有的原子执行语义下，每个有限执行前缀具有相同 Obsμ 与正常/失败/未知分类。尚未绑定实际执行设施时，只获得关系/操作语义保持，不能标记已运行。
基础证明：纯表达式接收相同输入并按相同数值规则求值；惰性条件只求相同分支；离散场用相同有限索引与次序装配，故每一残差相同；转移选择读取对应状态、守卫与优先序，更新得到对应后态；几何与外部调用采用同一原子/具体产物和协议，故保留其返回和失败。
组合证明：将部件局部变量作注入重命名，保留共享端口后，整体关系为
[ S_{sys}={x:\exists z,\ \bigwedge_i R_i(x_i,z_i)\land\bigwedge_j K_j(x,z)}. ]
逐构造等价使每个 Ri、Kj 在变量映射下相同；重命名、合取和隐藏内部变量保持集合相等。对行为，则连接的是状态转换关系及明确调度，按微步数归纳得到有限迹对应；不是把所有轨迹压成一个静态方程。
跨模型误差、耦合收敛和真实物理正确性不来自该等价式。系统可能过约束、死锁或物理假设冲突；等价翻译必须保留这些事实。前向计算有定义不推出逆问题可解，存在合格见证也不推出预算内能找到。
4.3 编辑保持的具体桥梁
Section titled “4.3 编辑保持的具体桥梁”允许编辑 U 是对源对象/值/关系/连接/模型的有类型有限改写，带基准修订、可写域和保持要求。目标编辑 Uᴵ 通过同一源键定位对应节点，应用相同改写，失效全部依赖结果，重新类型检查；跨字段约束不满足或引用歧义则双方同样拒绝。
因此 Cᴵ(U(d,e)) ≅ Uᴵ(Cᴵ(d),e)；成功后用定理 II 比较结果，失败保留原 d 及其图。对有限合法编辑序列再归纳，组合与修改保持成立。证明依赖的是可逆源映射和对应改写，不是“最终形状相同”。
这个定理解决同一源模型在两种表示中的编辑对应。换算法、换物理模型或换构造属于语义替换，不能借用该式跳过观察与未来编辑等价核验；不将模型级翻译与任意重构混为一谈。
5. 五类系统的全系统语义矩阵
Section titled “5. 五类系统的全系统语义矩阵”下表按系统层信息检查覆盖，单元格给出具体共同构造；不把每类产品缩成一个外形，也不要求列举每个子系统型号。相同字母均指 §1–§3 的有类型、可展开内容。
| 工程语义 | 工业产线 | 机器人 | 航空系统 | 潜航系统 | 运载系统 |
|---|---|---|---|---|---|
| 产品/配置/几何 | O/G：设备与工装实例、布局 | O/G：连杆、关节、安装 | O/G：外形、结构、设备 | O/G：壳舱、结构、设备 | O/G：壳段、结构、设备 |
| 材料与制造定义 | Q/R：工件、加工量、公差 | Q/R：材料、配合、公差 | Q/R：材料/层合与制造要求 | Q/R：材料、连接、密封要求 | Q/R：材料、连接与制造要求 |
| 机械/运动 | C/B：输送、机构、执行动作 | C/B/F：运动学、动力学、接触模型 | C/B/F：机构、弹性与振动模型 | C/B/F：机构、压力结构模型 | C/B/F：机构、动态结构模型 |
| 流体/热/电与能量 | C/F：公用工程和设备场 | C/F：驱动、电、散热 | C/F：气动、热、机电与管网 | C/F：流体、热、机电与管网 | C/F：流体、热、机电与管网 |
| 控制/事件/阶段 | B：工序、互锁、故障模式 | B：控制模式、传感与执行 | B：控制模式与工况变化 | B：控制模式与工况变化 | B：阶段状态及接口事件 |
| 队列/资源/顺序 | B：容量、争用、物流顺序 | B：任务/资源与动作顺序 | B：所选制造/维护过程 | B：所选制造/维护过程 | B：所选制造/集成过程 |
| 工况/边界/初始值 | Q/F/A：负荷与环境输入 | Q/F/A：环境、载荷和初态 | Q/F/A：载荷和外部环境 | Q/F/A：载荷和外部环境 | Q/F/A：载荷和外部环境 |
| 跨子系统耦合 | C：节拍—占用—能耗 | C：机电—控制—热 | C：流体—结构—热—控制 | C：流体—结构—热—控制 | C：流体—结构—热—控制 |
| 验收与证据 | R：产能、质量与互锁条件 | R：任务、运动及负载条件 | R：所选整机模型要求 | R：所选整机模型要求 | R：所选整机模型要求 |
| 修改与恢复 | E：布局/工序变化与保持项 | E：机构/控制变化与保持项 | E：结构/系统变化与保持项 | E：结构/系统变化与保持项 | E：结构/系统变化与保持项 |
“接触”“气动”“密封”在该表不是原子能力名字：必须展开为声明模型中的 G/Q/C/B/F/R；无法展开的输入不算该单元格完成。制造步骤可以表达为有限过程和判据，但原材料、设备能力和公差判据是否足以支持真实制造仍由 μ 及外部证据承担。
按 §1.1 的定义，Tj(μ) ⊆ Iμ；真正得到证明的是 Cᴵ 在整个 Iμ 上的信息、关系与编辑保持，而不是这个定义性包含本身。对具体工业输入，须先执行 §1.1 的覆盖判定，再应用定理 I–II。上表定位各类系统的语义责任，不能代替该输入的覆盖结论；五类使用同一判定与证明，产品名不增加新的求解器或模型权威。
5.1 可表达、可执行、已验证分别计
Section titled “5.1 可表达、可执行、已验证分别计”| 状态 | 本文实际得到什么 | 当前产品不能由此继承什么 |
|---|---|---|
| E：可表达 | Iμ 全构造到 Pᴵ 的可计算翻译、回读、关系与编辑对应 | 当前 AMIR 接受全部 Pᴵ、自动完成自然语言建模 |
| X：可执行 | 纯标量/有限索引/离散转移有明确求值；绑定既定算法的几何/分析可保留其执行语义 | 任意 Rh 都有解、任意 DAE 都终止、任意外部模型已部署 |
| V：已验证 | 本轮核对下面官方语义来源，完成纸面规则与证明 | 五类整机实例已运行、数值/物理/制造合格、AI 自主成功率 |
五类的 E 结论相同；X 按其实际使用的数学片段与绑定来判定，不能按产品名一票通过；本轮没有新增五类产品的 V 结论。现有几何与关系求解的既有验证仍按原证据范围使用，不因本文出现新矩阵扩大统计口径。
可执行的已知机制是：明确输入的前向求值；LP/MILP/连续凸 QP 与适用 NLP 片段；具体几何原子；Modelica 规约列明的组件和方程事件子域。一般离散场残差的验算可按表达式执行，寻找场解须按数学结构绑定成熟算法；二者不混称“已支持场分析”。
6. 扩展、成本与完成裁决
Section titled “6. 扩展、成本与完成裁决”新增工程概念若可由本基底展开，只增加有类型定义及前提，沿用同一归纳证明。例如新增材料本构须给公式/表和有效域；新增流程对象须给状态、资源、事件和关系，不能靠名称获得能力。
真正新增原子时，必须给输入/输出类型、单位、域、确定语义、求值/检查方法、失败、依赖和编辑规则。先证明其叶节点保持，再沿既有组合规则传播；覆盖定理只扩展到这个新子域。成熟通用算法仍优先直接调用/补绑定/薄适配，本文的语义编码不是另造数值内核的理由。
已展开大小为 n 的图，建立节点/引用及回读只需与 n 成正比的遍历工作；排序、类型核验、几何、联立求解和证据成本另计。共享定义、稀疏残差与紧凑有界生成可避免无谓复制；隐式大规模展开不享有按文本长度线性的保证。
本文完成的研究环节是：给出独立于现有 AMIR 的共同信息域与具体输入覆盖判定 → 给出域内全部构造的目标表示与展开算法 → 证明信息回读、关系/有限迹及对应编辑保持 → 用全系统矩阵定位五类模型的职责。 这比只说“若部件能表达就能组合”多出了离散场、事件资源及跨模型接口的基础翻译；不声称矩阵已穷尽五个行业的全部知识。
因此，架构可以承接通过该覆盖判定的五类全系统模型，无需逐产品试做来决定核心架构。目标表示和已有 AMIR 之间需要的契约演进已经可具体定位；这是实施义务，不是要求重新等待一个覆盖所有工业知识的理论。
O–E 是编译器的完整语义责任，不是要求 AI 每次手写全部底层字段。已登记的设备、关节、材料或场模型定义可生成这些结构；AI 只提供真实设计选择与缺少的工程输入。不存在定义时必须发现为能力缺口，不能让一个有吸引力的组件名称替代方程和检查。
不能被上述数学替代的事实只有各自明确的责任：工程模型 μ 是否遗漏现实要求，材料/边界/离散化是否适用于目标工况，既定后端和 Aira 接线是否遵守本文语义，以及实际规模下的资源成本。这些必须由领域证据、源码和运行验证建立；不以其尚未完成为由撤回已证明的表达覆盖，也不把表达覆盖充当这些事实。
7. 来源范围
Section titled “7. 来源范围”本轮核对 OCCT 8.0.1 BRep、Modelica 3.6 连接语义、W3C SCXML、CGNS SIDS 和 FMI 3.0.2 官方文档；引用随相应定义给出。它们分别支撑现存几何、连接、状态、网格/方程资料及模型协议的具体机制。
Iμ 的共同工程分解、Pᴵ 翻译、信息保持与编辑证明是本文推导，不把外部格式能力直接归到 Aira，也不宣称这几份标准已经穷尽所有工业工程知识。链接页面仅作本轮语义依据；没有据此安装或新增任何产品依赖。
8. 工程交付是有损投影，不是另一份设计权威
Section titled “8. 工程交付是有损投影，不是另一份设计权威”设已验证修订为 r，封存实现为 R，工程交付格式的投影为 E。E(r,R) 必须消费同一有效状态，但通常不可逆：若两份工程只在设计关系、分析定义或历史上不同，其 STEP 几何仍可相同。因此不能从 STEP 几何回读相同推出工程完整保存。当前产品 STEP 收据除原有几何/层级/材料等保持范围外，必须明示行为模型、分析结果、修订历史和非活动配置不进入文件；完整可编辑状态由现有原生项目备份保存。此为 Aira 当前导出器的范围，不是对全部 STEP 标准表达能力的断言。
2026-09-21 源码核对：exportExactProductSTEP 消费已求值产品并复核 resultHash 与 B-Rep 哈希，导出前克隆 XCAF，结束后检查原形状未变；UI exportSTEP 捕获 revisionId 并在返回前检查 head 未变。SDK export-step 复用 model.read 的当前导出配置，收据原样投影到工具结果，模型消息去掉字节但保留收据。公开 Schema 与生产者现同时增加上述四类 omission，唯一当前收据要求完整九类；不保留省略披露的旧契约。没有修改几何导出算法，不重跑几何案例来验证文本字段。
8.1 BOM 的物性来源与分组保持义务
Section titled “8.1 BOM 的物性来源与分组保持义务”BOM 数量来自活动配置的定义/实例图。对每个叶定义 b，q_b 是实例数量，v_b 是当前实现的有效实体体积，rho_b 是材料密度，则 M=Σ q_b rho_b v_b，单位换算统一为 mm³→m³ 的 10⁻⁹。此式来自对离散实例质量求和，不依赖产品名称。显示舍入必须在求和之后；先舍入单件质量会使误差随实例数量放大。只有组内单位质量一致时，才能用第一件质量乘总数量；零件号相同本身不是几何或物性一致性证明。
接线前源码缺口（2026-09-21 定位）：assembly-bom.ts 使用 productBillOfMaterials 计算配置数量，但质量取自与程序字符串绑定的 cots.metadata.volumeMm3，自定义零件仍未知；按零件号/版本/材料分组时保存第一件单位质量，且先舍入再乘数量。SDK BOM 查询 includeEvaluation:false，UI 直接从 session.read 计算，都没有消费当前验证物性。不能将其目录估计宣称为已验证几何质量。
确定的接线应复用既有已求值 source/result 体积与材料来源，以修订/Realization/产品结果身份绑定；同一求值结果的 parts 已记录 body→nodeId/artifactId/exactBrepHash，可建立实际生产者连接。关系节点源 ID 与物化节点 ID 不同，禁止仅按源 authority 在节点结果中猜匹配。公共 model.read 投影物性，SDK 与 UI 消费同一数据与汇总函数；未知体积/材料保持 unknown，不用目录估计或零补齐。分组必须保留各定义数量和各自质量贡献；若公开单位量要求组内一致，则不一致须拆分或明确报告冲突，不能冒用首件。估计成本须另有模型身份与适用假设，不能从质量已知推出成本可靠。STEP 披露已落实；BOM 的后续实际接线状态见下段，不把这一实施规则本身当作完成证据。
2026-09-21 实际接线：buildProductAssembly 对活动叶子的原生 Solid 复用 measureNativeVolume，在该次求值按 artifactId 缓存，公开 parts 的体积/积分误差估计并纳入既有产品 resultHash。未用 metadata 体积补缺，也未扩充到壳、密度场或无有效体积的拓扑。BOM 接受同次 model.read 的源与 revision evaluation，核对 revisionId/modelHash；从已求值 parts 按 Body 取得物性，材料仍由活动源配置解析。源关系到物化节点的对应沿产品求值已有绑定，不猜源 nodeId。SDK 与 UI 共用 readAssemblyBom 和 computeAssemblyBom；UI 异步读取时拒绝 head 变化并清除过期显示，CSV 每行携带修订、模型/实现/产品结果身份和质量依据。
分组键增加实际 B-Rep 身份、材料及相同估价分类；同零件号但不同几何不再冒用首件质量。质量原始数值求和，不提前舍入，格式化只在显示端；整体数量及质量溢出拒绝。原生链验证不同几何同零件号分行、材料与尺寸编辑后质量更新、保存重开保持绑定且不启动 Worker。UI 共享调用与类型检查已确认，未把它写成 DOM 操作验收。多材料单体、壳质量及成本模型有效性未因此完成；成本仍为明确标记的启发式成本，不是供应商报价。
独立 Body 与守恒读取的推导：设计身份 b、源生成规则 n 与实际几何 a 是不同对象。对修订 r 的已求值 Body，读取必须沿该次求值绑定 B_r(b)=(n_actual,a,hash)；材料从源 Body 读取，几何从 a 读取。关系节点可能有多个输出，所以源 nodeId 不能充当 Body 或 artifact 的替代身份。这个结论由引用语义决定，不需要枚举飞机、机器人或零件种类。实现将 bodyProperties 纳入几何证据、公共投影和恢复核对，装配 Body 复用 parts，独立 Body 使用同一原生积分并按 artifact 缓存；缺失测量保持 unknown。材料与 Body 坐标系编辑的守恒基线按 Body 绑定解析实际节点和 artifact，检查生产者及 B-Rep 哈希，避免把关系源节点当作实际几何节点。
2026-09-21 定向验证：已有独立关系 Body 原生链中，材料赋值、尺寸修改后的 BOM 与保存重开一致，全程 Worker 启动为零；Web 类型检查和相关 lint 通过。此次只复核身份接线与对应物性，不新增场景枚举，不以该结果证明所有工业设计可解。该项验证结束。