cleanup: golf padicLog_mul_of_norm_lt_one

[CBirkbeck]

Target: padicLog_mul_of_norm_lt_one — projects/PadicLFunctions/PadicLFunctions/ValuesAtOne.lean:551 (~43-line proof, on main).

Action: Run /cleanup on this declaration (single-declaration mode): golf the proof, apply mathlib style, search mathlib for anything that shortens it. Do not change the statement.

Acceptance (the green bar): lake build PadicLFunctions green · zero new sorry · #print axioms padicLog_mul_of_norm_lt_one shows only propext/Classical.choice/Quot.sound · statement byte-for-byte unchanged.

(First smoke-test ticket for the worker pipeline.)

[CBirkbeck]

claimed

[CBirkbeck]

Done — golfed via #4 (squash-merged to main as 172515c).

Acceptance bar (all green):

• lake build PadicLFunctions ✓ (3923 jobs, no new warnings)
• zero new sorry in ValuesAtOne.lean ✓
• #print axioms PadicLFunctions.MeasureR.padicLog_mul_of_norm_lt_one → [propext, Classical.choice, Quot.sound] ✓
• statement byte-for-byte unchanged ✓

Golf: removed dead exp-ball witness (hbxy/jxy were defined but never used — hkey only needs hbx,hby via padicLog_mul), collapsing N := max (max jx jy) jxy → max jx jy; golfed the ‖x*y-1‖<1 ultrametric bound; inlined hpN; stripped narrative comments. Proof body 37 → 27 lines.