feat(higher): normalize hammock path whiskering

[miuchan]

Summary

• add canonical left and right whiskering of generated hammock paths through linear-normal-form append isomorphisms
• add horizontal path append and prove semantic equality and exact-image membership closed under whiskering, append, and vertical composition
• define normalized semantics for arbitrary raw presented cells
• prove identity and original raw cells normalizable and vertical composition preserves normalizability
• expose exact cost-exact three-model nerve formulas for left whiskering, right whiskering, and horizontal append
• audit the expanded noncomputable semantic boundary and synchronize research and four-language status docs

Verification

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

Boundary

The raw Cell normalization induction is complete for identities, vertical composition, and original source 2-cells. Normalization-isomorphism naturality for raw left/right whiskering is still required before the remaining structural generators and all presented quotient 2-cells can be normalized. Fullness, critical-pair coherence, reduced-hammock invariance, standard weak-equivalence packaging, and the final Dwyer--Kan/Rezk theorem remain open.