Normalize right unitor hammock cells

[miuchan]

Summary

• extend generated hammock paths with common-prefix lifting and recursive terminal-empty-row deletion/insertion paths
• prove exact quotient semantics for both right-unit paths, their inverse law, and normalized raw right unitor/inverse formulas
• reduce StructuralGeneratorNormalizable from four fields to the two remaining associator directions and expose the completed cases in the cost-exact normalization core
• update the axiom audit, blueprint, model matrix, conjecture boundary, and four-language research status

Verification

• lake build Ript.ForMathlib.CategoryTheory.Bicategory.MarkedZigzagAlignedHammock
• lake build Ript.Higher.CostExactZigzagMappingSpace
• ./scripts/quality-gate.sh (3664 build targets, lint, executable examples, and axiom allowlist all passed)

Remaining boundary

This does not prove unconditional normalization of every raw cell. The associator and inverse associator generator cases remain open, followed by semantic fullness, critical-pair coherence, reduced-hammock invariance, standard weak-equivalence packaging, and the final Dwyer--Kan/Rezk comparison.