feat(Core): instantiate holds & LindstromQuantifier as mathlib homs

[hawkrobe]

Bundle two bespoke holds : _ → Set _ maps as mathlib homomorphisms, plus a mathlib-idiom pass on a Tense file.

• Core.Order.holds becomes a BoundedLatticeHom (holdsHom); the named comparison categories become joins of the three atoms (notAfter = before ⊔ overlapping, …); new Core/Order/Opposition.lean proves they form an Aristotelian square; Tense.nonpast = present ⊔ future.
• LindstromQuantifier gains a BooleanAlgebra instance (compl/inf/sup collapse to ᶜ/⊓/⊔, plus ⊤/⊥) and holdsHom — the Lindström analogue of Core.Order.holdsHom.
• Semantics/Tense/DeRe.lean: IsFelicitousWith/IsAbuschFelicitous casing, theorem-name fix, docstring path/claim fidelity (+ Abusch1997/HeimComments consumers).