查看并独立重放证书[#85]

derivation steps: 10

replay valid: #t

math-report-derivation取出证书；math-verify-derivation使用规则目录重新检查证书中的每条边。验证使用证书自己的假设快照，因此不要求原来的动态假设作用域仍然打开。

求导audit中的contract层就是多项式递归契约检查。检查器沿着原始表达式树递归：常数与变量是基例，加减、乘法、常数除法和自然数幂分别使用对应的递归契约。它把独立构造的结构证据与实际求导证书的终值比较：

certificate check: semantically-checked; structural cases present (power, product, sum): ((natural-power coordinate product constant coordinate) (product constant coordinate) (sum natural-power coordinate product constant coordinate)); wrong result: rejected; diagnostic: ("the supplied result differs from the exact polynomial derivative")

这次检查覆盖有理系数标量多项式：常数、变量、加减、乘法、常数除法和自然数幂。它直接检查实际运行的求导证书，并以独立递归语义计算预期导数。错误结果会被标为rejected，诊断说明终值与精确多项式导数不一致。这里的归纳由Grove检查器执行；它不是对Guile/Scheme实现本身的机器证明，也不覆盖多项式域之外的函数求导。

这里的subject是Contract Evidence IR的math-derivative-evidence记录。每个节点显式保存当前规则分支、原表达式、求导坐标、该子表达式的精确多项式结果和子节点。例如和式节点必须有左右两个有效子证据，且结果必须是两边导数之和；乘积节点还会独立解释两个操作数并检查乘积法则。验证器递归重算每一节点，而不是信任生成证据的过程。公开的记录字段也让文章可以直接按结构查询case，而不用把记录打印成字符串再搜索名称。

积分的验证还可以检查算法如何处理每个单项式。对于c*x^n，积分规则将幂次加一，并把系数除以新的幂次。检查器把实际antiderivative pass的证书与这些逐项契约比较，再检查原点归一化和求导恢复输入：

primitive: (+ (* (/ (num "1") (num "4")) (^ (var x) (num "4"))) (^ (var x) (num "2"))); replay: #t; contract: semantically-checked; Proof IR: unsupported (("rule has no fixed RuleSpec to elaborate")); per-term evidence: 2; bad constant: rejected; diagnostic: ("the primitive is not normalized to zero at the coordinate origin")

当前积分器选取在坐标原点取零的多项式原函数，因此这里验证的是Grove规定的规范结果；若要表示其他积分常数，那会是另一个结果契约。上面的错误例子导数仍然正确，但不满足原点归一化，所以检查器会拒绝它。

积分的Contract Evidence IR以每个规范输入单项式为一条记录，保存输入项与声称的输出项。独立检查器重新算出积分坐标的原幂次、加一后的幂次和除以新幂次的系数，再确认没有遗漏或多出输入项、这些输出组成了报告中的原函数，并且对积分坐标求导后恢复原多项式。原点归一化是单独检查的条件，因此错误常数有明确的归一化诊断。