refactor(Logic/Modal): register pass — refinement class is le, doc fixes

[hawkrobe]

Register and API pass on Modal/Defs.lean, following an architecture check against mathlib, plus consumer-driven refinements.

• IsBeliefRefinementOf deleted (it was the pointwise Rb ≤ Rk); IsSerial.serial is now Relator.LeftTotal R (the IsWellFounded.wf pattern); three redundant ⊤-instances deleted (derivable from Refl + Euclidean via the file's own implication chain); instance priorities dropped (Lean 4 tabled resolution handles the cyclic derivations; Prop-class selection is proof-irrelevant).
• Scoped □[R]/◇[R] notation (mathlib ~[R] style, partially-applied so ordinary application gives □[R] p w); duality restated in push-negation normal form as @[simp] not_box/not_diamond with one-line simp proofs, replacing the hand-rolled classical terms (sole consumer's textbook duality now derives in two lines); operators lead the file, title corrected to "Modal operators and frame conditions" (the file no longer defines accessibility relations).
• Docstrings are definition-form one-liners; section headers bare; variable-lifted binders with the (R)/{R} flip.

Checked, not changed: Std.Refl R/IsTrans W R mixed arity is mathlib's current register (IsRefl deprecated in favor of Std.Refl, 2026-01-08).