feat(higher): normalize left unitor cells

[miuchan]

Summary

• prove computable right-unit and associativity equations for linear-row append
• add generated equality paths for propositionally equal linear rows
• prove presented raw-cell relations preserve normalized semantics
• prove arbitrary-iso left-unitor conjugation and its inverse cancellation
• normalize raw left unitor and inverse exactly to the identity path
• remove both left-unitor fields from StructuralGeneratorNormalizable, reducing the remaining basis from six fields to four
• 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

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