feat(higher): add aligned hammock path category

[miuchan]

Summary

• add a non-groupoidal generated hammock-path syntax combining executable refinements, arbitrary aligned raw 2-cells, and vertical composition
• quotient paths by exact presented 2-cell semantics and prove the semantic functor faithful and object-essentially-surjective
• embed refinement-only paths faithfully, with strict semantic and nerve factorizations
• give every source 2-cell a canonical one-column representative and prove its right-unitor-conjugated quotient formula
• expose exact cost-exact nerve actions for refinement, aligned, and source 2-cell edges
• audit the new declarations and synchronize research boundaries and four-language status docs

Verification

• lake build Ript.ForMathlib.CategoryTheory.Bicategory.MarkedZigzagAlignedHammock
• lake build Ript.Higher.CostExactZigzagMappingSpace
• lake build Ript.Audit.Lint
• ./scripts/check-axioms.sh
• ./scripts/quality-gate.sh

Boundary

This PR covers arbitrary aligned cells and every source 2-cell in canonical one-column form. It does not yet normalize every presented quotient 2-cell into alternating aligned/refinement paths, so fullness into the complete linear mapping category, critical-pair coherence, reduced-hammock invariance, standard weak-equivalence packaging, and the final Dwyer--Kan/Rezk theorem remain open.