数值交付、容差与几何退化规约

研究总览 · 2026-09-20

本文是关系内核的待实现规范。它补齐关系编译与验收边界，不声称当前代码已满足，也不改写或重跑 §12.8 探针。需求仍由当前 AMIR assertion、有效配置和 tolerance profile 定义；数值编译视图、求解配置和证据均不形成第二份要求权威。

• 1. 容差与数值表示的权威
• 2. 编译与检查的数据形状
• 3. 候选验收、问题无解与表示不可交付
• 4. 非线性编译、缩放与终止
• 5. 几何退化、拓扑与封存
• 6. 既有代码接线与完成条件
• 7. 精确设计见证与执行交付分离

1. 容差与数值表示的权威

量	权威与来源	可以决定什么
需求接受范围及偏差	当前 assertion，或该 assertion 明确引用的 profile 字段	最终允许交付的量值范围
求解终止阈值	锁定后端数值配置	搜索何时停止；不扩大需求范围
表示、构造、测量误差界	对应转换或算法的已核验保证	为受检量给出包含区间
建模、相交、fuzzy、缝合容差	当前 profile 与实际操作参数	近重合实体的处理；不自动成为需求偏差或测量误差界

复用 ToleranceProfile 的 modelingLinear、modelingAngular、intersectionLinear、fuzzyBooleanLinear、sewingLinear、constraintLinearResidual、constraintAngularResidual、validationDistance、quantityRelative，不另建一组同义全局 epsilon。每个使用点必须说明采用哪个字段、为何适用于该量和如何转换单位。

当前 assert.numericRange 自带显式 tolerance，不得借用几何 profile 覆盖；assert.productDistance 的当前语义明确使用 validationDistance。编译器分别展开各 assertion 的既定接受规则，保留引用与原文，不能把二者统一成隐式放宽。新增规则需要修改同一权威契约。

源数值沿用 AMIR Value：带类型和单位的 canonical scalar 字符串、参数引用或已声明的数值结果引用。ConstAtom 明确禁止 JSON number 作为 canonical numeric scalar；不要先经 Number() 再恢复其“精确十进制原意”。

canonical decimal 的词法沿用 Rust 校验器：例如 "1.2" 合法，"1.20"、"1e-3"、"-0" 不是该格式。编译后有理数可以使用下节 Rat；它不是允许用户把 AMIR 常量改写成 "6/5" 的新语法。

编译器在精确十进制语义下直接解析字符串；有限十进制得到精确有理数。长度的有理换算可以保持精确；角度 deg → rad 涉及 π，必须保留符号因子或使用有依据的包围界，不能把一个 π 浮点常量称作精确有理换算。展示值和舍入位数不决定验收域。

求解与几何调用边界允许 binary64；封存其有限值的 64 位位型，不能只保存经过显示格式化的字符串。JSON 中仍不写工程浮点 number。±0 在模型值层按既有规范归一；诊断需要原始位型时可保留其区别。NaN、无穷和溢出不进入有限工程值。

未声明的放宽量为零；只有当前权威契约明确引用的默认值才能生效。制造公差、数字模型误差预算和算法停止阈值分别记录。允许制造偏差不自动授权数字建模消耗同等误差。

2. 编译与检查的数据形状

以下 TypeScript 描述编译产物和检查结果，实施时由当前 contracts 的唯一 schema 生成类型与校验器。string 别名均有下述运行时约束，不代表任意字符串可接受；源字段仍读取现有 Value，这里仅保留其位置。

type Hash = string;
type StableId = string;
type JsonPointer = string;
type DimensionId = string; // 指向编译器量纲登记；Angle 与 Ratio 不混同
type UnitId = string;      // 该量纲的已登记规范单位
type TriState = 'pass' | 'fail' | 'unknown';
type Rat = { n: string; d: string }; // 既约整数；d > 0；零仅 0/1
type Binary64 = { bits: string };   // 恰好 16 个小写十六进制字符，MSB 在前
type Bound =
  | { kind: 'finite'; value: Rat; closed: boolean }
  | { kind: 'negative-infinity' }
  | { kind: 'positive-infinity' };

interface AuthorityRef {
  modelHash: Hash;
  configurationId: StableId | null;
  assertionId: StableId;
  sourceValuePointers: JsonPointer[];
  profileFieldPointers: JsonPointer[];
  inputClosureHash: Hash;
}
interface AcceptanceView {
  authority: AuthorityRef;
  ruleHash: Hash; // assertion 操作语义与展开规则的锁定身份
  dimension: DimensionId;
  unit: UnitId;
  lower: Bound;
  upper: Bound;
  derivationHash: Hash;
  relation: 'exact' | 'inner' | 'outer';
}
interface ScaleView {
  sourcePointer: JsonPointer;
  dimension: DimensionId;
  unit: UnitId;
  offset: Rat;
  scale: Rat; // 严格正；不承载需求容差
}
type NumericEvidence =
  | { assurance: 'exact'; value: Rat; certificateHash: Hash }
  | { assurance: 'enclosed'; lower: Rat; upper: Rat; certificateHash: Hash }
  | { assurance: 'native-checked'; observed: Binary64;
      methodHash: Hash; nativeVerdict: TriState; diagnosticHash: Hash }
  | { assurance: 'none'; reason: string };
interface RequirementCheck {
  subject: 'candidate-requirement';
  authority: AuthorityRef;
  realizationHash: Hash;
  acceptanceViewHash: Hash;
  dimension: DimensionId;
  unit: UnitId;
  status: TriState;
  evidence: NumericEvidence;
  reason: string;
}
type ProblemConclusion =
  | { subject: 'mathematical-domain'; status: 'feasible';
      domainHash: Hash; witnessHash: Hash }
  | { subject: 'mathematical-domain'; status: 'proven-infeasible';
      domainHash: Hash; certificateHash: Hash }
  | { subject: 'mathematical-domain'; status: 'unknown';
      domainHash: Hash; reason: string };
type DeliveryConclusion =
  | { subject: 'delivery'; status: 'ready'; realizationHash: Hash;
      requirementChecksHash: Hash; geometryChecksHash: Hash }
  | { subject: 'delivery'; status: 'representation-unavailable';
      domainHash: Hash; representationHash: Hash; certificateHash: Hash }
  | { subject: 'delivery'; status: 'unknown'; reason: string };

AcceptanceView 是 assertion 在当前输入闭包中的可丢弃展开缓存，不能编辑、反写 assertion 或以求解结果覆盖其界。每次使用先匹配源、配置、profile 和规则身份；缓存失效必须重新展开。lower/upper 是编译后的接受范围，不是另一份需求。

Rat.n/d 遵守 canonical integer 语法且互质，禁止 -0、前导零、零分母；有理运算复用已选 num-rational/num-bigint，设置位长与预算上限。Binary64.bits 从 IEEE 754 位型读写，不经格式化十进制中转；其有限值可精确转成二进制有理数。操作预算超限返回 unknown。

有理端点不足以精确表达的接受集不得伪造 Rat。例如角度换算可在原有理单位检查，或保留带推导的内外接受视图；内视图通过可接受、外视图不相交可拒绝，其余 unknown。内外方向必须由规则证明，不由候选自行选择。

AcceptanceView.relation 明确记录此方向，derivationHash 绑定其依据；两个近似视图必须指向相同 authority/ruleHash。lower 只能是有限值或负无穷，upper 只能是有限值或正无穷；端点顺序、开闭性及空区间均核验。编译得到空接受集可用于对应要求的证据，但不能把编译器错误或未知端点当成空集。

NumericEvidence 的 exact/enclosed 针对指定数字受检量，不暗示真实制造品或物理模型准确。certificateHash 指向实际可核验内容及检查器身份；只有散列没有可获取内容，不构成证据。native-checked 是锁定原生方法的工程检查，不是精确证书。

问题结论不沿用候选三态：一个候选失败不能写成 proven-infeasible。布尔拓扑检查使用同样的候选层次、三态和方法身份，但不伪装成标量区间；交付汇总同时引用数值与拓扑检查。

mathematical-domain: feasible 必须有对该域的可核验见证；仅工程 native-checked 通过可以按已声明策略交付，但不能凭此升级为数学存在性证明。representation-unavailable 的证书须同时标明数学域、交付表示限制及排除全部表示见证的依据，不能只有一个舍入失败样本。

3. 候选验收、问题无解与表示不可交付

设 assertion 定义接受集 A，测量器保证真实受检量 q 位于 I=[L,U]。确定性规则为：

[ check(I,A)=\begin{cases} pass & I\subseteq A,\ fail & I\cap A=\varnothing,\ unknown & \text{其余情形}. \end{cases} ]

原要求	pass	候选 fail	unknown
q ≥ a	L ≥ a	U < a	其余
q > a	L > a	U ≤ a	其余
q ≤ b	U ≤ b	L > b	其余
a ≤ q ≤ b	L ≥ a 且 U ≤ b	U < a 或 L > b	其余

等式带显式偏差展开为 [target−τ−, target+τ+]；没有偏差就是单点。闭约束也可编译成余量 m(q)≥0，其区间下界非负才通过。源中的严格边界不能静默变成非严格边界，方向变换必须同时变换开闭性。

全部硬要求的合取：任一候选 fail 即候选失败，全部 pass 才通过，其余 unknown。当前 assertion 的 onUnknown: fail 表示阻止提交，诊断仍保存 unknown；不把认知上的未知改写成数学反例。暂停、取消、超预算同样不得产生交付成功。

对 native-checked，按该 assertion 已声明的原生检查方法报告工程 pass/fail/unknown，并显式携带此证据等级；不能套用上表声称已获得包含区间。要求精确/包围证明时，这种证据只能产生 unknown。核验器不能为获得 pass 自行降低要求的证据等级。

误差界只从有依据的转换和测量保证获得。独立阶段的已证明绝对界可保守相加；带相关性的表达式使用适用包围运算，不能假设随机独立后取均方根。observed ± epsilon、样本最大误差、求解器残差均不自动构成严格 I。

OCCT 的实体 tolerance、fuzzyBooleanLinear 与积分/测距算法参数也不自动证明任意测量误差界。缺少严格界时保留 native-checked，不把工程检查包装成已证真/已证伪。后端失败应保留错误、输入和方法身份。

整个接受域不可行必须有覆盖该域的证书。外近似须满足 Faccepted ⊆ Fout；只有 Fout 的已核验不可行证书可以排除接受域。内模型无解、一个局部 NLP 失败、一个构造失败都不足以排除原域，参见证据规则。

3.1 §12.8 边界的准确分类

该探针限定 D=1、固定对称族，要求 1≤p≤P、1/2≤h≤T、p²/4+h²≥1。当十进制边界为 P=6/5、T=4/5 时，上角点满足等号；函数在该正域对两个变量严格递增，所以唯一数学见证是 (p,h)=(6/5,4/5)。

既约分母含 5，两值均不能以有限 binary64 表示。因此零接受容差、该结构族及 binary64 参数交付限制的交集为空；这是表示域结论，不是原数学需求无解，也不是所有 IEEE 754 软件都不能处理该设计。

探针源码 的 binary() 精确解释返回位型，verify() 用有理算术检查板界与 28 对孔距。历史 A/B 未通过的结果记 unknown，因为探针本身没有输出表示域证明；本节推导补充解释，不改其统计。

保留有理语义能表达数学见证，不自动生成合格 B-Rep。合法处理是选择已支持且能通过检查的交付表示，或报告 representation-unavailable。修改需求偏差必须经正常需求编辑；不得在求解器内部悄悄加入容差。仅某候选舍入后失败时，不能报告整个表示域不可交付。

4. 非线性编译、缩放与终止

变量采用 zj=(xj−oj)/sj，sj>0，其中 x、o、s 同量纲。o、s 从声明范围或显式典型尺度确定，在一次求解内固定；所有选择与逆变换进入编译身份，不随候选结果改变。

每条约束独立采用 r̄i(z)=ri(o+Sz)/σi，σi>0 且与 ri 同量纲。原要求 |ri|≤τi 转成 |r̄i|≤τi/σi；源要求不变。给距离残差、距离平方残差、角度和无量纲正交条件分别选择尺度，不能共用一个长度阈值。

例如距离允许下限 D−τ 时，在非负距离域可用 distance²≥max(0,D−τ)²。不能把 mm 的 τ 直接减到 mm² 的 D² 上。原非负性、单位和转换证明同时进入检查映射。

角度接受范围用明确单位描述。单位向量差满足 ||a−b||=2 sin(θ/2)，其阈值须按此关系转换；叉积模 sin(θ) 在反向时也为零，不能单独作为同向证明。常规有符号角度区间也不等于周期角度区间，沿用 assertion 的已声明语义。

固定求解配置显式记录 tol、constr_viol_tol、迭代/时间预算和缩放方法。新硬约束路径将 bound_relax_factor=0，避免默认放宽变量界；g/lbg/ubg 与 lbx/ubx 保留硬条件，不替换成仅最小二乘目标。正的停止阈值不表示允许同量误差交付。

IPOPT 官方选项 区分缩放后的 NLP 终止误差、约束违反阈值与变量界放宽；这些都是求解行为参数。适用配置由锁定后端身份承载，任何算法“成功”标签均不代替源单位下的最终检查。

达到迭代上限但返回有限候选时，纯可行性任务仍可独立核验。可行不等于最优，局部最优不等于全局最优。异常后遗留 stats 不属于本次结果；每次候选、状态、证据必须绑定同一调用身份。

整数候选不得直接以“距整数很近”视为满足整数语义；可尝试舍入为新的候选，再对所有约束完整核验。恢复映射、单位转换与序列化后的值均参加检查，不能只核验求解器内部的高精度临时量。

数值 rank 阈值只支持带阈值的诊断，不自动证明自由度或全局唯一。非线性坐标图失效时，允许回到等价原约束或其他已证明适用的图；这不是扩大设计域，也不是原需求无解。

5. 几何退化、拓扑与封存

几何边界遵循以下固定处理，不以“再次加大 epsilon”作为默认恢复策略：

1. 零长度轴、零法向量、非法半径、非有限坐标等按操作前提诊断；不选任意备用轴替代作者意图。
2. 正间隙要求按实际声明阈值检查。间隙区间跨越接触边界时为 unknown；不能用中心值猜测分离。
3. 接触、相切、零厚度、非流形输出是否合法由操作接受域和输出类型决定。合法曲面不能当作合法实体，所有接触也不能一律禁止。
4. fuzzy、healing、simplify 是已声明构造策略的一部分，参数固定并记录；禁止不断放宽直到 IsValid() 返回真。
5. 分别检查 B-Rep validity、输出类型、连通性及所需语义角色。几何距离变化小不保证孔数、连通分量或引用身份不变。
6. 替换构造只能在已声明等价范围内进行，并重新检查几何和引用恢复；若需要改变接受域或拓扑要求，走需求编辑事务。

替换的充分条件、整个参数族与未来编辑的证明见构造替换规约。数值误差如何与物理模型误差、耦合残差及原工程要求组合，见工程有效性规约；不能把几何有效或某个残差小直接升级为物理要求通过。

OCCT 布尔运算规范 中，实体 tolerance 参与干涉判定，fuzzy 是附加用户指定容差，可改变近重合实体处理。它们不是对结果无影响的性能选项。

精确几何谓词 解决所声明的 orientation/incircle 等符号判定；不能由此推出一般修剪曲面求交、构造或后续实体都精确。检查器的接受域与证据等级必须保持明确。

所有结果在 shared candidate evaluation 内检查。Realization 绑定实际浮点位型、构造策略、后端身份、源输入闭包、容差 profile 身份与检查规则。源、配置或 profile 变化使旧证据失效；旧证据不能跨不同接受域复用。

提交前检查实际待提交形状和引用映射。历史恢复使用当次封存值和构造策略，不再次搜索或自动换一个更宽容的 profile；资源缺失、身份不符、重放检查失败均停止恢复并保留诊断，不偷偷修复源设计。

6. 既有代码接线与完成条件

当前源码已存在分量纲 profile 与独立 assertions，但以下数值路径不能直接宣称符合本规约：

位置	当前行为	实施时必须改变的职责
inspection-evaluator.ts 的 checkRelationViolations	max(1e-4, 10*tolerance/scale) 导出方向阈值，并将方向误差换算成 errorMm 汇总	显式绑定线性、角度或无量纲要求；诊断保留真实量纲
solver.ts	ipopt.tol=1e-12，在 stats.success !== true 时先拒绝结果	分开搜索终止、候选验收与最优性；不得把 tol 当交付精度
AMIR schema	canonical scalar、ToleranceProfile、assertions 已有权威位置	复用并明确字段语义；不增设可编辑的平行数值要求
有理证书规约	已选成熟有理数设施及预算边界	复用有限代数核验；一般 OCCT 曲面不伪装成精确有理模型

实现完成必须同时满足：canonical 字符串或引用到精确语义的编译、量纲检查与有依据的缩放、可追溯接受视图、三态候选检查、独立问题/表示域结论、实际几何及封存重放。类型能通过编译并不等于上述语义已经接通。

验收使用既有产品操作和构建检查，覆盖边界开闭、单位变换、表示不可交付、候选越界、区间跨界、非线性停止与拓扑变化这些机制。它们用于核对实现，不以逐个产品遍历来建立理论。研究探针仍保留原有输入、计时范围、统计和局限。

7. 精确设计见证与执行交付分离

7.0 接线次序：先保持语义边，再交付执行叶

当前实现已为关系封存块增加必需的 exactOutputs：键为公共数字端口，值为名义数量类型、规范单位和精确有理见证。它与原 outputs 的执行值职责分离，共同纳入块哈希。联合恢复只从精确见证恢复辅助列，经原联合约束检查、生产者表达式重算比较，再用私有精确 AST 绑定消费者；整块仍须重新生成并比较哈希。当前契约不保留缺失此字段的旧封存块兼容分支。该分离不自动启用浮点交付，也不把保存的见证本身当作源等式证明。

执行单位须在舍入之前确定。现有几何 graphLength 使用毫米，Number(米值) * 1000 会引入额外的浮点运算；只封存米值的转换误差不足以描述实际参数。Core 转换入口因此增加数量请求 {type, unit, value: Rat}：复用现有词汇求出规范值与交付单位的仿射关系 w = s u + o，精确计算 u = (w-o)/s 后仅舍入一次。返回的 bits/exact/decimal/absoluteError 均属于交付单位，同时提供 canonicalExact 与 canonicalAbsoluteError；请求哈希绑定源有理值、类型和交付单位。Int/Count 不允许舍入改变离散值；含 π 的单位转换保持 unknown。叶接线应交付 mm/rad 等执行器本身的单位，不能把这份参数误差当作几何误差界。

构造叶与数值输出现沿此入口交付，封存块的必需字段 numericDeliveries 以转义后的配方指针为键，记录 type/unit/source/bits/exact/decimal/absoluteError/canonicalExact/canonicalAbsoluteError，数值实现身份沿用块的 numericIdentity。同一块保存实际执行字面量与这些记录；Core 读取时根据 source/type/unit 重新转换，逐字段核对并拒绝下溢至零，源恢复则重新 lowering 并比较整个块。原生 evaluation.realization.relations 同时公开 exactOutputs 与 numericDeliveries。记录覆盖有限十进制的转换，不仅覆盖非终止小数；Bool 继续精确传递。名义 numericRange 要求绑定使用 §7.5 的精确范围封存与独立检查，不通过舍入改变被检对象。

2026-09-20 源码核对发现，同一 materializeRelationScalarsJson 既用于 relation-lowering 的构造输入，也用于 relation-joint-execution 的 outputLiteral；联合恢复还从封存 outputs 的十进制字面量取得边界值。Core known::Evaluator 的 input 路径同样只读取 const 标量。因此将该物化函数的 nonterminating-decimal 分支直接改为 round-to-binary64，会同时改变语义连接，而不只是几何调用精度。现阶段保留拒绝是正确的，不能把全局舍入当成修复。

必要保持式为：生产者精确输出 y=f(w)，消费者的连接约束为 z=y；执行叶另外接收 d=round(y)，转换记录 e=|d−y|。若先用 d 代替 z，原连接等式和消费者谓词都被替换，原候选证明即不再适用。保存 d 及 e 也不能补救已经改写的语义边。恢复必须从同一精确 y 重验连接，随后重算或核对 d/e，不能从 d 反推 y。

确定接线采用现有表达式与有理算术，不新增求解库或把任意 Rational 引入全部 AMIR 值类型：

1. 私有关系专门化对精确绑定 n/d 使用当前 AST 的规范单位数量 n 除以无量纲 d；既约 d=1 可用原字面量。绝对温度属于仿射量，不能直接除法；分数温度使用 0 K + (n K 温差 / d) 保持绝对温度类型。这个有限 AST 在现有 Core 精确求值中等于原有理数，不要求把 1/3 写成有限小数。生成表达式须有碰撞安全 ID、编译预算及原输入/端口来源映射；源 AMIR 仍保留原始 PortRef。整数/Count 只有满足原类型细化时才能专门化，不用实数除法结果偷换整数声明。
2. 联合见证需保留公共数值输出的精确值和数量声明，用于恢复辅助列、原端口等式与下游关系；该值是源表达式重算得到的派生见证，纳入同一块哈希，不是可单独编辑的源权威。几何/列表等既有输出继续按各自语义封存。恢复必须重算并比较，不能只相信保存的 tagged 值或哈希。当前 outputs 中的执行字面量不能继续兼任这一精确值。
3. 只有跨入现有几何/普通数值执行器的叶参数才调用 deliverRelationBinary64Json。复用其 bits、exact、decimal、absoluteError、numericIdentity；按具体构造输入地址绑定精确表达式值与交付值，并与节点输入一起封存。上溢、非有限、类型细化失败拒绝；下溢和非零误差不能自动获得工程准入。不能只给非终止十进制记录误差，有限十进制 0.3 在 binary64 边界也有误差。
4. 原关系 P 在精确语义图检查，独立执行要求 Q 在实际几何及有依据的误差上检查。转换误差只是参数误差，除非已有构造敏感性界，否则不能冒充几何距离误差；没有相应证明时沿现有要求语义返回 unknown/拒绝，而不放宽需求。

这一单元的完成条件是精确跨节点连接、几何交付、封存、公开读取与免求解恢复共同闭合。固定的一组 1/3 m 相连关系已沿真实原生工具构造实体并提交，公开读取精确端口与毫米交付误差；禁止求解器重开保存相同实现根，修改精确输出并重算块哈希仍被源约束拒绝，伪造零转换误差并重算块哈希仍被 Core 拒绝。这证明已声明的有理构造参数交付路径贯通，不证明一般有理系统都可求解、名义 numericRange 非终止绑定已经可执行或所有几何/物理误差均有传播界。

本次修正前的共同限制已由源码定位：RelationRealizationBlock.variables 的唯一 schema 只允许 number，Core known::bind_candidate 与 verify::check 都用 BigRational::from_float 解释候选，联合恢复也把端口字面量转成 Number。这不是 HiGHS 精度参数问题，而是把数学设计见证限定到了有限 binary64 集合。x=3/10 的定义关系因此不可能由该表示的任何点严格满足；一次失败不证明一般设计无解。更换 LP 算法、增加场景或放宽优化器 tol 均不能改变这个集合包含关系。

7.1 必须保持的两层命题

设源设计的关系谓词为 P，精确设计见证为 w，执行交付为 d，交付方法及误差证据为 E。完整接受必须分别建立：

• P(w)：类型、单位、变量域、law、连接及声明作用于设计数值的要求成立。
• Bridge(w,d,E)：实际执行值确由 w 按锁定方法获得，误差、溢出与单位换算有据可查。
• Q(d,E)：声明作用于执行几何、拓扑或物理分析结果的要求按各自方法成立。

只有三者与共同身份/事务检查都成立才可提交。P(w) 不推出 Q(d,E)，反之也不成立。要求的受检对象由原 assertion 的绑定决定，编译器不得为了成功把几何要求改成名义尺寸要求。若设计只要求名义宽度为 0.3 m，则可以保存精确 3/10 设计值并给几何内核交付带误差证据的浮点量；若要求执行测量在零容差下也精确等于 3/10，则仍须证明该执行要求，不能用设计值代替测量。

7.2 同一封存变量契约

当前未发布契约已将变量见证统一改为有标签的 rational 或 binary64，而不是在 number 字段旁加一个可独立变化的 exactValues 字典。前者携带 §2 的既约 Rat，后者携带 §2 的有限 Binary64.bits；它们都由同一个 Core 解码器得到精确数学值。求解器返回的 binary64 可以直接成为后一种候选，但不能因接近某个十进制就自动变成前一种。源变量单位在编译时归一一次，见证和所有连接使用规范单位，恢复不得二次换算。

candidateHash 绑定有标签的原始见证映射；同一见证用于原关系检查、构造参数求值和 Realization。几何调用的交付值及误差引用该见证，不能反过来覆盖源候选。关系块的 schema/生成 TS/Core 解码、原生查询、联合候选拆分、typed 输出物化、封存读取和免求解恢复必须同批改到这个当前契约；旧 number 表示不留兼容分支。该变更不是只给求解器增加一个返回字段，也不能仅更新 TypeScript 类型后宣称完成。

7.3 精确候选从哪里来

求解器只负责给出近似点和可用的结构信息。精确候选必须由源关系推导或由有界重构获得，再独立检查全部原谓词。对于精确仿射等式 a·x=b 且 a≠0，x=b/a 是唯一可能值；若其它自由变量已选定，则可对相应确定量做同样代入。这是源约束的等价变换，除法及规范化复用现有 num-rational/num-bigint，不通过小数位四舍五入猜设计意图。多个耦合主元需要统一恢复映射和受预算限制的精确线性代数；逐节点各自吸附近似值会破坏连接，不能采用。

有理候选能表达非终止小数，但当前 typed scalar 常量只直接保存有限十进制。从 Rat 到浮点构造输入统一使用 deliverRelationBinary64Json：先精确换算执行单位，再保存 bits、精确二进制有理值、可精确解析回该位型的 decimal 与误差，按 Bridge 与执行要求检查后交付。有限十进制同样经过这一边界，不能免记二进制舍入。整数/Count 必须另外保持整数与非负性；非有理或超越函数结果仍需要包络，不能由有理类型推导为已支持。

7.4 完成界限

这一修改完成的标准是同一源关系经求解/重构、精确验收、显式交付、几何检查、原子提交与免求解恢复贯通；修改后旧见证失效，交付误差不污染设计值。已有 x=0.3 的拒绝记录是现状证据，不是修改成功证据。当前 tagged 见证已替换 number-only 封存实现；下面的已实现范围仍不替代 §6 的其它数值交付与几何退化义务。

当前接线：relation-realization-block 的唯一 schema 定义 rational/binary64 联合，原生结果 schema 引用同一定义；Core witness::decode 为精确候选求值与原谓词检查提供同一个解码器，非既约分数、负零、非有限位型及旧 number 见证均不接受。求解器的原生 number 仅存在于 Worker 候选边界，进入关系求值前统一编码为位型；源字面量由现有数量转换解码，联合恢复不再经过 Number(decimal)。candidateHash、块哈希和原生读取使用相同 tagged 值。旧封存格式不保留兼容路径，当前既有新契约内的恢复仍须成立。

精确传播已进入同一源候选链：reconstruct.rs 从无条件仿射等式构造稀疏关联表，只把含一个剩余非零系数的行 a·x+c=0 化为 x=−c/a，随后从相邻行消去该量；由初始行正确、代入保持等式含义的归纳，所得确定量均来自源法则，不依赖近似点的接近程度。系数合并、除法与位长保护复用已有 BigRational；邻接项随消元访问，队列和算术共用 20,000 工作预算，不枚举赋值。不从条件 law 推导其条件变量，不进行任意稠密主元消元；无法确定的自由变量仍保留原位型。传播结果只称 candidate，矛盾行、变量域、整数约束、目标接受条件和连接等式由原检查器再次检查，不能凭传播成功直接提交。

早期实际原生链已使 x=0.3 m 及下游 y=x 保存为 3/10，沿当时有限十进制物化路径生成实体并提交；禁止 Worker 后重开保持同一实现根。原不可行射线在该新问题上不再通过核验，可行编辑未被缓存误剪。该证据只覆盖精确有限十进制见证，不证明任意有理系统均能重构或 B-Rep 测量精确等于源有理数。当前 §7.0 已接通非终止有理构造参数与转换误差封存；完整几何误差传播及 §7.1 的全部 Q 检查仍不能由 rational 类型或单次纵向核验推定完成。

源确定量还可以在求解前闭合。相同精确传播器接受 null 种子时，从空映射开始，仅录入由无条件等式确定的值；不得为未确定变量填零或默认初值。只有覆盖原变量键全集并通过原精确谓词检查，才进入同一候选/构造链而不创建数值 Worker。若不完整、矛盾、超预算或不满足原域则保留既有求解/诊断路径。该规则由等式代入归纳及完整谓词检查推出，与初值、优化器、产品名称和遍历的成功样本数无关；它不宣称已解决一般线性消元或非线性唯一解识别。候选仍标 unverified，因为代数通过不代替后续几何和事务准入。

7.5 名义范围断言：精确受检对象不能降格为执行字面量

源码已定位出完整阻塞链：relation-ranges.ts::compileRelationRanges 已把固定准则归一为精确闭区间 [minimum−tolerance, maximum+tolerance]，检查 minimum≤maximum 和 tolerance≥0，并交由现有 Core 代数检查器验收。随后 relation-lowering.ts 仍把 requirement.bindings.value 物化为 ConstValue；relation-assertion-projection.ts 将该值写入临时 numericRange；exact-feature-graph-assertion-checker-v0.4.ts 再经 graphNumericValue 转为 binary64 比较。非终止有理值的缺口位于封存与后续检查契约，不在求解算法；增加分母样本或调优化器容差不能修复它。

设固定源准则为 a、b、t，受检设计表达式为 w。名义断言的命题是 a≤b ∧ t≥0 ∧ a−t≤w≤b+t，其中各量按源单位精确归一。几何交付 d 和它的转换误差 E 不出现在该命题中；若源断言检查几何测量，它继续走既有几何检查链，不能被名义 w 替换。因此采用以下唯一接线，不增加第二个有理比较器或借用浮点近似伪造源断言：

1. 关系块的 requirement 数值绑定改为类型/规范单位/精确 value 与编译后的精确 lower、upper，仍绑定 sourceAssertionHash。同一选中候选经 compileRelationRanges 生成这些值；没有精确范围时保持 pending，不默认为通过。生成的边界是派生见证，不能由调用者独立指定。
2. 执行投影把名义绑定要求保留为显式的精确断言集合，与实际几何断言共同进入现有断言检查入口。不能把占位数值写成一个看似正常的 numericRange，也不能删除要求后只返回一个先前保存的 pass。未绑定或显式 preserved 的源断言仍独立保留；同一源断言被多个关系绑定时，各绑定均须独立检查。
3. 现有入口对精确断言调用同一个 Core verifyRelationLinearJson，以无待求变量的精确 range 问题核验，不启动求解器。报告包含源断言/关系身份、精确受检值和边界、规范单位、检查问题身份与执行身份；不能把这些精确值强制塞进现有 number 报告字段。名义检查与测量检查必须在公开报告中可区分。
4. 恢复从当前源准则和选中候选重新 compileRelationRanges、重建整个块，再进行上述独立检查。修改 a/b/t、参数或表达式须改变来源或块身份；只重算篡改块的哈希不能使伪造范围获得准入。

该项验收义务为：同一非终止设计值落在声明范围内可交付，范围外拒绝且头修订不变，恢复不调用求解器，伪造边界或更改源准则不能复用旧检查。范围包含关系与身份保持是验收对象，不展开工业场景枚举。当前接线已完成：requirement.bindings.value 保存 RelationExactRange，lowering 复用 compileRelationRanges；共享断言入口和历史证据读取均复用 checkExactRelationRange → Core，读取另外检查报告集合完整性。公开报告用 evidenceLevel=exact-design-value 区别名义值检查，同一源断言被不同关系绑定时以关系/断言二元身份分别验收。实际原生工具的两个相连 1/3 m 值在 [0.3,0.4] m 内提交并各产生精确报告；范围外编辑拒绝且头保持，伪造上界并重哈希仍被源重算拒绝，禁止求解器重开保持实现根。该验收停止，不推定一般几何/物理误差传播已完成。