ColumnTraceTotal.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

All four contributions to the literal centered trace on a single column/padding catalog, with the full external dimension allowance retained.

theorem OAI.TwoPointCorrelations.eventually_prohibited_column_trace_total line 17