feat(higher): normalize hammock path whiskering

AXIOMS.md

@@ -970,15 +970,29 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.lean`.
 | `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_essSurj` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
 | `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
 | `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.semanticFunctor_factorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
-| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_vcomp` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
-| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.semanticFunctor_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
-| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinementFunctor_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_vcomp` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.semanticFunctor_faithful` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinementFunctor_faithful` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
 | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinementSemanticFunctor_factorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
-| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.inSemanticImage_iff_exists_map` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
-| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinement_mem_semanticImage` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
-| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.aligned_mem_semanticImage` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.inSemanticImage_iff_exists_map` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinement_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.aligned_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
 | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.originalAlignedCell_toHom` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
-| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.originalCell_mem_semanticImage` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.originalCell_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedWhiskerLeftHom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedWhiskerRightHom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_whiskerLeft` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_whiskerRight` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_append` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerLeft_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerRight_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.append_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_id` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_vcomp` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_original` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.identity_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.vcomp_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.original_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
 | `Ript.Higher.CostExactZigzagMappingSpace.AlignedHammockGrid.linearHammockGridEquiv_simplex` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` |
 | `Ript.Higher.CostExactZigzagMappingSpace.alignedHammockCore` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` |
 | `Ript.Higher.CostExactZigzagMappingSpace.columnRefinementCore` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` |
@@ -998,6 +1012,10 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.lean`.
 | `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_originalEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` |
 | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_hammockFactorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` |
 | `Ript.Higher.CostExactZigzagMappingSpace.hammockPathNerveCore` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` |
+| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_whiskerLeftEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` |
+| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_whiskerRightEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` |
+| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_appendEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` |
+| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathWhiskeringCore` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` |
 | `Ript.Higher.CostExactZigzagMappingSpace.core` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` |
 | `CategoryTheory.Pseudofunctor.homotopyFunctor` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/PseudofunctorHomotopy.lean` |
 | `CategoryTheory.Pseudofunctor.homotopyFunctor_map_homMk` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/PseudofunctorHomotopy.lean` |

BLUEPRINT.md

@@ -390,9 +390,9 @@ Every node in this graph is an existing compiled module.
 | 12 (zero-truncated common-refinement mapping nerve) | Wrapped rows form a thin common-refinement groupoid; its canonical functor to the discrete row quotient is faithful, full, essentially surjective, and hence a categorical equivalence; the induced nerve map has categorical-nerve equivalence evidence, an explicit simplicial inverse and both homotopies, and exact row-vertex action | PROVED |
 | 12 (non-thin semantic refinement-path nerve) | Refinement syntax modulo equality of quotient-cell interpretations forms a non-thin groupoid; executable reversal supplies inverses; its semantic functor into the linear mapping category is faithful and essentially surjective on row objects, maps every path to an isomorphism, and induces a nerve map with exact row-vertex and arbitrary-refinement-edge action; the zero-truncation functor to the thin groupoid is full and essentially surjective | PROVED |
 | 12 (exact refinement-generated semantic image) | Actual quotient 2-cells equipped with existence of an executable refinement generator form a non-thin image subgroupoid of the linear mapping category; inclusion is faithful, the semantic refinement-path functor is full, faithful, essentially surjective and hence an equivalence onto this exact image, and the induced nerve equivalence has an explicit simplicial homotopy inverse, exact generator-edge action, and strict factorization of the original semantic nerve map | PROVED |
-| 12 (aligned-cell-augmented hammock paths) | A non-groupoidal generated path syntax alternates executable refinements with arbitrary aligned raw 2-cells and vertical composition, then quotients only by equality of quotient-cell semantics; its semantic functor into the full linear mapping category is faithful and object-essentially-surjective, the refinement-path groupoid embeds faithfully and factors strictly through it, every aligned cell lies in its exact semantic image, and every source 2-cell has a canonical one-column representative equal to the original quotient cell conjugated by right-unitors; the induced cost-exact nerve maps have exact refinement/aligned/source-edge formulas | PROVED |
+| 12 (aligned-cell-augmented hammock paths) | A non-groupoidal generated path syntax alternates executable refinements with arbitrary aligned raw 2-cells and vertical composition, then quotients only by equality of quotient-cell semantics; normalized left/right whiskering enters and leaves binary append through canonical linear-normal-form isomorphisms, horizontal append composes those operations, and semantic equality/image membership are closed under all three; the semantic functor is faithful and object-essentially-surjective, refinement paths embed faithfully and factor strictly, every source 2-cell has a canonical one-column representative, raw identity/original cells are normalizable and normalizability is closed under vertical composition; cost-exact three-model nerve maps have exact whiskering/append edge formulas | PROVED |
 | 12 (cost-exact two-layer global comparison) | Pseudofunctor-induced functor on homotopy categories; localization-aware relative Rezk map and auxiliary ordinary outer map into the actual marked-zigzag target; explicit source/target outer completeness homotopy equivalences; marked outer arrows factoring through the target actual-equivalence space; packaging with the exact non-groupoidal local nerve comparison; exact vertex, identity, horizontal-composition, associator, and left/right-unitor gluing; arbitrary invertible local 2-cell decoding; explicit pentagon and triangle compatibility | PROVED |
-| 12 (global cost-exact complete-Segal/Rezk equivalence) | Normalize every presented quotient 2-cell into alternating aligned-cell/refinement hammock paths (or characterize the remaining missing generators), prove critical-pair coherence and reduced-hammock homotopical invariance (or compare the generated path category to another accepted derived mapping-space construction), connect that comparison to a standard weak-equivalence interface, and finish the standard Dwyer--Kan/Rezk weak-equivalence and completeness theorem | OPEN_RESEARCH |
+| 12 (global cost-exact complete-Segal/Rezk equivalence) | Prove normalization-isomorphism naturality for raw left/right whiskering, normalize the remaining structural raw-cell generators and hence every presented quotient 2-cell into alternating aligned-cell/refinement hammock paths, prove critical-pair coherence and reduced-hammock homotopical invariance (or compare the generated path category to another accepted derived mapping-space construction), connect that comparison to a standard weak-equivalence interface, and finish the standard Dwyer--Kan/Rezk weak-equivalence and completeness theorem | OPEN_RESEARCH |
 
 ## Finite deterministic copy-discard theorem records
 

CONJECTURES.md

@@ -468,11 +468,14 @@ through it strictly. A larger non-groupoidal path category now alternates
 refinements with arbitrary aligned raw 2-cells. Its semantics is faithful, the
 refinement subsystem embeds faithfully and factors strictly, and every source
 2-cell has a canonical one-column representative whose quotient semantics is
-the original 2-cell conjugated by right-unitors. The remaining classical gap
-is normalizing every presented quotient 2-cell into these alternating paths
-(or identifying the missing generators), together with coherence for
-competing forward/marked moves, reduced-hammock moves, and their homotopical
-invariance.
+the original 2-cell conjugated by right-unitors. The path calculus is now
+closed under normalized left/right whiskering and horizontal append, with
+exact cost-exact three-model nerve formulas. Raw identities and original cells
+are normalizable, and normalizability is closed under vertical composition.
+The next missing induction law is naturality of the chosen normalization
+isomorphisms with raw whiskering; after it, the remaining structural generators
+must be normalized before fullness can be claimed. Competing forward/marked
+moves, reduced-hammock moves, and their homotopical invariance remain open.
 The 0-truncated layer is now compiled separately: wrapped rows form a thin
 common-refinement groupoid categorically equivalent to the discrete row
 quotient, and its nerve comparison has an explicit simplicial homotopy inverse.
@@ -577,9 +580,12 @@ and simplicially equivalent to the exact subgroupoid of refinement-generated
 quotient 2-cells, which includes faithfully in the full linear mapping
 category and strictly factors the semantic nerve map. The aligned-cell-
 augmented path category now adds arbitrary pointwise raw cells, contains every
-source 2-cell in one-column form, and strictly extends refinement paths.
-Normalization of all presented quotient 2-cells into this generated category,
-critical-pair coherence, and reduced-hammock invariance remain open.
+source 2-cell in one-column form, strictly extends refinement paths, and is
+closed under normalized left/right whiskering and horizontal append. Identity,
+vertical-composite, and original-cell normalization cases are proved.
+Normalization-isomorphism naturality for raw whiskering and the remaining
+structural generators, critical-pair coherence, and reduced-hammock invariance
+remain open.
 
 The first complete construction against that predicate is now kernel checked.
 Identity precomposition is an adjoint equivalence of pseudofunctors and an