Independent reproduction of a Lean factoring certificate: Rudich and Rousseau, "Deterministic Factoring in Time N^{o(1)}", what the machines checked and what they did not

A reproducibility record for the Lean 4 certificate accompanying I. Rudich and L.-M. Rousseau, "Deterministic Factoring in Time N^{o(1)}" (Hexagon 2610.00600v1, 29 October 2026). The note separates two claims of different strength. [Machine-checked] The certificate for Factoring.subexponentialRate (project commit c91cc3f) was rebuilt in two environments, one with bubblewrap sandboxing; lake comparator --paranoid returned exit code 0, all six checker runs (Lean kernel in two modes, lean4lean, nanoda, con-leche, con-ron) accepted it, and the proof depends only on the three permitted axioms. [Model judgement] Two separately prompted AI instances found no mismatch between the 13-line formal statement and the stated result; this is not a human certification. The note does not claim that the result is correct as mathematics or that the formal statement means what the English title says. It ends with four specific questions for human readers about the Mathlib definitions the statement relies on. Disclosure: according to the authors, the ideas and Lean proof were generated by Claude Opus 5.5 (Anthropic). Parts of this reproduction and note were carried out with AI instances, including Claude. The checker results are recorded in the two attached evidence archives so that anyone can repeat them. Files: the note (PDF), its LaTeX source, and two evidence archives with logs and SHA-256 checksums.