Row–column symmetry and contraction of coordinate sweeps

Formalization

• OpenAI math release, Lean scope notes for family 238 (lean/docs/238.md, 2026). States that the formalization covers the weighted Schatten-moment bound giving sweep operator norm at most D^{-c} (WeightedSweepMoments.lean) and the row–column overlap estimate on occupied boards (OccupiedOverlap.lean); the full mixing conclusion is outside the scope. [family-level]
• punk01-shaka, OpenAI's Comparator configs leave 62 fully-written definitions unchecked (definition holes) (GitHub issue, 12 Oct 2026). Lists the OccupiedOverlap comparator config of family 238 as leaving 5 of 5 definitions as holes, so the automated check alone would not fix those definitions. [family-level]

Possibly relevant literature (found by the agent, not checked)

• Y. Jiang, A subquadratic upper bound for the mixing time of the Thorp shuffle (arXiv:2610.18884, 3 Oct 2026). Independent preprint proving a full-deck bound of order d^{5/3} for N=2^d; relevant for comparison with this paper's Θ(log N) claim. It does not mention the release. [family-level]

Digests and expositions

• Latent Seminar, Optimal logarithmic mixing of the Thorp shuffle (expository notes, 2026-10-06). Outlines all twelve manuscripts’ proof methods and formalization boundaries, explicitly disclaiming independent full-proof verification. [family-level]
• heyprof, Thorp shuffle: how often until the deck is random? (interactive exposition, undated). Illustrates the family’s full-deck mixing question with small-deck distributions, single-card marginals, and the support bound. [family-level]