# A correction that improved the verification record

The original finite checker began after an integral had already been simplified. A later checker began with the literal four-variable integral quoted in the proof. That added a separate finite check of the reduction, while the written argument remained responsible for the all-orders claim.

Review caught two implementation issues in the first revision of the later checker: one sign-condition comparison used floating-point complex arithmetic, and reported mismatches did not cause a failing process exit. The correction used integer real and imaginary coordinates and made mismatches return failure. The [recorded source diff](verification-correction.patch) shows those changes.

The coordinator had replayed all 1,036 ordered even-total cases through degree 12 on the original revision. It then inspected the changed functions, compared the corrected integer condition on all 1,036 inputs, and injected a mismatch to check the failure path. This is a full earlier replay plus a bounded review of the correction; it is not presented as a second full coordinator replay of the corrected program.

A separate verification reviewer checked a smaller source-integral range and additional odd cases. That review did not itself replay the full degree-12 set. Likewise, the checker printed normalization and an odd-degree example; those diagnostic prints alone were not automated assertions of a general odd-degree result.

The same review process narrowed descriptions of the Lean results. The existing character theorem summed over all sixteen sign choices, while the analytic argument needed the eight with product one. A subsequent worker was assigned that exact missing identity, and the coordinator freshly rebuilt it and a separate restatement. The new identity closes that specific gap; the full analytic theorem remains outside Lean.

These distinctions matter because a successful command, a finite calculation, an AI review and a Lean theorem support different claims. This account is drawn from the retained verification supplement and correction commit, not an invented conversation or a claim of faster research.
