Lean: operator matrices on PiLp 2 (fun _ : ι => H) — entry calculus that scales

For 2x2 dilation arguments (Kaplansky, bicommutant amplification) define entry R i j := PiLp.proj 2 _ i ∘L R ∘L singleCLM j and prove once: ext_entry (operators equal iff entries equal, via (R v) i = ∑ j entry R i j (v j)), entry_mul (sum formula), entry_star (adjoint of transposed entry, via a helper ⟪single i u, v⟫ = ⟪u, v i⟫), and closed forms for entry (R * E_kl), entry (E_kl * R), entry (ampl a * R) (= a * entry R i j, rfl). With these, commutant computations such as M_n(A)' = ampl(A') become two-line rewrites instead of sum manipulations. Gotchas: PiLp.single_eq_of_ne takes p explicitly (PiLp.single_eq_of_ne 2 h); PiLp.norm_apply_le can time out unless the vector is first set with an explicit PiLp type; annotate singleCLM (0 : Fin 2), or + on the resulting CLMs fails with a stuck HAdd instance.