Three raw font-size values need a design call before tokenising

[ElbertePlinio]

The design system says never to type a raw font-size, but three exist:

• src/screens/workbench/workbench.css:1716 — font-size: 13px
• src/screens/workbench/workbench.css:2185 — font-size: 9px
• src/screens/workbench/workbench.css:3407 — font-size: 9.5px

Deliberately left out of the easing gate in #353. Unlike easing, this is not mechanical: the nearest --pf-size-* token may not equal the current value, so tokenising changes rendering in dense workbench chrome where 9px vs 9.5px was likely deliberate.

Note border-radius was considered and rejected as a gate: of seven raw uses, most are legitimate geometry (0, 1px, 2px 0 0 2px bracket shapes), so a blanket rule would produce false positives.

Scope

• Decide per value: map to the nearest token and accept the visual delta, add a token, or document the exception
• Only after that, consider extending the gate to font-size

Refs #353