feat(higher): normalize marked pair cells

[miuchan]

Summary

• prove generic normalization formulas between an empty word and any closed two-atomic-step word
• use unitor equality and right-whiskering semantics to identify both directions exactly
• specialize the formulas to marked unit, inverse unit, counit, and inverse counit
• prove all four marked generators normalize exactly to their executable pair insertion/deletion refinements
• remove the four marked fields from StructuralGeneratorNormalizable, reducing the remaining basis from ten fields to six
• extend the cost-exact normalization core and synchronize audits and four-language boundaries

Verification

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

Boundary

Six unconditional structural normalization fields remain: associator and inverse, plus left/right unitors and inverses. All-cell normalization, semantic fullness, critical-pair coherence, reduced-hammock invariance, standard weak-equivalence packaging, and the final Dwyer--Kan/Rezk theorem remain open.