feat(higher): normalize source composition cells

[miuchan]

Summary

• expose singleton append comparison formulas and their explicit inverses
• prove the pure bicategorical coherence formula for normalization of two atomic steps
• identify the hom and inverse of two-atom normalization as right-unitor/associator composites
• prove raw source composition and inverse normalize exactly to executable forward expansion and contraction
• remove sourceComp and sourceCompInv from StructuralGeneratorNormalizable, reducing the remaining basis from twelve fields to ten
• extend the cost-exact raw-cell 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

Ten unconditional structural normalization fields remain: marked unit/counit and inverses, associator and inverse, and 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.