refactor(Modal): Hilbert-style primitives for modal propositions

Refactor the modal `Proposition` inductive to the `{atom, bot, imp, box}`
primitive basis: falsum and implication as the primitive propositional
connectives, box as the primitive modality. Negation, conjunction,
disjunction, verum, possibility, and biconditional become derived connectives
via the `Cslib.Foundations.Logic.Connectives` interface introduced in #635;
`Proposition` is registered as a `ModalConnectives` instance.

- Replace `not`/`and`/`diamond` constructors with `bot`/`imp`/`box`; derived
  connectives are `abbrev`s, enabling definitional unfolding.
- Rewrite `Satisfies` on the new primitives and add explicit characterisation
  lemmas (`neg_iff`, `diamond_iff`, `and_iff`, `or_iff`, `iff_iff_iff`).
- Replace all `grind`-based axiom-validity proofs (K, dual, T, B, 4, 5, D and
  their frame-correspondence converses) with explicit term-mode proofs.
- Update `Denotation.lean` for the new primitives with explicit proofs.
- Rework `LogicalEquivalence.lean`: a one-hole `Proposition.Context` and a
  direct `LogicallyEquivalent`/`congruence`, in place of instantiating the
  shared `LogicalEquivalence` typeclass (rationale in the file's Design Notes).
- Add `#grind_lint skip` entries for the derived-connective characterisations
  whose `@[scoped grind =]` annotations have long instantiation chains.

Stacked on #635 (propositional primitives); review/merge that first.

Author: benbrastmckie