Evidence for the analytic Sidon property of the roots of unity

../

verify/: The independent statement-fidelity audit of L20 as it stood on 2026-09-28, its distinct grade and the non-author clean gate of 2026-09-29 for the kernel-only promotion, and the two non-author clean gates of 2026-10-13, the later on Lean v4.34.1.

---

The verification records assess the exact formal statement of L20. Three records are filed. The first, statement_fidelity/, holds an independent whole-statement fidelity audit of Erdos.L20.statement against the card's prose statement as it stood on 2026-09-28, the distinct grade that asserts the tier, and the non-author clean-gate receipt with the gate's captured log and the runner's wrapper. An audit and its grade do not by themselves establish a kernel gate or promote the claim; the grade's assertion is in force from the promotion that cites it together with the clean gate, one run of which serves the five claims whose records name that source. The second, clean_gate_2/, holds the non-author clean gate of 2026-10-13 over the whole lean/ tree of the change that ported the Lean modules of L20, L21 and L22 to Lean v4.34.1, as committed at 2026-10-13T19:38:30Z, one run serving L20, L21 and L22, with its receipt, captured log and wrapper; it holds no fidelity audit, and the card's standing binds the warrant to the tree it checked, with a grade decision that applied the grade to that tree. The third, clean_gate/, holds the earlier non-author clean gate of 2026-10-13 over the whole lean/ tree as it stood on 2026-10-13T04:56:43Z, on Lean v4.32.0-rc1, one run serving L17, L20, L21 and L22, with its receipt, captured log and wrapper.