feat(Logic/Modal/BSML): Hintikka formulas; expressive completeness proved

[hawkrobe]

Builds the Hintikka machinery and uses it to discharge the library's expressiveCompleteness_converse sorry, making Logic/Modal/ sorry-free.

• charFormula M k w (depth-k Hintikka formula: atomic type ∧ ◇ of each successor type ∧ □ of the successor-type disjunction) with the two-directional characterisation classicalEval_charFormula_iff_bisim : … ↔ WorldBisim k M w M v, plus the singleton-support lift and supporting falsum/bigDisj/team-support API.
• expressiveCompleteness_converse: every convex, union-closed, bounded-bisimulation-closed team property is BSML-definable (within-model finite-atom form of Anttila 2025 Ch 3 — the cross-model theorem indexes bisimulation by finite atom sets, so [Fintype Atom] is the honest hypothesis). The defining formula is δ_U ∧ ⋀_{T ∈ 𝒯} ((δ_T ∧ NE) ∨ δ_U) over flat characteristic disjunctions, with U the union of P's teams and 𝒯 the transversal world-sets; a supporting team's uncovered-worlds set fails transversality, yielding s₀ ∈ P covered by t, and s₀ ∪ (U ∩ cover t) closes via convexity + bisim-closure.
• expressivelyComplete — the headline theorem — is now fully proved.