Evidence for the near-logarithmic dissociation bound

../

verify/: The independent statement-fidelity audit of L22 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 under verify/ assess the exact formal statement of L22. Three records are filed. The first, statement_fidelity/, holds the independent whole-statement fidelity audit of Erdos.L22.statement against the card's prose statement as it stood on 2026-09-28, verdict PASS, 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 by themselves establish no kernel gate and promote no 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. 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.