Lin's density theorem in the vocabulary of Statement.lean
(audit node 1.1.1): the standalone file's own TracialDensityHypothesis is
a theorem, transferred from CommutingRepetition.Density.tracialDensity
(stage E7 of the density programme) through the field-by-field identification
of the two copies of StdTracialAlgebra and
TraciallyEmbeddableCorrelation. This is why UniformParallelRepetition
below carries no hypothesis.
The development proves the standalone statement of Statement.lean.