Add terminating generated hammock reductions

[miuchan]

Summary

• add executable raw-path metrics nodeCount, leftWeight, and their scalar reduction complexity
• define a directed administrative reduction with vertical unit elimination, right association, adjacent refinement/aligned/common-prefix fusion, executable refinement inverse cancellation, and closure under every generated path context
• prove every elementary step weakly lowers both structural measures, strictly lowers at least one, and therefore strictly lowers complexity
• prove well-founded termination, existence of irreducible reducts, and exact quotient-semantic preservation for one-step and arbitrary finite reductions
• define critical pairs and joinability; prove competing one-step moves are semantically coherent while keeping raw joinability/local confluence explicitly open
• expose the reduction through the cost-exact mapping core and update audits and four-language research status

Verification

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

Remaining boundary

This is the first terminating administrative layer, not the complete classical reduced arbitrary-grid hammock system. Raw critical-pair joinability/local confluence, the remaining grid moves, reduced-hammock homotopical invariance, standard weak-equivalence packaging, and the final global complete-Segal/Rezk theorem remain open.