cleanup: golf summable_prod_of_norm_coeff_le_linear

[CBirkbeck]

Target: summable_prod_of_norm_coeff_le_linear — projects/PadicLFunctions/PadicLFunctions/MeasureR/FormalPsi.lean:887 (sorry-free, ~50-line proof, on main).

Action: /cleanup (single-declaration): golf the proof + mathlib-search for shortcuts. Statement unchanged.

Acceptance: lake build PadicLFunctions green · zero new sorry · #print axioms summable_prod_of_norm_coeff_le_linear unchanged · statement byte-for-byte unchanged.

[CBirkbeck]

claimed

[CBirkbeck]

Superseded by file-level cleanup tickets (whole-file granularity).

[CBirkbeck]

Done via #264 (squash-merged). Acceptance bar green: lake build PadicLFunctions ✓, zero new sorry, #print axioms = [propext, Classical.choice, Quot.sound], statement byte-for-byte unchanged. Golf: gcongr for the hbd calc, by_contra!, inlined hn, dropped exfalso, stripped narrative comments. Body 40→33 lines.