AMIR 到 Modelica 的代码生成规约

研究总览 · 2026-09-20

本文补齐选型 §22.10的语法、类型和数据往返契约，目标为 OpenModelica 1.27.1、Modelica 3.6 与 MSL 4.1.0。分析声明、结构/量纲校验、参数精确检查、浮点参数复检与 .mo/.mos 生成已有基础实现；生成的集中热网络已在真实 1.27.1 后端编译、仿真并与分段解析解对照，具体版本内容、误差与范围见工作进度。这不代表下文全部生成子集已实测，产品任务、绑定、完整数值/轨迹准入仍未接通。实施清单仍由现有计划 P5维护。

1. 权威输入与生成边界

本地 Node 数值服务使用 /api/analysis/modelica，默认关闭。主机操作者通过 AIRA_LOCAL_MODELICA_PROFILE 指定 JSON 配置文件，字段为绝对路径 executable、workingRoot、files: [{path, sha256}] 及正整数 compileMilliseconds、runMilliseconds、maximumOutputBytes；前两项预算上限为 600000 ms，输出上限为 64 MiB。files 必须包含可执行文件且摘要为 sha256: 加 64 位小写十六进制。浏览器来源使用现有 AIRA_LOCAL_GATEWAY_ORIGIN，仅允许 loopback。GET 检查配置文件内容与运行版本，POST 仅传节点 ID 和交付定义；请求不能替换主机配置。浏览器传输响应上限为 128 MiB。此路由提供数值产物，不能授权项目提交；任务权限和 Session 准入属于上层原生接口。配置文件摘要仍不代表完整 MSL/toolchain 闭包。

分析声明属于同一 AMIR 修订，沿用 ModuleNode 外壳，以注册结构类型 AnalysisDefinition 承载声明。生成的 .mo/.mos 和轨迹是派生产物，不是第二份产品权威。当前 design.analysis@1.0.0 已进入唯一目录、Schema 与生成类型，Core 静态准入接受其源结构；共享几何编译器仍以 ANALYSIS_TASK_REQUIRED 明确拒绝缺少任务结果的候选。节点尚未完成原生任务与原子提交接线，不将目录注册等同于产品执行完成。

分析输入需要的几何由同一执行器的内部 prepareAnalysisGeometry 阶段生成，保留完整源模型身份并封存/重放几何实现。准备证据与 execution manifest 使用独立版本域，不能作为候选验证凭据；普通验证仍要求完成分析准入。此顺序解除“先要分析结果才能得到分析输入几何”的循环，未新增建模执行器。准备证据已接入节点参数交付并验证本地主机执行；原生任务授权、结果身份与原子提交仍须完成。

现有 ProductStructure有装配、配置、尺寸与图纸，但没有完整物理连接和行为声明。转换器必须读取显式分析声明＋已求值 occurrence/Realization 绑定。静态 mate、接触面、共同材料和装配父子关系均不能自动推出转动关节、热接触或流体连通。几何可提供体积、局部坐标等已声明计算的输入，材料和物理假设不能由外观猜测。

本规约的实际生成子集为：刚体、固定坐标变换、理想被动关节、集中热网络、代数／连续状态方程和有限离散事件。Fluid/Media、接触、柔性体及驱动组件需要各自具体的参数、端口、初始化规则才能进入同一目录；库支持它们不等于本转换器已经支持。用户 .mo 文件、任意类路径和宿主函数不在本生成接口内。

2. 有类型分析声明

Id/ExprId/Expr/ScalarAtom/Domain 及量纲规则引用共享关系 AST，不复制标量计算语言。ProductOccurrenceReference 导入当前生成类型，不重定义 occurrence 寻址。Expr.var 在此作用域引用 symbols；Expr.input 仍只读取模块的显式输入端口。分析仅增加 time/der/pre，不进入静态 SolveIR。下列所有表达式引用必须存在；未知字段拒绝。

type AnalysisExpr = Expr
  | { op: "time" }
  | { op: "der" | "pre"; arg: ExprId };
type Vec3 = [ExprId, ExprId, ExprId];
type InitialValue =
  | { kind: "fixed" | "guess"; value: ExprId }
  | { kind: "steady" };
type FrameTransform = { translation: Vec3; xAxis: Vec3; yAxis: Vec3 };
type AnalysisComponent =
  | { kind: "rigidBody"; mass: ExprId; centerOfMass: Vec3;
      inertia: { xx: ExprId; yy: ExprId; zz: ExprId;
        yx: ExprId; zx: ExprId; zy: ExprId } }
  | { kind: "fixedFrame"; transform: FrameTransform }
  | { kind: "revolute"; axis: Vec3;
      angle: InitialValue; angularVelocity: InitialValue }
  | { kind: "prismatic"; axis: Vec3;
      displacement: InitialValue; velocity: InitialValue }
  | { kind: "heatCapacity"; capacity: ExprId; temperature: InitialValue }
  | { kind: "thermalConductance"; conductance: ExprId }
  | { kind: "fixedTemperature"; temperature: ExprId }
  | { kind: "prescribedHeatFlow" };
type ComponentQuantity = "temperature" | "angle" | "angularVelocity"
  | "displacement" | "velocity" | "heatFlowInput";
type AnalysisSymbol = { type: Id; unit?: string } & (
  | { kind: "componentQuantity"; component: Id; quantity: ComponentQuantity }
  | { kind: "continuous"; initial: InitialValue }
  | { kind: "discrete"; domain: Domain }
  | { kind: "algebraic" }
);
type AnalysisPort = "frame_a" | "frame_b" | "port" | "port_a" | "port_b";
type Endpoint = { component: Id | "$world"; port: AnalysisPort };
type AnalysisDefinition = {
  expressions: Record<ExprId, AnalysisExpr>;
  symbols: Record<Id, AnalysisSymbol>;
  components: Record<Id, AnalysisComponent>;
  // 有机械组件时必须提供；其他模型不得生成无用 World。
  world?: { gravityMagnitude: ExprId; gravityDirection: Vec3 };
  bindings: Record<Id, { occurrence: ProductOccurrenceReference;
    frameRef?: Id }>;
  connections: Record<Id, { first: Endpoint; second: Endpoint }>;
  equations: Record<Id, { left: ExprId; right: ExprId }>;
  eventGroups: Record<Id, {
    writes: Id[]; initial: Record<Id, ExprId>;
    branches: { guard: ExprId; updates: Record<Id, ExprId> }[];
  }>;
  outputs: Record<Id, { expression: ExprId;
    occurrence?: ProductOccurrenceReference; requirementRefs: Id[] }>;
  conditions: { startTime: ExprId; stopTime: ExprId;
    intervalCount: number; integrationRelativeTolerance: string };
  budget: { compileMilliseconds: number; runMilliseconds: number;
    maximumOutputBytes: number };
};

bindings 的键是 component ID；它只声明物理模型与产品实例的关联，不赋予对几何的写权限。允许同一 occurrence 关联不同物理表示，例如刚体和集中热容，但不会由此自动添加耦合方程。frameRef 必须解析到该 occurrence 的显式稳定局部坐标；不得用临时面索引。$world 是保留端点，不是产品实例。

省略 frameRef 时采用该 occurrence 所引用零件定义的本地坐标系；不是世界坐标系，也不取当前任意选中的面。组件质量属性、端口与绑定坐标不一致时必须显式转换并记录来源，禁止默认按数字相同处理。

组件参数、world、工况、初始值和 domain 界只能依赖已知输入及常量；引用时间、待解符号或组件输出则拒绝。手写 continuous 只允许 Real 数量，discrete 允许 Bool/有界 Int/离散 Real，algebraic 的类型由已注册签名决定。Bool 域使用非空 finite 子集，Int 域为有限枚举或上下界俱全的整数区间；整数值及运算不得超出锁定后端整数表示范围。符号声明的类型必须与组件字段的目录类型一致，不能自填 type 绕过单位校验。

domain 原样保留，不夹紧越界的事件更新。初值核对全域，每次事件更新生成同域成员关系的 assert，并从完整离散输出事件记录独立复核；需要复核的符号自动生成检查专用输出别名并纳入 variableFilter，用户输出列表不能移除它。区间严格端点按声明打印，不加隐式 epsilon。数值证据不足、事件记录缺失或整数溢出可能无法排除时返回 unknown，不能宣称轨迹满足全部域。域约束用于验收状态，不自动重新选择另一条事件分支。

起止时间必须有限且 stopTime>startTime，intervalCount 是正的 JS safe integer；预算为正的 safe integer，积分相对容差满足 0<tolerance<1。推导输出间隔 (stopTime-startTime)/intervalCount 必须正且有限，交付后不得舍入为零。具体资源上界由锁定运行配置决定并写入运行身份，不通过增大输入值绕过主机限额。所有物理输入、初值和事件更新均进行同型检查。

der 只接连续 Real 符号或目录声明为连续状态的组件量；本子集只允许一阶导数。pre 只接 discrete 符号，不能把连续轨迹的任意历史值当作 pre。表达式引用图无环，方程可组成 DAE 环；不按表达式 DAG 的无环性声称 DAE 一定可解。

每个离散符号恰有一个事件组作为写入者，且不得另有普通方程写入。连续状态可通过方程隐式约束；不强行要求每个状态都写成显式 ODE。结构奇异、过约束和数值初始化失败保留不同诊断。

普通方程是无方向等式，不能把左边的变量自动解释为赋值目标。事件状态 d 与代数量 x 的 d=x 和 x=d 因而具有相同准入结果：允许由事件给定的 d 约束 x；是否可解仍由完整 DAE 编译与初始化判定。当前子集拒绝包含离散依赖、却不含任何连续/代数/组件未知量的额外普通方程（包括嵌套表达式和 pre 依赖），以免把独立离散约束冒充第二个事件驱动器；该拒绝表示未支持的约束位置，不是全局无解证明。校验沿已检查且有预算的表达式拓扑序传播离散依赖/非事件未知量两个标记，再对等式两侧对称合并，复杂度 O(表达式引用数+方程数)，不枚举离散状态。符号抵消、结构奇异和隐藏过约束不由这种依赖判据证明，后端检查仍不可省略。

3. 组件、端口和字段的确定映射

下表路径均以 Modelica. 开头；frame 连接由 MultiBody 库处理，heat 连接由 HeatTransfer 库处理。每个端点必须存在、同域且满足其连接基数规则。未连接物理端口在本子集中拒绝，绝热或固定支撑须明确表达；不利用库的隐式零流默认值补充设计。

Aira kind	MSL 4.1.0 类与生成参数	可连接端口／可引用量
rigidBody	Mechanics.MultiBody.Parts.Body(m,r_CM,I_11,I_22,I_33,I_21,I_31,I_32,animation=false)	frame_a:frame
fixedFrame	Mechanics.MultiBody.Parts.FixedRotation(r,rotationType=...TwoAxesVectors,n_x,n_y,animation=false)	frame_a/frame_b:frame
revolute	Mechanics.MultiBody.Joints.Revolute(n,useAxisFlange=false,animation=false)；初始化 phi/w	frame_a/frame_b:frame；angle→phi，angularVelocity→w
prismatic	Mechanics.MultiBody.Joints.Prismatic(n,useAxisFlange=false,animation=false)；初始化 s/v	frame_a/frame_b:frame；displacement→s，velocity→v
heatCapacity	Thermal.HeatTransfer.Components.HeatCapacitor(C)；初始化 T	port:heat；temperature→T
thermalConductance	Thermal.HeatTransfer.Components.ThermalConductor(G)	port_a/port_b:heat
fixedTemperature	Thermal.HeatTransfer.Sources.FixedTemperature(T)	port:heat
prescribedHeatFlow	Thermal.HeatTransfer.Sources.PrescribedHeatFlow(alpha=0)	port:heat；heatFlowInput→Q_flow，必须由且仅由一条驱动定义提供
$world	inner Mechanics.MultiBody.World world(g,n,gravityType=...UniformGravity,enableAnimation=false)	frame_b:frame

参数类别	目标单位与强制范围
mass / capacity / conductance	kg 且 m>0；J/K 且 C>0；W/K 且 G≥0
centerOfMass / translation / displacement	m，全部有限；不由符号正负推断物理限位
inertia	kg·m²，关于质心的对称矩阵；PSD，主惯量满足每一项不大于其他两项之和；退化惯量另检查关节有效惯量，不能仅凭 PSD 声称动力学可解
angle / angularVelocity / velocity	rad、rad/s、m/s，有限；固定姿态变换使用双轴向量
temperature / heatFlowInput	K 且 T≥0；W，有限；正热流输入表示向连接对象注热
axis / gravityDirection / gravityMagnitude	方向向量无量纲、有限且非零；g 为 m/s²、有限且 g≥0
xAxis / yAxis	无量纲单位正交向量，叉积确定右手第三轴；只接受数值规约所允许的误差

重复连接和端口自连拒绝；符号引用的组件 kind 与 quantity 必须命中上表。上述范围须在原单位验证交付值；矩阵与量纲检查无足够证据时不默认为有效。

未列出的 quantity／参数／端口不可通过字符串拼接透传。被动关节的 useAxisFlange=false 明确表示零外加驱动力／力矩，不代表已实现电机、控制或限位。任意闭环关节图也不保证可求解，不能遇到奇异闭环就擅自改成另一种关节。

依据：Body 参数、关节端口、热组件、热源。这些来源支持组件接口，本文的生成和拒绝策略是 Aira 的工程选择。

4. 单位、坐标与初始化

所有参数先按共享 QuantityType 规则转换到目标字段单位：长度 mm→m 乘 10⁻³，惯量 kg·mm²→kg·m² 乘 10⁻⁶，力矩 N·mm→N·m 乘 10⁻³。绝对摄氏温度转 K 加 273.15，温差不加偏移；integrationRelativeTolerance 不是温度或几何公差。

固定 frame 约定为 p_a=R_ab*p_b+r_ab，R 的列为 b 坐标轴在 a 中的坐标。translation→r，xAxis/yAxis→n_x/n_y。生成前检查轴的长度、正交及右手性；超出明确输入误差的矩阵不得让库静默正交化。使用双轴向量避免欧拉顺序歧义。锁定 FixedRotation 源码的 angle/angles 实际是度，而 Revolute.phi 是弧度；不能统一按 rad 原样传参。

Body 的 r_CM 以 frame_a 表示；惯量必须关于质心且轴平行 frame_a。若上游惯量关于其他原点，先应用平行轴定理转到质心；若轴不同，按声明旋转变换张量。保持非对角项真实符号，检查质量、有限性、对称性及物理惯量条件；未知参考原点／坐标返回缺失输入，不能直接复制六个数字。

机械模型恰有一个 inner World world。局部端口偏置生成 fixedFrame，明确关节连接其两端；当前装配位姿只为初值/一致性检查提供输入，不生成每个刚体永久固定到世界的方程。World 定义

fixed 初值生成 v(start=x0,fixed=true)；guess 生成 fixed=false；steady 仅允许 heatCapacity.T 或手写连续状态，生成 initial equation der(v)=0 且不再固定该状态值。关节的 steady 在本规约中拒绝，避免同时固定坐标、速度和加速度造成隐藏过约束。

**MSL4.1.0 HeatCapacitor 的说明仍提 steadyStateStart，但实际源码没有该参数。**生成器必须采用上述初始化方程，不能输出不存在的 modifier。锁定源码

离散记录独立验收的实施边界

事件生成中的 assert 与返回制品的独立检查承担不同义务。对于交付后的离散域 D 和每条解码记录 x，必须检查 x∈D；有限域建立成员集合，区间按原始严格/非严格端点比较，Count 另检查非负。每个离散符号恰有一个 domain-check 列，缺失、重复或未知符号不能忽略。域常量须为已交付的规范单位字面量，回读器不另建表达式求解器，也不按 epsilon 吸附域外值。

当前 checkAnalysisArtifacts 在 CSV 类型和时间检查后调用同一域校验，因而本地主机、浏览器接收及制品重验消费同一规则。复杂度为域成员总数加记录中离散单元数；有限集合查找不遍历所有设计或状态组合，记录沿用既有行/单元预算与取消检查。结论仅是解码记录满足交付域，不证明事件记录完整、采样间行为或原精确域与浮点交付域相同；这些仍由各自交付与工程证据承担。

2026-09-20 实际 OpenModelica 运行已核对初值 0、时间触发后值 1 的 Count 事件与自动检查列，共 14 条记录；把同一结果末条状态改为域外值 2 后，共享检查器返回 ANALYSIS_TRAJECTORY_DOMAIN。该接线检查到此停止，不推广为全部事件语义或工业有效性通过。

5. 方程、事件与源映射

数值结果的原生读取使用既有 model.read 的 analysis 查询（nodeId、outputId、offset、limit），SDK 同源投影为 currentModel.analysisRecords。单次读取一个声明输出的至多 100 条记录，默认 20；分页按 rowOrdinal 而非 time，保留重复时刻。响应绑定 revisionId/contentHash，值标注规范单位和 number/boolean-01 编码，时间单位秒；跨页须固定修订。读取消费已重验的封存数值记录，不重新仿真、不输出私有主机日志、不将模型证明转成虚构轨迹。不存在的结果或输出明确拒绝；超出末页返回空 rows。记录观察不构成采样间或物理有效性保证。

组件与纯方程按稳定 ID 排序；事件分支保留声明次序。Modelica 标识符为命名空间前缀加稳定 ID 的完整 UTF-8 十六进制编码：组件 c_、自声明符号 v_、请求输出 y_、域检查输出 d_。因此组件与符号 ID 相同也不会重名；组件量别名直接映射到对应 c_ 实例字段，不重复声明变量。不直接使用用户名称或截断哈希。顶层固定 AiraGenerated，每次在独立目录编译。world 名保留。源 map 使用同一编码表，记录生成行列区间→源 node、JSON Pointer、组件/关系 ID、occurrence 和 requirement。

生成器逐节点打印共享表达式并补足括号，不接受源码片段。cmp.eq/le/lt/ge/gt 分别打印 ==/<=/</>=/>，方程左右侧之间才打印 =；数值 select 打印 if c then a else b。der/pre/time 仅在分析作用域打印。连接输出 connect(a.port,b.port)，让后端生成域对应的守恒与连接方程；不得自行把 frame 或 stream 类端口展开成全部字段成对相等。连接语义

每个事件组生成一个 when initial() then ... elsewhen g1 then ... elsewhen g2 then ... end when。initial 是离散初值的唯一权威，不再生成该符号的 start/fixed 初始化方程。writes 非空且无重复，initial 和每个分支的键必须恰等于 writes 集合，保持项显式 pre(v)；拒绝跨组重复写入和同分支重复赋值。guard 为 Bool，初值不依赖 time/der/pre/未初始化离散量。

同一时刻多个 guard 上升时，靠前的 elsewhen 优先。pre 遵守 Modelica 事件迭代语义，不是整个物理时刻永久冻结的全局快照。需要同步必须共享触发器或明确时钟；不把接近的时间按容差合并。不擅自加入滞回、延迟、优先级或取消事件。零时循环、抖振和事件迭代失败在预算下返回 unknown；语法／结构错误返回 invalid。when 与初始化语义

6. 完整生成文本示例

以下输入语义为一个显式绑定的刚体、被动转动关节、集中热容、向环境散热和声明的滞回温控。数值是示例工况，不是材料默认值；机械与热模型之间没有隐含摩擦发热。为便于审查，示例使用短实例名；生产输出执行 §5 编码。温控初温低于低阈值，初始加热=true；生成前要求 low<high 并检查初始化策略与边界一致。

within;
model AiraGenerated
  import SI = Modelica.Units.SI;
  inner Modelica.Mechanics.MultiBody.World world(
    enableAnimation=false,
    gravityType=Modelica.Mechanics.MultiBody.Types.GravityTypes.UniformGravity,
    g=9.81, n={0,-1,0});
  Modelica.Mechanics.MultiBody.Joints.Revolute joint(
    animation=false, useAxisFlange=false, n={0,0,1},
    phi(start=0.2, fixed=true), w(start=0, fixed=true));
  Modelica.Mechanics.MultiBody.Parts.Body body(
    animation=false, m=1, r_CM={0.5,0,0},
    I_11=0.001, I_22=0.084, I_33=0.084,
    I_21=0, I_31=0, I_32=0);
  Modelica.Thermal.HeatTransfer.Components.HeatCapacitor cap(
    C=500, T(start=293.15, fixed=true));
  Modelica.Thermal.HeatTransfer.Components.ThermalConductor loss(G=2);
  Modelica.Thermal.HeatTransfer.Sources.FixedTemperature ambient(T=293.15);
  Modelica.Thermal.HeatTransfer.Sources.PrescribedHeatFlow heater(alpha=0);
  parameter SI.Temperature low=308.15;
  parameter SI.Temperature high=313.15;
  parameter SI.HeatFlowRate power=100;
  Boolean heating;
  output SI.Temperature y_temperature;
  output SI.Angle y_angle;
  output Integer y_heating;
equation
  connect(world.frame_b, joint.frame_a);
  connect(joint.frame_b, body.frame_a);
  connect(cap.port, loss.port_a);
  connect(loss.port_b, ambient.port);
  connect(heater.port, cap.port);
  heater.Q_flow = if heating then power else 0;
  when initial() then
    heating = true;
  elsewhen cap.T >= high then
    heating = false;
  elsewhen cap.T <= low then
    heating = true;
  end when;
  y_temperature = cap.T;
  y_angle = joint.phi;
  y_heating = if heating then 1 else 0;
  annotation(uses(Modelica(version="4.1.0")));
end AiraGenerated;

输入中的 bindings.body 与 bindings.cap 可指向同一 occurrence；symbols 分别把 temperature 映射 cap.T、angle 映射 joint.phi、heatFlowInput 映射 heater.Q_flow，并声明 heating 为 Bool discrete，domain 为 false/true 的 finite 集合（布尔类型已确保成员关系，无需多余 assert）。六条连接逐项对应 connections；温控 eventGroups 的 writes 为 heating，initial 为 true，branches 依次为 temperature>=high → false、temperature<=low → true；每个标量由共享 Expr DAG 提供，没有任何 Modelica 文本输入。

7. 编译脚本与本机执行

以下脚本保存为任务私有目录的 compile.mos；同目录为 AiraGenerated.mo。脚本的所有值由通过校验的结构生成。示例时间、采样数量和积分容差来自 conditions，不能硬编码成所有任务的默认保证。

ok := setCommandLineOptions("--std=3.6");
if not ok then
  print(getErrorString());
  exit(9);
end if;
print("AIRA_COMPILER " + getVersion() + "\n");
ok := loadModel(Modelica, {"4.1.0"}, requireExactVersion=true);
if not ok then
  print(getErrorString());
  exit(10);
end if;
print("AIRA_MSL " + getVersion(Modelica) + "\n");
ok := loadFile("AiraGenerated.mo", requireExactVersion=true);
if not ok then
  print(getErrorString());
  exit(11);
end if;
print(checkModel(AiraGenerated) + "\n");
(nMessages, nErrors, nWarnings) := countMessages();
print(getErrorString());
if nErrors > 0 then
  exit(12);
end if;
built := buildModel(AiraGenerated,
  startTime=0, stopTime=300, numberOfIntervals=3000,
  tolerance=1e-6, method="dassl",
  fileNamePrefix="aira_analysis", outputFormat="csv",
  variableFilter="y_temperature|y_angle|y_heating");
(nMessages, nErrors, nWarnings) := countMessages();
print(getErrorString());
if nErrors > 0 or built[1] == "" or built[2] == "" then
  exit(13);
end if;
print("AIRA_EXECUTABLE " + built[1] + "\n");
print("AIRA_INITIALIZATION " + built[2] + "\n");

checkModel 返回 String，不是 Boolean。buildModel 返回 String[2]，宿主核验可执行产物和初始化文件实际存在、解析后的绝对路径属于当前工作目录，才允许运行。版本探测必须先确认锁定编译器身份，脚本中的版本输出再次记录实际加载身份；不能只按安装目录名称猜测版本。1.27 Scripting API

宿主在现有本地 Node 入口调用 spawn(verifiedOmcPath,["compile.mos"],{cwd,shell:false,windowsHide:true})；编译通过后以同样配置调用已核验的产物绝对路径，参数数组为 ["-r=result.csv","-outputFormat=csv"]。不通过 shell 拼接，不把后端返回的任意路径直接执行。工作目录名称由宿主生成，不采用用户标签。

只生成固定白名单的类和表达式；不透传 external、用户注解、库搜索路径、C flags 或脚本。Modelica 编译会生成并执行原生代码，非 shell 调用并不使任意用户源码安全。资源限制包括编译/运行墙钟和输出字节数；取消终止本次进程及其子进程，清理前确认路径仍在本次目录。日志与临时结果默认不进入 Git。

缓存绑定生成源码、编译器、MSL、生成器和 toolchain 身份及选项。仅当初始化 XML 中参数实际可覆盖且改变不会影响结构时允许 -overrideFile；无法证实则重新编译。运行结果还绑定完整数值工况。不设置 -noEventEmit 或 -noRootFinding；CSV 事件记录保留原始顺序。1.27 运行参数

8. 输出映射、成功条件和提交边界

type AnalysisOutputBinding = {
  column: string;
  occurrence?: ProductOccurrenceReference;
  requirementRefs: Id[]; type: Id; unit?: string;
} & (
  | { kind: "requested"; outputId: Id }
  | { kind: "domain-check"; symbolId: Id }
);
type AnalysisSourceBinding = {
  sourceModelHash: string; inputClosureHash: string; realizationHash: string;
} & (
  | { kind: "candidate"; candidateId: string }
  | { kind: "revision"; revisionId: string }
);
type AnalysisRunBinding = {
  source: AnalysisSourceBinding;
  configurationId?: string; analysisNode: Id;
  analysisDefinitionHash: string; conditionsHash: string;
  generatedSourceHash: string; backendIdentity: string;
  columns: AnalysisOutputBinding[];
};

候选分析绑定 candidateId、源模型、输入闭包与 realizationHash；不能伪造尚未产生的 revisionId。不可变结果内容哈希包括冻结输入身份、生成器/后端身份及轨迹载荷，不含候选/修订的外层挂载字段；修订通过结果内容哈希引用，提交成功后外层绑定最终 revisionId，避免结果哈希与修订哈希互相递归。失败或过期候选不挂到当前修订。

实现根也必须遵守这一无环条件：令 G = seal(R with witnesses.analyses = {})，分析结果内容 A 引用 G.realizationHash，最终实现 R 的 witnesses.analyses[nodeId] 引用 hash(A)，修订再引用 hash(R)。几何、源配置、编译器、资源和其他求解见证均保留在 G 中；仅分析引用被清空。因此新增结果不会改变自身输入身份，而任何几何输入依赖变化都会使旧结果失配。当前唯一 Schema 必须含 analyses 映射（无结果时为空），不接受缺字段旧根。bundle 保存原始 XML/CSV、读取结果与内容摘要，读取时核对完整引用闭包，重放时核对源节点确为 design.analysis；重建几何后再附加已核验引用。此处只证明内容依赖一致性，不证明工程要求满足，也不替代候选准入与 Session 原子提交。

当前内部 prepareAnalysisGraphDelivery 通过 resolveDesignAnalysisNode 从 AMIR 节点和当前配置读取定义与参数，核对作者声明的 occurrence 和要求引用，再复用图证据核验与 Core 源模型身份；不接受外部替换定义或参数。数值端口缺少求值结果时保留 awaiting-inputs，frameRef 未解析时拒绝交付。checkAnalysisGraphFreshness 独立比较内容与外层挂载，任一变化即过期。此 analysis-node-source 身份仅证明所检查快照的一致性，不证明节点已提交、实际位姿/物性来源已受检或调用者拥有 Session 权限。它不是包含生成器/后端/轨迹的最终结果身份；完整 AnalysisRunBinding 与原子持久化仍按本节规约实施。

上例列 y_temperature/y_angle/y_heating 分别映射原 temperature/angle/heating 输出 ID，单位为 K/rad/无量纲计数，且保留原 occurrence、工况与要求。源模型、配置或 Realization 变化使结果过期，不从轨迹反写另一套当前模型。

数字输出使用正确 CSV parser，不按逗号手工切割。检查列名、声明类型、有限性、记录数、时间非递减以及终点覆盖。保留 (time,rowOrdinal)，不得用 Map<time,row> 去重；没有独立事件 ID 时，不把每个重复时间行解释为一次独立物理事件。Bool 输出可生成明确的 0/1 别名并在映射中记录转换。

结果	判定
unsupported / invalid	不支持的组件、缺少物性、非法连接、单位错误、结构/初始化声明错误，附源 pointer
unknown	超时、取消、后端缺失、数值失败、事件不收敛、文件不完整；不等于物理不可行
numerical-complete	进程正常结束且无错误诊断、所需列完整有效、轨迹达到工况终点；仍不是设计要求通过
requirement pass/fail/unknown	按原要求及其证据策略检查轨迹，单独记录覆盖范围和误差依据

积分 tolerance 是后端数值设置，不是全局轨迹误差界，不能代替数值交付规约。采样与记录事件点的检查只证明被检查点；全时域限值需要额外包络或连续时间验证证据。初始化猜值被后端调整、变量被结构化消去、要求仅被部分观测时均保留诊断，不将“仿真成功”升级成整机工程有效性保证。

工程有效性规约给出上述证据的具体生成规则：带全域导数界的时间包络、残差到轨迹误差的传播、耦合收缩界以及被动热网络的不变区域。分析输出绑定同一要求、适用域、假设与证据；编译器能从已注册模型推出的界由核心生成，缺少物性或模型误差依据时不能让 AI 猜一个上界。

9. 从几何到行为输入的推导契约

本节规定 P5 的完整能力单位：同一候选内，从实际部件、材料和显式物理抽象生成行为模型输入，并随修改、封存、恢复保持来源。它不是新的独立执行器，也不是“增加一个惯量查询”即可结项。以下公式为连续质量分布的推导；代码现状及尚未接通部分在 §9.6 分开记录。

有限实例的组合实施契约见 §9.8。该契约扩展当前单体物性链，不改变单体 frameRef 的所有权，不将几何装配自动解释成动力学连接。

9.1 哪些信息可以消除，哪些必须保留

设实体占据区域 Ω，密度场为 ρ(x)，所选分析参考系为 F。质量分布确定后，质量、质心和惯量是函数值，不再是独立设计自由度。内核应计算它们，AI 只声明材料分布与所需物理抽象；修改形状后要求 AI 再填质量和惯量，会引入可由程序消除的不一致。

反之，几何相接不能唯一确定焊接、滑动、接触或柔性连接；同一外形也不能确定内部密度、载荷、阻尼、温度依赖或边界条件。这些必须来自作者声明或有来源的外部事实。静态装配配合不自动升级为动力学关节，外观材质不自动升级为密度，选择 rigidBody 也不证明刚性近似在所声明工况内有效。

因此统一规则是：输入和模型假设确定的量由程序派生；未确定的事实和选择以有类型依赖暴露。 缺失输入返回源位置与所需类型，不用默认密度、零惯量或占位形体填补。

9.2 质量矩给出可组合的充分表示

在同一参考系中定义零阶、一阶与二阶原始质量矩：

[ m=\int_\Omega\rho,dV,\quad p=\int_\Omega\rho x,dV,\quad S=\int_\Omega\rho xx^T,dV. ]

对有限、非负且总质量 m>0 的分布，有

[ c=p/m,\quad C=S-pp^T/m,\quad I_c=\operatorname{tr}(C)\mathbf1-C. ]

这三个积分足以确定刚体模型所需的质量、质心和质心惯量；不需要按工业产品类别设计算法。充分性仅针对刚体惯性输入，不意味着能够从这些矩恢复形状、接触、柔性振型或流体行为。

可加性来自积分的线性：若物质域构成无重复的分区，则 m、p、S 分别求和。由此得到任意有限装配的归纳构造：叶子计算质量矩，父级把子级转入共同参考系后相加，再计算父级 c 与 I_c。定义复用允许复用叶子积分；不同 occurrence 是不同物质实例，必须分别计入。一个实例被重复引用不能被重复计重。空间重叠不能默认为合法材料分区：融合体按实际融合区域积分，装配干涉由几何要求独立处理，不能靠矩求和消除重叠问题。

给定右手刚性变换 x’=Rx+t，R^TR=1、det(R)=1：

[ m’=m,\quad p’=Rp+mt, ] [ S’=RSR^T+(Rp)t^T+t(Rp)^T+mtt^T. ]

这是将 x’ 代入积分并展开所得，故组合变换与逐级变换得到相同的理想质量矩。对质心形式等价于 c’=Rc+t、I’_c=RI_cR^T。平行轴项只用于改变惯量参考点；不能再次加到已经关于质心的 Modelica Body 惯量上。缩放不是刚性变换，必须重新解释尺寸、密度与材料域，不能走这一规则。

原始矩是推导与组合语义，不强制数值实现用大坐标下的 S-pp^T/m 相减。成熟算法返回质心惯量时应保留该稳定形式，装配可用质心合并和平行轴定理等价计算，避免远离原点导致灾难性消减。等价公式不能被误当成浮点结果逐位相同的承诺。

9.3 与现有几何、单位和 Modelica 的唯一映射

对已声明均匀密度的闭合有效实体，复用现有 OCCT 体积积分，不自研积分器。几何坐标为 mm、密度为 kg/m³ 时，几何体积乘 10^-9 得 m³，质心坐标乘 10^-3 得 m；单位密度几何惯量的量纲为 mm⁵，乘密度及 10^-15 得 kg·m²。只给体积乘密度，不能得到惯量。

若后端给出的是惯量张量，采用 I_ij=∫ρ(||r||²δ_ij-r_i r_j)dV 的符号约定；非对角元素不是不带负号的产品矩。统一结果取 xx、yy、zz、yx、zx、zy 六个独立分量，映射既有 Body 的 I_11、I_22、I_33、I_21、I_31、I_32。对角项满足三角不等式的依据是 C 半正定，而不仅是 I_c 半正定；现有分析数值检查须继续执行。

Body 的 r_CM 和 I 都必须表达在该组件 frame_a 的轴系中。必须显式解析从几何定义坐标系到分析组件坐标系的变换；世界坐标中的惯量不能直接作为局部惯量。occurrence 的静态位姿不自动成为运动状态约束。绑定 frameRef 的作用是确定物理端口参考系；初始状态及固定/猜值语义仍来自分析声明。

非均匀材料只能在已有能力可计算的显式材料分区上按 §9.2 合并；任意空间密度场需要对应积分能力。薄壳和梁的面积/线密度不是体密度，不以任意厚度替代。缺少这些能力时报告未支持的物性模型，而不是以均匀实体计算结果冒充。

9.4 源声明、派生值与更新依赖

物性来源必须在当前唯一契约中明确二选一：由几何与材料派生，或来自显式外部测量/物性声明。不能让自动值和手填值同时作为同一分量的权威。外部声明保留适用对象、参考系、单位和证据；几何派生保留材料来源及均匀/分区假设。选择外部输入不把它自动证明为与几何一致。

几何派生的依赖闭包为：源配置、实际 occurrence 身份及定义、候选几何实现、材料分配及密度值/条件、参考系变换、积分器身份及数值设置。不可只绑定形状哈希：材料或坐标系改变也必须使输入过期。叶子积分缓存可以不包含世界位姿，但最终分析输入必须包含所使用的变换；缓存命中不得省略当前来源核验。

沿用 §8 的无环封存：源声明 → 候选几何实现 G → 派生物性 → bound analysis → 分析结果 A → 最终实现根 R。派生输入进入现有 inputClosureHash；所依赖的源与 G 必须可恢复。恢复通过保存见证或同一锁定算法重算并核对输入身份，不重新选择材料、刚体划分、关节或设计解。提交仍使用已有候选检查和 Session 原子事务。分析建议改变几何时形成下一候选，不允许反写当前输入闭包制造环。

同一依赖规则贯通发现和诊断：AI 能查询当前选择的物性来源、未满足输入、参考系、派生值及其假设；更改材料或形状只更改权威源。UI 使用同一声明与执行链，不增加维护质量/惯量副本的面板逻辑。

9.5 误差义务与停止条件

积分器的 relativeTolerance 和体积误差估计不是质量矩、惯量或轨迹的严格误差界。若仅有估计，结果明确标记数值估计，不能通过乘密度构造出“已认证惯量区间”。材料不确定度、几何误差、积分误差、坐标变换误差和刚体模型误差各有来源；要求需要认证界而来源不足时为 unknown。

由推导得到本能力的有限实现义务：物质计数与分区正确；密度/量纲转换正确；参考系与张量映射正确；完整来源闭包随修改失效；派生输入通过既有分析准入；封存恢复和失败事务保持同一权威。检验只围绕这些义务，不按飞机、火箭、机器人逐项增加场景。符号推导解决组合规则，源码核对解决实际接线；仅对尚无证据的运行时绑定、序列化及事务行为做必要的整链检查，完成后停止。

9.6 当前实现差异与决策

2026-09-20 源码核对：锁定 replicad-opencascadejs 1.0.0 的声明将 MatrixOfInertia 标为 unknown，但维护版密封运行时 v0.21 的实际声明返回 gp_Mat，构建清单已包含两个类，无需补绑定或第二积分库。measureShape.ts 现复用已有 GProp 积分，提供数值体积、质心和质心惯量的同次读取；显式运行时入口返回复制后的数据并释放 GProp、点和矩阵句柄，不依赖全局 OCCT，既有只读体积调用不额外读取惯量。调用方仍须检查真实闭合材料域，onlyClosed 是积分过滤条件，不是形状有效性证明。现有材料守恒路径只把密度与体积结合计算质量，不能当作本节完整物性实现。

design-analysis-node.ts 已解析 occurrence，却把 frameRef 留为 pending；analysis-delivery.ts 对未解析 frameRef 拒绝。analysis-modelica-components.ts 从显式表达式生成 Body 参数；analysis-numeric-checks.ts 已检查惯量半正定和主惯量三角条件。所缺是几何/材料/参考系到这些现有消费者的完整来源绑定，并非再写一套 Body 或惯量合法性检查。

实施决定：在现有分析源契约中增加明确的物性来源选择，并在共享候选求值上下文解析实际几何、材料与参考系，生成同一有类型标量表达式输入。精确程序的六种数值类型不足以直接承载所有物理量，不能仅为绕过此限制把 Mass 改名 Real，或另建 NumericValues 执行器。分析物性派生应直接使用既有关系数量词汇和分析表达式链；若未来通用程序本身需要物理量，再对其完整生产者/消费者契约统一扩展。

新增原生读取路径已在密封运行时完成一次绑定核验：不设置全局 OCCT 的 2×3×4 长方体返回体积 24、质心 (1,1.5,2)、质心惯量对角 (50,40,26)，与积分公式一致；非对角保留约 10^-14 的浮点残差，不吸附为零。此核验仅确认该绑定与单位密度读取实现，不证明一般几何积分精度；绑定核验到此停止。内核构建与类型检查通过。该读取本身不包含分析来源、材料/参考系转换或封存接线，不宣称 P5 完成。

来源契约现已加入 AnalysisDefinition.physicalInputs：键为既有 input 表达式使用的名字，值为 {binding,property}；binding 引用同一分析的组件 occurrence 绑定，property 为 mass、centerOfMass.x/y/z 或 inertia.xx/yy/zz/yx/zx/zy。有 frameRef 时使用该参考系，无 frameRef 时明确采用几何定义坐标系，不猜世界位姿。来源不存在或未使用的声明在结构准入时拒绝；同名 node.inputs 值以 ANALYSIS_INPUT_SOURCE_CONFLICT 拒绝，避免外部值覆盖派生值。派生声明计入既有编译预算。解析器把它们报告为 pendingPhysicalInputs，不伪造 typed 或 ready；当前交付入口以 ANALYSIS_PHYSICAL_INPUTS_REQUIRED 明确阻止尚未完成的读取接线。

有类型绑定沿用 bindAnalysisInputs：私有绑定投影把输入替换为标量字面量并移除已经兑现的来源请求；权威源节点保留声明及来源身份。此内部函数不构成外部提交授权。Schema、模块依赖哈希、唯一当前 catalog、Core catalog 常量与 SemanticRef 当前身份同步更新，不保留旧模块身份兼容入口。本项完成来源表达和冲突准入，实际候选测量、材料与参考系转换、输入闭包封存仍待接通，不把声明可解析当成分析可执行。

候选测量现进入共享 evaluator：只读取该次 execution.sources 中仍存活的实体，核对 authority 的生产者与输出端口，按 body 的真实材料分配读取锁定材料记录；没有材料、密度无效、非单一 Solid 或未解析 frameRef 均明确拒绝。单次 binding 积分同时供其多个标量输入使用，质量/质心/惯量分别按 §9.3 转换。当前接受域为均匀密度单实体及几何定义坐标系；未实现分区、多实体组合或自定义参考系，不使用过滤闭合子集掩盖缺口。

复制出的 analysisPhysicalInputs 随同候选几何证据封存，证据重验使用同一字段重建哈希；内容包括输入标量、occurrence、材料记录哈希、密度、参考系、均匀体密度假设、积分设置和原始几何矩读数。实际分析绑定通过既有数量推导检查 Mass/Length/MomentOfInertia 后进入原组件编译；inputClosureHash 同时绑定该来源记录。恢复时在真实重建几何上重新取得观测，再检查已保存分析的输入闭包；没有模型证明的数值分析结果也必须先完成来源核对，不能因 proof=unknown 跳过。积分误差仍只是数值估计，未升级为物理有效性保证。

整链接线核验发现 catalog 中 schemaDependencies 投影曾未随模块更新；已修正当前目录，并在现有 generate 命令中加入与 Core 一致的完整模块投影比较，使此类错误在生成阶段失败，不新增 Gate 或独立检查入口。

一次原生 Chrome SDK 事务核验已贯通：10×10×2 mm 实体、真实 6061 材料分配生成质量 0.0005400000000000001 kg（公式值 0.00054 kg），经显式 C=(m/1 kg)×500 J/K 的模型假设进入热容，与导热元件及恒温边界组成分析；set-analysis 的模型证明、候选验证与原子提交成功，关闭并重开保持修订且完成来源重验。500 J/K 是该核验明示的模型参数，不冒称材料库提供的比热或真实部件热验证。此链确认实际来源绑定和保存恢复；未据此宣称一般惯量精度、材料分区、自定义参考系、连续修改重分析或全部历史操作完成。该链核验停止。

连续修改的依赖核对确认：新候选由源文档重新 materialize，旧修订的 analysis 结果不自动携入；已有 before-validate 流程对当前缺少分析结果的节点生成当前证明。相同原生链继续以 set-material 更换为材料库中密度 7900 kg/m³ 的钢材，再以 set-parameters 将宽度从 10 改为 20 mm，质量由 0.00054 更新为 0.00316 kg，两个修改均完成分析、提交并可重开。没有新增失效状态机或独立求值路径；这条证据覆盖该声明域内的材料与尺寸修改，不覆盖所有历史操作或数值后端自动重分析。

公开查询现在从同一已核验几何证据投影 evaluation.physicalInputs，按 analysis node ID 返回 SI 类型值及 binding 来源（body、occurrencePath、生产者、材料记录哈希/密度、参考系、积分设置与数值估计假设）。完整原始积分记录仍保留在内部证据，公开结果不将其伪装为认证误差界。Schema、原生投影、工具上下文及 aira_model_read 描述同步，查询无需 includeSource，也不触发编辑。上述修改—重开链中的真实工具读数与当前派生值和材料身份一致；投影检查已停止。

9.7 局部参考系的所有权与逆变换

源码核对给出明确缺口：AnalysisDefinition.bindings 的 frameRef 是裸 ID，Body 没有对应的局部坐标系注册表；ProductStructure.datums 是工程基准要素，并非带完整原点和轴系的刚性坐标系。不能按同名寻找装配组件、把基准面索引解释为轴系，或从 fixedFrame 组件的模拟连接猜测 frameRef。必须先补齐权威声明，再解除 pendingFrames。

实施决定：坐标系定义属于 Body，分析只是消费者。 在当前 Body 契约增加可选 frames 映射，键是稳定 frame ID，值复用 ProductPlacement（translation 的三个 Length 值和 rotation 的三个 Angle 值）；所有坐标均相对于这个 Body 的几何定义坐标系。引用解析为 (binding.occurrence.bodyId, frameRef)，不是全局字符串检索。无 frameRef 明确指 Body 的几何定义坐标系。同一 Body 的不同 occurrence 共享定义内坐标系；实例的装配位姿仅决定其世界位置，不改写局部物性。

采用现有 placement 的确定约定：x_D = o + R x_F，其中 R = Rz · Ry · Rx，旋转角按现有有类型求值转换为 rad，原点按现有 Length 求值转换为 mm。这里 D 是 Body 定义坐标系，F 是被引用局部坐标系；矩阵列是 F 的轴在 D 中的表达。复用 assemblyPlacementTransform 的 OCCT gp_Trsf 构造与生命周期，不另实现欧拉角旋转器，也不改动装配当前约定。

给定几何积分得到 D 系中的质心 c_D 和关于质心的惯量 I_D，分析所需值是逆变换：

[ c_F=R^T(c_D-o),\qquad I_F=R^T I_D R,\qquad m_F=m_D. ]

推导：点坐标关系为 x_D=o+Rx_F，正交性给出逆式；关于质心的相对向量满足 r_D=Rr_F，将其代入惯量积分定义即得上述共轭变换。平移不改变关于质心的惯量，因此不加平行轴项。Modelica Body 的 r_CM 是组件参考原点到质心的向量，惯量仍关于质心，这两个参考点不能混淆。若未来消费者要求关于 F 原点的惯量，必须是不同的明确字段 I_F,origin=I_F+m((c_F·c_F)1-c_F c_F^T)，不能悄悄改变现有 inertia.xx 等字段含义。

世界装配变换记为 x_W=t+Qx_D。F 的世界位姿是 (t+Qo, QR)，但局部物性依旧为上式；不能先用 Q 旋转惯量再交给局部 Body，造成世界旋转重复应用。物理连接、初始状态与装配位置是否一致是另外的模型约束，不因存在 frames 自动生成关节或锁定运动。

输入依赖与构造顺序。 frames 的 Value 与既有 placement 使用相同字面量/参数/有类型端口绑定。共享图必须收集这些引用并核对类型、源存在和当前配置，数值生产者完成后才计算 frame；不能仅在最终测量函数临时读取尚未执行的端口。几何关系求解可以向 frame 提供已封存的数值结果；从本分析结果再回到本分析 frame 的依赖则构成环，按现有执行依赖准入拒绝，不能通过旧修订值打断。

没有 parentFrame 的第一版声明均直接相对于 D，故 frame 本身无需树遍历或搜索，也不存在同名父链的解析歧义。不同表达可以给出同一变换，不要求规范化为某组唯一欧拉角；封存绑定源声明与实际数值变换，而不是假定参数唯一。若以后确需坐标系层级，先定义带类型的父引用和无环准入，不能把 frameRef 当前裸 ID 当作隐式路径。

保存、编辑与删除。 源 frame ID、声明、所用参数/端口结果以及数值变换都进入物性输入闭包；变换发生变化时旧分析结果失效。Body 修改必须保留未修改的 frames，显式删除或替换 frame 使受影响引用重新准入；找不到 ID 时报告 Body 和 frameRef，不回退到原点或选择另一个同名 frame。替换几何定义时，固定坐标声明可以保留，但这不证明它仍对应某安装面；几何关联含义需要显式关系或要求独立维护。恢复只重算同一源与已封存数值结果，不重新选面、求解或猜轴向。

实现闭合范围。 完整能力须同步 Body Schema/Core 类型、模块依赖及当前 catalog、源引用/依赖收集、既有产品 placement 数值求值、原生逆变换、质心惯量输入、来源封存及公开查询。Native inertia 读取和已有 Body 参数校验不重写。验证只核对变换方向、单位、来源失效和恢复这些具体义务，不按飞机/机器人类别扩展样例。Body.frames 已进入源契约，但尚未开放 frameRef 执行，不能以部分接线冒充完整能力。

原生计算实施状态（2026-09-20）。 assemblyPlacementTransform 已允许显式传入所属 OCCT 实例；measureNativeVolumeProperties 复用此变换并取逆，用原生点变换及 gp_Mat 乘法执行上述质心、质心惯量公式。仍只积分一次，不复制或重新放置形状，不改变全局运行时。变换、矩阵和积分句柄在返回纯数值或异常时释放；只读体积入口不增加这些计算。成熟设施为密封 v0.21 已绑定的 gp_Trsf/gp_Pnt/gp_Mat 与 BRepGProp，Aira 只负责既定参考系语义及所有权接线，没有新增数学库或手写矩阵算法。

一次原生绑定检查用 2×3×4 的均匀长方体及平移 (1,0,0)、绕 z 转 π/4 的目标坐标系，解析结果为体积 24、质心 (1.5/√2,1.5/√2,2)、惯量对角 (45,45,26)、yx=-5；实际读数在 1e-9 绝对比较阈值内一致（该阈值仅为此绑定检查，不是通用交付容差）。检查同时不设置全局 OCCT，确认显式运行时路径；内核完整构建、Web 类型检查与改动 lint 通过。此检查停止，不扩展姿态枚举。该实现仅完成底层转换；Body.frames 源声明、依赖求值、分析闭包和公开编辑仍待贯通，frameRef 继续拒绝未支持的请求。

源契约实施状态（2026-09-20）。 Body.frames 已采用稳定键到 ProductPlacement 的映射，生成类型、依赖模块和 catalog 身份同步到唯一当前契约；Core 校验各坐标的 Length/Angle 类型、参数和端口引用。关系执行投影同时改写 frame 内的关系输出引用；布尔差集覆盖现有 Body 时保留 frames，既有程序及直接几何修改中的 Body 展开保留机制沿用。装配数值求值已提取为 graphPlacement，统一当前求值结果、长度与角度单位转换，不引入第二套实现。源契约可承载声明不代表分析消费者可运行：frame 消费依赖、环拒绝、当前配置求值、来源闭包和公开编辑尚须贯通，未支持请求继续拒绝。契约生成、Core Clippy/WASM、Web 类型及改动 lint 通过；尚未以原生 Interface 核验 frame 编辑/恢复，不声称此项完整完成。

分析引用接线（2026-09-20）。 Core 与工作台的既有引用收集器现已遍历 AnalysisDefinition 的 bindings/outputs 实例，以及 binding 所引用 Body.frames 的数值生产者，将其放入既有执行依赖图；这同时修复了分析定义中实例引用原先未被统一依赖收集识别的缺口。缺失 frame 不回退为原点，源解析报告 ANALYSIS_FRAME_MISSING，并在解析结果中纳入 frame 的端口生产者。工作台源码执行核验只检查依赖边、自依赖环拒绝和缺失 frame 拒绝三项，均通过；不是完整 Interface 分析执行或 Core WASM 行为核验。契约构建、Core Clippy、Web 类型和改动 lint 通过。实际数值求值及来源封存尚未开放，pendingFrames 保留；该状态不宣称 frameRef 已可执行。

当前执行状态（2026-09-20）。 几何派生物性绑定的 frameRef 已贯通当前执行文档、graphPlacement、显式 OCCT 逆变换及来源封存。物性来源记录 body-local/geometry-definition，局部系额外保存 frameSource（稳定 ID、执行文档中的声明、实际 mm 平移和 rad 旋转），进入既有几何证据及分析 inputClosureHash，公开读取使用同一记录。分析交付只在已核对的物性证据包含对应 Body/frameRef 时解除 pendingFrames；恢复使用新测量记录重新核对闭包，没有几何派生输入的 frame 绑定仍保留未支持状态。

现有 Chrome 原生 SDK 链使用已声明的 Body frame（平移 x 引用 p.width，绕 z 旋转 90°）创建热网络分析、提交，再修改材料和宽度。宽度从 10 改为 20 后，记录中的平移及局部质心随当前参数更新；关闭重开后 aira_model_read 返回相同当前 frameSource 与派生质量。此核验覆盖当前源参数修改、提交、重开和公开物性读取，不覆盖独立 frame 创建/替换/删除工具或全部历史操作；到此停止，不再追加姿态枚举。契约生成、Web 类型及改动 lint 通过，未增加数学库。独立坐标系编辑、无物性输入的 frame 绑定及更广工业行为能力仍未完成。

原生编辑入口（2026-09-20）。 当前计划工具增加 edit-body-frames，直接沿用 SDK 的 Schema 发现、Body patch、候选验证、几何保持与原子提交。frames 按稳定 ID 合并，声明替换整个坐标系，null 删除，未给出的 ID 保持；值复用显式 AMIR 长度/角度与参数/端口绑定，不增加第二执行器。删除不存在的 ID 报错，删除被分析引用的 ID 由源引用验证拒绝，不隐式删除消费者或改绑原点。Chrome 原生工具链在已提交修订上完成创建、分析绑定、替换、参数修改、重开及公开来源读取；删除被引用坐标系未提交且头修订不变。创建/替换/悬空引用拒绝的接线检查停止。最初人工非空 genesis 没有候选几何历史证据，触发 REVISION_CANDIDATE_EVIDENCE_CARDINALITY；未放宽恢复检查，改为先正常提交分析形成已封存修订再验证编辑，不把无证据 genesis 恢复计入通过。契约及工具构建、Web 类型、改动 lint 通过。无物性输入的 frame 绑定、完整撤销/重做及工业行为覆盖仍未闭合。

坐标系独立求值与修订恢复（2026-09-20）。 坐标系依赖的是配置和已求值坐标，不依赖材料密度；因此先对全部 pendingFrames 求值并封存到 analysisPhysicalInputs.frames，再由需要质量/质心/惯量的消费者复用同一 frame 结果。没有 physicalInputs 声明时 values/bindings 为空，frames 仍通过既有几何证据与 inputClosureHash 绑定当前来源；公开读取同步返回这些字段。取消了以“没有物性测量”作为阻止 frame 绑定的条件，没有创建平行分析执行器。这里仅确定坐标基与来源，不自动旋转手填物理参数，不推导关节、世界初始状态或运动学一致性。

Chrome 原生计划工具在替换前后两个已提交修订之间使用 restore-revision 往返恢复，公开 frameSource 分别回到参数化平移 20 与固定平移 5；随后将分析改为显式质量输入、保留 frameRef，提交与公开 frames 读取通过，物性 values/bindings 为空。该有限检查到此停止。修订恢复不是 UI 撤销/重做历史选择覆盖，不扩大到所有历史或物理模型。契约构建、Web 类型及改动 lint 通过；整个 P1–P6 及物理模型有效性承诺仍未完成。

实际分析主机边界（2026-09-20）。 已用 WSL 的 OpenModelica 1.27.1、MSL 4.1.0 和项目内临时 Linux Node v24.13.0 执行现有主机，不引入 Windows/WSL 转发执行器。声明内固定热网络完成生成、编译、初始化回读、执行、轨迹解析和制品哈希核验；再经既有 createGatewayServer、关闭模型提供者，核对 HTTP 发现与执行，以及无效定义的具体拒绝码。该结果证明当前模型的实际主机及 HTTP 边界接通，不证明浏览器 numerical 候选已提交或恢复，也不把配置文件身份扩张为完整工具链闭包或物理有效性证明。此边界的运行核验结束。

失败也是原生能力的输出：HTTP 宿主保留限长 ANALYSIS_* 错误码，初始化回读不通过有明确拒绝码；浏览器限量读取失败响应并沿既有结构化异常传播 code，未知格式保留 HTTP 状态诊断。不能把所有失败折叠为 422 后要求 AI 猜测，也不通过响应转发原生过程日志。未新增错误协议或第二执行器。

原生候选封存与公开读取（2026-09-20）。 实际 Chrome SDK 已将几何派生质量送入上述数值链，完成预览、验证和原子提交；禁止访问分析服务后重开仍成功。当前 Evaluation.analyses 与 SDK 读取返回绑定该实现根的分析类型、contentHash 与数值 rowCount，修复此前分析存在但公开读取不可见的缺口；重开后哈希与 12 行记录数一致。该摘要不携带完整轨迹，也不将记录数解释为精度或有效性保证。预先取消请求的拒绝与 head 保持已核对，运行中编译取消尚不能据此认定。验收浏览器显式授予本地网络权限，未放宽产品来源限制。本项接线验收结束，不扩展为全部事件、物理模型或历史操作覆盖。

9.8 有限实例质量集合的实施契约

源语义。 当前 binding.occurrence 必须落在一个 Body，兼作组件局部参考系的所有者；直接允许它指向装配会同时破坏现有 bodyId/frameRef 规则。采用一个明确扩展：binding 可声明非空、有限的 massMembers 数组，成员仍为现有 ProductOccurrenceReference（bodyId、path）。未声明时保持同一契约内的单体含义；声明时，数组完整决定物质实例集合，anchor occurrence 只提供参考系，除非也列入数组，否则不参与计重。这是当前源语义的扩展，不保留两套版本或新增分析执行器。最多 20,000 个成员，解析、依赖遍历与执行均消费现有分析预算，不能让每个 binding 的局部上限绕过全局上限。

同一配置中，同一 occurrence path 只能出现一次；bodyId 必须与该路径实际叶子一致。相同 Body 在不同路径是不同实例，可各计一次；配置禁用、重定向或丢失的实例必须重新解析并拒绝无效引用。不能按 shape hash 去重，因为重复使用同一零件定义并不等于只有一份物质。成员按规范路径键确定累加顺序，避免源列表的排列任意改变数值累加路径。空集合不伪装为零惯量刚体。

物理边界。 集合表示对这些离散实例的质量分布求和，不是几何并集。它既不证明实例无干涉，也不自动焊接它们；使用一个 rigidBody 组件仍是作者明确选择的刚体抽象，热容量等消费者则保留自己的模型假设。融合材料域必须先由真实融合体表达；相交实例不得因质量已相加而显示为已通过碰撞或材料分区检查。每个叶子继续要求一个有效 Solid、真实材料记录及正体密度；壳、梁、任意密度场与单体内部多材料分区仍不能被此扩展冒充。

共同参考系。 令 T_A 为 anchor occurrence 的实际定义系到装配世界系变换，F 为 anchor Body 的 frameRef 到定义系变换（未声明为单位变换），T_i 为成员 i 的实际定义系到世界系变换。成员到分析系的唯一变换为 H_i=(T_A F)⁻¹T_i。必须从当前 execution.product.occurrence 的已求值 placement 取得 T_A/T_i，不能重新读取源初值或忽略装配求解结果。该式直接来自坐标关系的复合与求逆；当成员就是 anchor 时，H_i=F⁻¹，与 §9.7 单体规则一致。局部参考原点到总质心向量与总质心惯量由同一 H_i 表达，不给 Modelica Body 的质心惯量再次加平行轴项。静态 T_i 不自动成为各物理组件的运动初值或约束。

成熟设施与薄适配。 本地锁定 replicad-opencascadejs 1.0.0 的 GProp_GProps.Add(Item,Density) 声明明确支持质量属性组合，并自动应用平行轴定理；Mass、CentreOfMass、MatrixOfInertia 读取组合结果。密封 v0.21 的 Add 已在原生 Interface 创建分析的实际组合链中执行通过；GProp_GProps 与 gp_Trsf 沿用同一运行时。复用原生变换、体积积分和 Add，不自写惯量合并算法或引入第二矩阵库。Aira 负责成员身份、单位、材料来源、参考系及句柄生命周期。几何坐标为 mm 时向 Add 传入 densityKgPerM3×10⁻⁹，仅加权一次；得到质量 kg、质心 mm、质心惯量 kg·mm²，惯量乘 10⁻⁶ 后交付 kg·m²。不能继续对已经加权的组合结果乘第二次密度或使用单体 mm⁵ 的转换系数。积分失败和取消释放全部临时属性、变换与形状句柄。原生积分设置及误差估计仍按 §9.5 标记，不由 Add 自动获得认证误差界。

依赖与封存。 resolveDesignAnalysisNode 除绑定每个成员 authority 外，还必须收集 anchor 与各成员路径上的 placement 输入及相关装配求解依赖。集合任一成员的几何、材料、启用配置或相对位姿改变，都使当前物性与分析输入失效；只依赖 anchor 的生产者是不完整的。共享 evaluator 先验证每个实际 source artifact 的生产者/端口，再取得物性。组合证据记录 anchor/frame、每个成员身份及实际变换、材料 hash/密度、积分设置、组合规则身份和输出单位，进入既有 analysisPhysicalInputs/inputClosureHash。公共读取从同一证据投影成员来源，不能把多材料结果压成一个虚假的 materialId 或 density。恢复消费原分析制品，在当前锁定几何链重建来源并核对闭包，不重新选择物质集合或运行仿真。

源级依赖保持。 Core 的 collect_analysis_references 同样遍历 massMembers，并复用 collect_product_occurrence，而非只校验 anchor。对路径长度归纳：根提供起始定义；每层读取真实组件定义并收集该层 placement/装配求解引用；叶子核验 bodyId 并收集 authority。对有限成员集合取依赖并集即可保留所有成员依赖，无需按产品枚举。配置投影仍先于该遍历，浏览器编译与 Core 源检查承担各自边界。2026-09-21 源级核验确认合法源通过、错误成员 bodyId 在 massMembers/1 拒绝、成员位姿反向引用分析节点产生 DEPENDENCY_CYCLE；Rust fmt/clippy 及 WASM 构建通过。

接线和停止条件。 修改既有 AnalysisDefinition、解析器及依赖收集、物性 evaluator、封存与公开投影，最后贯通现有 bindAnalysisInputs 和分析准入；只加一个求和工具不算完成。数学依据为 §9.2 的积分线性及刚性坐标变换，适用于任意满足前提的有限集合。运行核验只需区分：同定义的不同实例与重复路径；材料/相对位姿修改的传播；带 anchor/frame 的质心及非对角惯量；保存恢复与损坏拒绝。这些是不同的实现义务，不扩展为工业产品枚举。当前 massMembers 已贯通运行时 Schema、全局成员预算、实例与 placement 依赖、原生物性组合、分析输入闭包、封存及公共读取。未声明集合仍表示单体，不生成虚构的集合平均材料。物性标量使用已有 canonicalDecimalText 展开科学计数法，保留浮点残差，不以吸附零来通过十进制 Schema。

2026-09-21 接线核验：同一原生 SDK 链创建两个共享几何生产者、不同 Body/材料的实例，带 anchor 局部平移和旋转，质量、质心及非对角惯量符合独立解析式；修改相对位姿和材料后重新求值，重复路径被拒绝且 head 不变，禁止 Worker 后保存重开保持实现根与公开物性一致。恢复检查器先接受原证据，再拒绝改写成员密度的证据（ANALYSIS_REPLAY_SOURCE_MISMATCH）；实际恢复入口由 evaluator 从当前形状重新测量后传入该检查器，并非信任保存的密度。此负向核验覆盖闭包一致性，不宣称完成所有持久化损坏类型。不同路径不按 Body 或 shape 去重由解析及逐成员组合代码保证；本次运行未额外枚举同 Body 的重复实例场景。相关构建、类型检查与 ESLint 通过。该接线单位不等于 P5 全部完成，也不提升 numerical-estimate 为认证误差界。

源离散类型与记录域的验收交集（2026-09-21）

对离散符号 s 的每个已记录值 v，记录验收谓词必须为 Type_s(v) ∧ Domain_s(v)。区间属于值域限制，不能代替类型：例如 Int 的 [0,2] 不包含 0.5。Bool 的记录编码限于 0/1，Int/Count 在当前 number 记录表示下须为安全整数，Count 另须非负。类型从已检查的源符号取得，不由 CSV 列元数据决定；CSV 词法/编码检查与源域检查分别承担自己的入口契约。

checkAnalysisTrajectoryDomains 已将源标量类型与集合/区间、Count 细化联合检查。一次有界核验确认整数区间内的分数被拒绝、越域值被拒绝，合法 CSV 解码到源域验收的原链保持。这里修复的是可独立调用的源域检查入口；既有产品 CSV 路径已经检查整数编码，不能将本修复说成发现了该产品路径可接受分数的漏洞。本结论不证明事件记录完整、事件间行为或物理有效性。

封存证据的原生读取（2026-09-21）

分析证据应满足读取闭包：一次分析可见的证明范围、未知原因与要求判定，在同一 Realization 保存重开后仍能通过原生读取发现。model.read 的 analyses 因此投影 modelInvariant 与带 source-model-analysis-requirements scope 的 requirements；numerical 结果另投影 sourceModelInvariant，与交付浮点模型的不变量区分。所有值来自已封存且恢复检查的同一结果，精确温度界与时间端点用 n/d 字符串，不从 CSV 推断证明，不重新运行分析。即时工具和读取共用摘要函数；记录数继续只描述已记录行数。公开读取链已核对编辑、提交和禁止求解器重开，仍不属于外部 LLM 自主使用证据。

分析能力的运行环境发现（2026-09-21）

可表达性由源契约决定，可执行性还要求宿主几何准备能力、当前授权及数值后端可用。先前仅在 numerical 执行内部做 GET 身份/预算检查，外部 AI 无法在创建候选前查询，不能满足 P5 的后端缺失可发现要求。现复用同一 inspectAnalysisBackend，不复制身份或预算校验、不增加仿真入口。已有 aira_analyze_candidate 增加 mode:discover，使用同一 SDK Schema 自动进入 MCP；此模式不接收候选/节点 ID，也不修改源模型。

发现继续检查 read/validate 授权、过期、取消及宿主生命周期。结果 scope=analysis-capability-observation 带 observedAt；modelProof 表示当前宿主有源证明执行路径，不表示任意模型适用。numerical 为 available / unavailable / unknown：后端明确报告未配置时 unavailable；网络、身份、预算或忙碌错误保留 unknown 与有界诊断。available 返回与执行相同的后端身份及预算，只在观察时成立；正式执行仍重新检查，不能以一次发现结果替代候选验证、后端绑定或工程有效性。发现只使用宿主连接地址，模型不能指定远端。

实际 SDK 与 MCP initialize/tools/list/tools/call 已核对 discover 无候选参数可调用。浏览器请求使用生产 createLocalAnalysisHandler(undefined) 的真实未配置响应，结果为源证明 available、数值 unavailable/ANALYSIS_BACKEND_UNAVAILABLE，发现前后公共模型完全相同，预取消拒绝；这验证未配置分支和协议接线，不声称本轮运行了 OpenModelica 或证明 available 模式的数值分析正确。工具构建、Web 类型/生产构建和相关 lint 通过；P5 其他物理/事件/耦合义务保持。

发现、执行与回读的后端身份准入（2026-09-21）

原浏览器发现及 checkAnalysisArtifacts 只核对 scope/version，未验证 executable/files。版本字符串相同不蕴含所声明的可执行文件被内容绑定，缺失文件表也不能构成 configured-files-only 身份。因此在既有 analysis-artifacts 契约中统一身份及预算准入：非空可执行路径、1..20000 个文件条目、非空无 NUL 路径、唯一条目路径、合法 SHA-256，且可执行路径必须在清单中；数值预算沿既有上下限核对。身份范围仍只是所配置文件，不证明整个工具链、宿主真实性或物理模型正确性。

浏览器发现及执行前复用此校验，制品检查/恢复同样先检查身份再解析原始记录；移除两处版本/预算的重复局部判断。Node 主机先沿原路径检查要求规范化绝对路径，再复用共享身份/预算规则，实际文件哈希仍按原文件读取核验，OpenModelica –version 仍实际运行。路径规范化后同一路径不能以重复条目进入内容身份；没有自动补清单或猜缺失哈希。

零费用核对：共享制品入口对空表、缺可执行条目、重复路径、坏哈希均在记录解析前拒绝；浏览器原生 discover 收到声称 available 但缺少文件身份的响应后返回 unknown/ANALYSIS_BACKEND_IDENTITY_INVALID，模型不变、取消保持。真实既有本地主机脚本使用 OpenModelica 1.27.1 完成 GET 发现、POST 编译仿真与原始制品检查，返回 200 与内容哈希 f3854f3342e2e61de1d9be0f7b049d815f4f2153124181d43c6d6e749213cc47；非法模型仍为 422/ANALYSIS_SCHEMA_INVALID。首次 WSL 调用因 PATH 中缺 Node 失败，改用项目已有 node-v24.13.0-linux-x64 后通过，未安装依赖。契约/服务构建、Web 类型/生产构建与相关 lint 通过。本项不扩展事件完整性、耦合或全时域误差保证。

数值分析恢复重建交付义务（2026-09-21）

先前恢复检查核对封存内容/原始记录的哈希，以及源模型证明，但没有按当前源输入重新解析数值后端记录。哈希相等仅证明内容对应，不能替代 XML 初始化、CSV 类型/域与交付模型的一致性。现沿 recheckStoredAnalysisModels 的数值分支，使用当前已重放几何和源绑定重建 prepareAnalysisParameterDelivery，再复用 checkAnalysisArtifacts 重新读取原始 initializationXml/trajectoryCsv，比较完整制品内容哈希，并重算 delivered-model-temperature-invariant。该检查在源证明 unknown 的分支之前执行，数值结果不能因缺少源证明而跳过记录核验。

当前数值结果内容新增 numericPolicy，保存与 source.policyHash 对应的规范化策略，参与原内容哈希及 Realization/revision 身份；重开核对该哈希后使用原策略，后端身份与预算取自封存证据，预算不能超过当前源声明。重放不发网络请求、不编译 Modelica、不调用求解器，也不重新选择解。当前项目未发布，不为缺失策略的旧数值结果新增兼容或默认值路径；旧结果需经当前正常分析链重新生成。模型证明结果的现有内容格式不变。

原生 SDK 实际链：两实例几何及材料质量组合驱动 RC 热模型，analysisMode:numerical 经真实 OpenModelica 主机运行、检查与提交；对副本 CSV 改写温度后，直接恢复数学检查入口拒绝，未借用前置哈希闭包的拒绝。关闭 Session 后禁止 Worker 与分析网络请求，重开及 evaluateCurrentHead 保持同一修订和 Realization 根，无新求解/仿真。Windows 无法直连 WSL 回环端口，验收运输使用本地 curl 转发原 HTTP 请求/响应；产品地址、授权和执行实现未改。Web 类型、生产构建与相关 lint 通过。该检查不把数值轨迹变成全时域误差界或物理有效性证明；事件完整性等原边界仍保留。

共享温度的并联热容（2026-09-21）

同一 thermal connector set 的热容满足共同势变量 T，流量守恒给出 Σ Cᵢ·dT/dt = Qexternal，因此 CΣ=Σ Cᵢ>0 可直接代入现有被动 RC 比较包络。该结论对任意预算内有限热容集合成立，不依赖逐个试验。每个 Cᵢ 的严格正值与已知性继续由原参数检查保证；各个固定初温必须精确相等，否则共同温度的初始化不一致，不能通过平均温度掩盖冲突。

现有 compilePassiveThermalInvariant 按 connector set 聚合容量表达式，保留所有组件身份，并把初温相等条件送入相同 Core 精确检查链。温升率、移动包络边界及导数界的分母统一采用 CΣ；每个成员发布相同共同温度导数界，输出要求仍绑定各自组件。源节点、Modelica 组件、物性绑定与几何不被合并或改写。连接热容与理想定温边界、多个定温边界以及无锚代数结点仍保留原 unknown 边界，不由此推断任意 DAE 的可解性。

实际原生计划完成两热容 2、3 J/K、共同初温 300 K、输入 10 W 的模型证明与提交，得到一秒上界 302 K、两个成员各自的导数界 2 K/s。改为不同固定初温时不提交且 head 不变；禁止 Worker 后重开保持原 Realization。此为模型证明与恢复接线验收，未在本轮运行该并联模型的 OpenModelica 数值仿真，也不证明所选集中参数物理模型适用于实际产品。

数值链接线（2026-09-21）。 随后的真实 OpenModelica 运行将 first.T 消元为 second.T 的 alias；原初始化读取只接受 noAlias，因而在数值提交前拒绝合法模型。复用既有 fast-xml-parser 和变量表，读取器现在沿 alias/negatedAlias 解析到直接变量，累计符号并限制最多 64 个访问节点；缺失目标、循环、超限或未知标记返回 unknown。原声明与最终目标均须有有限 start，单位一致，起始值及请求的 fixed 属性吻合，不能只凭别名自身的 start 放行。回读仍核验编译输出，不宣称独立证明整个 DAE 初始化或宿主真实性。

同一原生 numerical 计划经真实本地主机完成编译、回读、仿真、封存提交和禁止 Worker 的重开；两温度输出的 12 条记录一致，末值为 302.0000000000001 K，精确交付模型的包络仍为 302 K。保留这一区别，不把浮点轨迹误差算作零，也不从有限记录推出全时域数值误差保证。真实 XML 副本改变目标初值得到 fail，制造循环别名得到 unknown；矛盾初温候选未提交。契约、服务与 Web 构建、相关 lint 通过；运输复用已有 Windows/WSL 本地 curl 转发，未改变产品接口或启动付费模型。

离散轨迹的初始化一致性（2026-09-21）

域检查只能证明 d(0)∈D，不能推出 d(0)=d_initial。当前事件契约为每个离散符号指定唯一写入组，初始化表达式必须已知；生成器把 initial() 放在 when/elsewhen 的第一分支。因此已交付初始化值与首条离散状态记录必须一致。checkAnalysisTrajectoryDomains 复用已强制输出的 domain-check 列与规范字面量解析，额外核对每组 initial；不增加列或平行检查器。错误码 ANALYSIS_TRAJECTORY_INITIAL_STATE 带原事件组和符号路径。它只补齐首条离散记录的义务，不证明事件完整性、连续初态残差或所有状态转移正确；不能把连续 start 猜值和事件前后记录直接混为固定初态。

真实 OpenModelica 对 Bool 初态 false、t≥0.5 时变为 true 的模型产出 14 条记录，首值 0、末值 1，现有制品读取通过。仅把首条 domain-check 值改成同属合法域的 1，新的初态检查拒绝，证明该义务不被普通域检查替代。原生候选最终仍被 ANALYSIS_ENGINEERING_EVIDENCE_REQUIRED 拒绝：现有工程证明仅覆盖被动热网络，不覆盖此事件系统，不能把后端执行成功当作可提交证据。下一项功能缺口是为声明的事件系统接入适用的源模型/转移证明及工程要求检查，而不是放宽该拦截条件。

有限时间触发的离散更新证明（2026-09-21）

首个规则接受无连续组件、无额外方程、全部状态为显式离散符号的封闭系统。事件写入所有权和完整赋值沿用原契约；每条守卫为 time≥τ 或 time>τ（含交换两侧的等价写法），τ 为已知时间表达式；每个更新值也是已知表达式。未知实数、状态反馈、连续耦合及任意守卫不进入本规则。这里“已知”仍须由 Core 精确求值成功，编译状态不等于证明通过。

证明按事件序列归纳：各初值在对应域内作为基例；每个分支的全部赋值在对应域内，因此更新保持不变量，未触发期间状态不变。各时间守卫随时间单调且最多产生一次上升沿，elsewhen 的声明优先级只能抑制触发，不会增加触发次数；初始化赋值与更新均不依赖离散状态，故不会构成状态反馈的事件迭代。整个有限时间域的事件组激活数不超过组数加分支数。重合阈值与同组优先级不要求枚举状态组合；即使某分支不可达，检查其更新保持域仍是保守充分条件，失败不证明真实轨迹越界。

compileScheduledEventInvariant 复用 compileAnalysisNumericChecks 和同一 RelationExpression/Core 算术，将每个初值/更新的域成员关系、整数细化及 Count 非负性编译为谓词，保留事件源路径、阈值、赋值表达式及激活次数上界。复杂度随源分支、赋值和显式域成员规模增长，并消费原编译预算；没有新求解器、状态空间遍历或事件仿真器。实际 Core 求值核对通过模型的全部 7 个谓词、域外更新的失败谓词和状态反馈的 unknown。当前只完成证明编译层，尚须接入候选模型证明、要求检查、公开 scope 和封存恢复；不得以 compiled 直接授权提交。

候选与恢复接线（2026-09-21）。 checkAnalysisModelInvariant 在现有分析链中选择有限定时更新证明或被动热包络证明；前者公开 source/delivered-model-discrete-domain-invariant，返回状态列表、源语义激活次数上界及精确时间域，不伪装成温度界。域充分条件未建立时返回 unknown，详细谓词证据保留。源证明、交付证明、要求检查进入既有内容哈希与 Realization；恢复核对源/交付证明家族一致并沿原检查器重算完整证据，不新增恢复执行器或仿真调用。

数值离散状态的直接输出范围要求使用该状态的初始值与所有分支赋值形成保守包络。全部值位于有序接受区间可证明全时域范围成立；初值越界是实际反例；只有其他赋值越界时保留 unknown，因为该分支可能不可达。Bool 不进入数值范围比较，physical-bounded 要求仍需物理证据。此规则既不枚举状态组合，也不从有限 CSV 采样推出全时域性质。

实际原生 SDK numerical 计划完成 Bool 定时事件的真实 OpenModelica 编译、14 行轨迹、封存提交及禁止 Worker 重开；首值 0、末值 1，篡改首条域检查值为 1 被初始化检查拒绝。实际 Core 对 Count 0→1 核对范围 [0,1] 为 pass、[0,0] 为 unknown、[1,2] 为初态反例 fail。契约、工具、Web 生产构建（含类型）与相关 lint 通过；没有新付费调用。该结果证明此声明族的候选与恢复链已接通，不证明后端事件无遗漏、状态反馈混合系统的可解性或工程物理适用性。

规则选择与共享编译（2026-09-21）。 规则是否适用与证明前提是否成立是不同层次。事件规则返回 unknown 后再调用热规则，会把 scheduled-reset-not-known 覆盖成 mechanical-model-or-events，使 AI 无法判断应修改更新表达式还是整个物理模型。现在由已校验的 eventGroups 声明选择事件或热规则，模型证明和要求检查保持同一诊断；包含事件的混合模型仍诚实报告事件规则不覆盖，不能靠另一规则丢弃其事件。compileAnalysisNumericChecks 每次证明请求仅执行一次，两个规则直接消费 CompiledAnalysisNumericChecks 并扩展其私有表达式程序，不再次绑定源输入；调用方不共享该可变程序给另一规则。删除旧输入签名，不新增兼容入口。

实际 Core 检查确认状态反馈的模型与范围要求均为 unknown / scheduled-reset-not-known；原事件范围 pass/unknown/初态 fail 保持。真实 SDK 并联热容仍提交 302 K 上界，矛盾初温拒绝，禁止 Worker 重开保持。契约构建、Web 类型检查及相关 lint 通过。此为规则接线正确性修复，不扩大接受域或宣称新增自主 AI 成功率。

公开规则发现（2026-09-21）。 原 mode:discover 只返回 modelProof.available，无法让外部 AI 知道新增事件族是否可用。现由各证明编译器导出规则说明及同一个 rule 身份，既有 SDK 返回接受条件、保证、rangeOutputs 与 excludes。说明是发现信息，候选适用性与全部前提仍由执行链检查；不能据发现结果授权提交。数值后端状态独立返回，后端不可用不掩盖本地证明能力。工具描述指向同一计划的 set-analysis 与完整范围保留语义，不增加另一个建模入口。

实际 SDK discover 在受控 HTTP unavailable 响应下返回两类规则、数值 unavailable，head 保持；本项未调用真实后端或付费模型，不代表自主 AI 理解率。契约/工具构建、Web 类型和相关 lint 通过。

有限定时功率驱动连续热网络（2026-09-21）

事件子系统的所有初值/更新已知且满足域约束时，任一时刻的离散功率属于这些赋值的集合。因此每个热源可取 q_min=min(initial,updates)、q_max=max(initial,updates)。不需要计算分支的实际可达性或事件时刻顺序：扩大可取值集合只使包络保守。多个源即使存在相关性，逐源极值求和仍包含实际净功率。

对热容组 C>0，使用各组 Q_min/C 的全局最小值与 0 中较小者作下界速度，Q_max/C 的全局最大值与 0 中较大者作上界速度。被动导热在全局极值面的方向条件继续成立，定温边界位于初始温度盒内。切换不重置热容温度，有限次事件之间应用原比较原理，事件处由连续性拼接，故原全时域温度包络仍成立。导数绝对值采用 max(abs(Q_min),abs(Q_max)) 加原导热通量界，再除以组总热容；不能只取正功率上界，否则冷却幅值较大时会低估导数。

实现复用 compileScheduledEventInvariant 生成子系统域义务，compilePassiveThermalInvariant 将同一参数 IR、事件检查和热检查合并。事件编译器的输出只证明离散子系统；独立模型入口仍要求封闭离散系统，组合入口还严格检查热组件、完整功率方程及已知参数。当前组合仅接受热流右侧为已知表达式或直接离散 Power 变量；任意反馈更新、一般守卫、任意连续方程、非线性控制均保持 unknown，不以一次后端运行替代证明。公共热规则说明同步该接受域。

实际模型证明以 −5→10 W 驱动 2+3 J/K 的共享热容，得到 [299,302] K，状态反馈编辑拒绝且 head 保持，免 Worker 重开通过。真实 OpenModelica 数值链采用 −20→10 W、阈值 0.5 s、初温 300 K、区间 [0,1] s；精确证明得到 [296,302] K、两组件导数绝对值界均 4 K/s。14 条记录从 300 K、−20 W 到 298.9999999991 K、10 W，要求检查、封存提交与免 Worker 重开通过，矛盾初温编辑拒绝。契约与 Web 构建（含类型）及相关 lint 通过。数值记录仍不证明事件完整性或全时域积分误差，几何物性绑定与物理适用性须沿既有契约另行核验。

组合模型的联合范围要求（2026-09-21）。 温度证明使用离散功率赋值包络后，不能丢弃该包络而令同一模型的功率输出要求返回不支持。热证明编译结果现保留其事件义务已覆盖的 assignments；共同要求检查按输出符号选择证据：数值离散变量使用初始/重置赋值，热容温度使用连续包络。两者消费同一组精确前提，Bool 仍不进入数值范围，物理有效性要求仍不因模型证明而通过。

实际 SDK 创建两热容温度要求及一个离散功率要求；只将功率要求收紧至 5 W 时拒绝且 head 保持，联合把源切换功率 10 W 改为 5 W 则三项要求通过并一次提交，温度上界从 302 K 改为 301 K、导数界从 2 改为 1 K/s。禁止 Worker 重开保持最终实现根。首次核验脚本读取错误字段 requirementChecks，改按现有封存字段 requirements.checks 核对；未改产品数据契约。契约构建、Web 类型及相关 lint 通过，无新增数值仿真或付费模型调用。

关系物理量输入与时间无关输出（2026-09-21）

跨关系端口的物理量必须区分两种单位表示：规范见证的量纲字符串描述 SI 维度，而交付原子与变量声明使用词表登记的实际单位。例如热容的 m^2kgs^-2*K^-1 不自动成为合法输入单位，J/K 才是当前登记符号。TS 现从共享词表按名称排序选择 scale=1、无 pi、offset=0 的单位，与 Core canonical_unit 的规则一致；lowering、精确专门化和联合变量使用该单位，空单位省略。精确输出和结构见证仍使用原规范量纲，哈希含义没有被改成显示单位。Core 普通常量准入复用同一词表，检查物理实数的规范十进制和登记单位，未登记量及错误单位仍拒绝；既有基础量编码规则保留。

对于类型分析已证明不依赖 var/time/der/pre 的表达式，绑定参数后表达式在时间上恒定。按表达式 DAG 归纳，其叶为同一已绑定常量，每个操作及有效域不随时间变化，故输出的全时范围可取单元素集合。共同范围检查复用 Core 原精确谓词与定义域处理，不引入新数值求解器。模型不变量前提仍须成立，浮点交付与物理有效性继续各自核验；本规则不使未知动态模型通过，也不把已知表达式等同于无条件有定义。

真实 SDK 将关系板宽映射为声明的热容输入，再与第二个 3 J/K 热容求和。高度修改带来第一热容精确 5→4 J/K，分析来源哈希更新，范围要求通过；错误 W 单位与过窄容量范围均拒绝、head 保持，禁 Worker 重开保持实现根。该尺寸—热容关系是显式模型假设，不是由几何测量自动证明的材料规律。Bool 联立路径同批核验，修正空单位编码后通过。contracts/WASM/Web 构建、类型、Rust clippy 及相关 lint 通过。

同一修复的联合端口路径已核验：第二关系以 HeatCapacity 未知量表达上游热容加 3 J/K，将解作为分析输入；上游尺寸修改后该解精确从 8 变为 7 J/K。操作仍只声明源变量、单位和等式，未向客户端增加矩阵或中间求解值。下游范围检查、错误单位拒绝、冲突拒绝和禁 Worker 保存重开均通过。该验证覆盖联合变量声明与精确输入专门化，和直接物理量端口共用原来的编译、证据与恢复链；不另建模型或求解器。

已证状态范围的表达式组合（2026-09-21）

输出可以是表达式，而不必直接等于一个状态。已有模型证明给每个受证叶提供区间 [l,u] 和初值：已知参数表达式是单点，热容温度使用比较原理区间，数值离散状态使用已检查初始/重置赋值的 hull。对源表达式 DAG 作结构归纳：neg 取 [-u,-l]；add 取 [la+lb,ua+ub]；sub 取 [la-ub,ua-lb]；mul 的最小/最大值取四个端点乘积。矩形域上线性分量的极值在端点，故该乘法区间包含所有合法乘积。原类型系统先验证单位及绝对温度语义；区间编译不绕过类型规则。

这些区间通过 Core 的精确算术、比较和 select 求值，不新增浮点区间库。每个表达式记忆化一次，显式栈避免递归深度问题，受现有节点预算和取消控制。所有要求按稳定 ID 编译，避免源对象序列化顺序改变临时表达式 ID 和封存证据。初值表达式同步组合，用于可靠的初始违反判定；包围不能装入要求但初值合格只返回 unknown。相关性不由区间自动推断，例如同一状态相减可能仍得到宽区间，不能凭实际样本零差强行收紧。未知叶、一般动态除法、非线性函数及状态选择不在本次扩展中。

实际公开 SDK 对已有热模型的 -(T1-T2)*C1 输出：温度全时域 [299,302] K、C1=2 J/K，因此能量区间 [-6,6] J 通过；收紧到 [-5,5] J 为 enclosure-insufficient/unknown，初始违反 [1,6] J 被拒绝，两者不改变 head。成功状态禁 Worker 重开保持实现根。首次重放发现要求顺序不稳定，修复为稳定 ID 顺序后完整路径通过。该结果复用已有模型假设，不宣称新物理模型、连续相关性或数值积分误差已经证明。