The ℓ¹ estimate from an entrywise estimate

theorem CommutingRepetition.Density.l1Dist_le_of_forall {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (p r : Correlation X Y A B) {C : ℝ} (h : ∀ (x : X) (y : Y) (a : A) (b : B), |p x y a b - r x y a b| ≤ C) : l1Dist p r ≤ C * (↑(Fintype.card X) * ↑(Fintype.card Y) * ↑(Fintype.card A) * ↑(Fintype.card B))

The standard-form step

theorem CommutingRepetition.Density.abs_corr_sub_stdOf_le {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (S : CommutingStrategy X Y A B) [TopologicalSpace.SeparableSpace S.H] [Nonempty S.H] {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) (x : X) (y : Y) (a : A) (b : B) : |S.correlation x y a b - (stdOf S hε0 hε1).corr x y a b| ≤ 2 * ε / (1 - ε)

Lin's density theorem

theorem CommutingRepetition.Density.tracialDensity : TracialDensityHypothesis

Stage E7 / audit node 1.1.1: Lin's tracial density theorem. Every commuting-operator correlation on common finite alphabets is an ℓ¹-limit of tracially embeddable correlations.