Evidence for the proportional dissociation of the roots of unity

../

verify/: Whole-statement fidelity audits of Erdos.L21.statement against the L21 card's prose statement, one folder per audited source, with their grades and the non-author clean gate of each promotion, and the two non-author clean gates of 2026-10-13, the later on Lean v4.34.1.

---

The verification records under verify/ assess the exact formal statement of L21 against its prose statement as it stood on a named date. A fidelity audit filed there compares the two texts and states its verdict, its distinct grade asserts the tier, and the non-author clean-gate receipt filed beside them, with the gate's captured log and the runner's wrapper, puts the tier in force at the promotion that cites the grade together with it; neither the audit nor the grade by itself establishes a kernel gate or promotes the claim. The first record, for the source of 2026-09-28, holds all three, its clean gate being one run serving the five claims whose records name that source. The folder verify/clean_gate_2/ holds no fidelity audit: it is 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, to whose tree the card's standing binds the warrant, with a grade decision that applied the grade to that tree. The folder verify/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.