# RootCover 数值语义与边界

## 数学对象

给定 n∈1…6 的方形多项式方程组 f:Rⁿ→Rⁿ 和有限闭初始盒 X。目标是分类 X 内的实根区域，不处理 X 外的根。名称是唯一ASCII标识符。表达式总节点≤512，语法深度≤32；单次整数幂0…16，总次数≤32。只允许 +、-、*、非负整数幂；不支持函数调用、隐式乘法、除法或方程等号，输入表达式均表示“=0”。-x^2 解释为 -(x^2)。

系数、十进制字面量及边界首先转换为binary64点值。后续区间包含的是这些点值定义的实多项式，而不是任意精确十进制原文或系数不确定族。初始区间可退化，但严格内部认证可能因此不可用。

## 算术与导数

每个加、减、乘操作用相邻binary64值向外扩张，整数幂利用偶次幂非负性收紧下界。NaN中间结果退化为整个实轴，溢出产生保守无界区间；不能因此排除根。公开区间运算要求合法有序非NaN区间，所有求解入口再次校验输入。区间前向自动微分对同一表达式计算自然区间值与Jacobian包围。

包围依赖二进制浮点正确舍入、渐进下溢、无fast-math重新结合。默认编译目标使用普通浮点操作；测试包括次正规数和溢出。没有宣称符合IEEE1788全部装饰语义、任意精度或已由证明器证明。

## Krawczyk 判定

取盒内binary64中心m，数值近似Jacobian的浮点逆Y只作为预条件矩阵；它无需等于真实逆。用区间运算计算 B=I−YJ(X) 和 K=m−Yf(m)+B(X−m)，其中f(m)也用区间运算，不以一个四舍五入点残差代替。

1. 任一方程区间不含0，则该盒无根。
2. X与K任一坐标无交集，则该盒无根。
3. K严格位于X内部，且 ||B||∞ 的向上舍入界q<1，才认证X中存在且仅存在一个根。其根位于X∩K；原始域、中心、Y、K、q对外提供。
4. 其他情况下，足够收缩则继续处理X∩K；否则划分或保留未决。预条件器失败不是无根证明。

认证后最多12次额外Krawczyk精化收紧包围，仍受全局评估预算约束。返回的最终包围由这些保根收缩产生；序列化certificate记录原始唯一性域和证明参数。独立有理数oracle重算该域的判定；解析已知根测试另外核对最终包围。没有宣称只凭导出的单份certificate便可重放全部后续精化历史。

## 区域覆盖、完成与精度

栈式处理保留未处理盒。分割使用确定性非对称位置，左右闭盒在接口处重合，联合覆盖原盒；它减少对称根恰好处于接口的情况，但不保证永远避免。严格认证域的根处于其内部，不能因为接口重合重复计算同一个已认证根。收缩丢弃的区域没有该盒中的其他根。

`complete=true` 当且仅当没有未决盒，表示初始区域中所有可能根均位于已认证的唯一解域，且每域只有一个。此时root_count可作为区域内不同实根数。否则root_count只是已认证根数；未决盒可能有0、1、多根或非孤立根。

`tolerance_met` 只检查已认证根包围的最大坐标宽度。没有已认证根时它可能为true，绝不覆盖complete=false。预算用尽时已经认证的根可以保留，同时把所有待处理盒输出为未决。深度、容差和无法找到可表示内部划分点也会产生未决。

单次最大20000次区域评估、搜索深度80；默认4096次、深度60、绝对宽度容差1e-8。每个评估成本受6维/512节点约束，但大任务仍可能昂贵；宿主可用独立进程或Worker终止。没有全国/工业无限规模的性能保证。

## 测试不是数学全覆盖

Python Fraction oracle独立实现精确有理数区间、AST解释和导数，不复用MoonBit求解/舍入/逆矩阵代码。有限的解析模型和证据重放提供错误发现能力，并不是对整个实现的形式化证明。真实实验数据、条件数和缩放敏感性仍需后续系统研究。