---

This proves the entire statement of L21 by machine-checked Lean, at tier 2 for the Lean sources of 2026-09-28 that the card's standing names; the Lean proof map lists the modules stage by stage. The formal entry point is Erdos.Research.Problem774.rootsOfUnity_proportionalDissociation in lean/Erdos/RootsOfUnitySidon/RootsOfUnitySidonComplete.lean, which applies statement_of_analyticSidon_of_pisier to the analytic Sidon theorem (the subject of L20) and to the finite Pisier implication PisierForwardComplete.pisierForward. That implication is proved in the same folder: given a Sidon constant and a finite set of frequencies, finite interpolation and Khintchine's inequality bound the even moments of the real character sum (FiniteSidonInterpolation.lean, FiniteKhintchine.lean), one finite character sample captures all moments through the needed order (FiniteOrthogonalCharacters.lean, FiniteMomentOrthogonality.lean), a Riesz-product average bounds the weighted count of signed relations (FiniteRieszMomentBound.lean, PisierRelationCounting.lean), and two counting lemmas select a proportional relation-free subset (PisierFixedSizeThinning.lean, PisierThinningAssembly.lean). The definitions rootsOfUnity, UniformExtraction and statement live in RootsOfUnitySidon.lean.