The finite Schur test for the Euclidean operator norm

The general Lean4LPD Schur-test API is provided by LeanPool.LowWeightPauliDynamics.SchurCore, also exported through BlockNorm. This entry preserves the original imports and declaration names for Pauli-dynamics users while sharing one proof with the block/spectral-sensitivity project.