feat(higher): characterize refinement semantic image

[miuchan]

Summary

• define the exact refinement-generated quotient-2-cell image as a subgroupoid of the linear hammock mapping category
• prove semantic refinement paths are full, faithful, essentially surjective, and categorically equivalent onto that image
• lift the equivalence to a nerve equivalence with an explicit simplicial homotopy inverse and strict semantic factorization
• audit the new flagship declarations and synchronize the blueprint, conjecture boundary, model matrix, and four-language status docs

Verification

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

Boundary

This PR characterizes the exact image of executable refinements. It does not prove that this image covers every quotient 2-cell required by a standard derived/hammock mapping-space model; critical-pair coherence, reduced-hammock invariance, weak-equivalence packaging, and the final Dwyer--Kan/Rezk theorem remain open.