refactor(Modal): Lukasiewicz primitive convention for modal propositions

Refactors Modal/Basic.lean from {atom, not, and, diamond} primitives to
{atom, bot, imp, box}, following the Lukasiewicz convention. Derived
connectives (neg, and, or, top, diamond, iff) defined as abbrevs.
All grind-based proofs replaced with explicit term-mode proofs.
Denotation.lean and LogicalEquivalence.lean updated for new primitives.
LogicalEquivalence typeclass fully instantiated following HML pattern.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: benbrastmckie