feat(higher): prove hammock normalization naturality

[miuchan]

Summary

• expose exact atom, empty, and binary-append equations for linear normalization
• prove append-isomorphism naturality around arbitrary left- and right-whiskered quotient 2-cells by exchange and cancellation
• prove normalized semantics commutes with raw left and right whiskering
• normalize raw source-identity and inverse generators using unitor equality, and prove equality transport preserves normalizability
• close the identity, original, source-identity, vertical-composition, both-whiskering, and transport induction branches
• define StructuralGeneratorNormalizable with exactly twelve remaining structural obligations and prove it implies normalization of every raw cell
• expose a cost-exact machine-facing normalization core and synchronize audits and four-language boundaries

Verification

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

Boundary

The all-cell induction theorem is conditional on twelve explicit, still-unproved structural generator fields: source composition and inverse, marked unit/counit and inverses, associator and inverse, and left/right unitors and inverses. No unconditional fullness or complete normalization claim is made. Semantic fullness, critical-pair coherence, reduced-hammock invariance, standard weak-equivalence packaging, and the final Dwyer--Kan/Rezk theorem remain open.