feat(higher): prove hammock normalization naturality

AXIOMS.md

@@ -993,6 +993,27 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.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` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.flatten_forward` | `none` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.flatten_backward` | `none` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_atom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_nil` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_append` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.AlignedCell.quotientVcomp_assoc` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.appendIso_inv_whiskerLeft_appendIso_hom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.appendIso_inv_whiskerRight_appendIso_hom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedHom_whiskerLeft` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedHom_whiskerRight` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_whiskerLeft` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_whiskerRight` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerLeft_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerRight_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceId` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceIdInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceId_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceIdInv_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_transport` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.transport_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizable_of_structuralGenerators` | `[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` |
@@ -1016,6 +1037,7 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.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.hammockRawCellNormalizationCore` | `[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; 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 (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; explicit append-isomorphism exchange/cancellation proves normalization naturality for raw left/right whiskering; raw identity, original, source-identity/inverse, whiskering, vertical-composite, and equality-transport cells are normalizable; `StructuralGeneratorNormalizable` lists exactly the remaining source-composite, marked pair, associator, and unitor obligations and yields all-cell normalization by structural induction; the cost-exact core records these completed branches and conditional induction | 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) | 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 |
+| 12 (global cost-exact complete-Segal/Rezk equivalence) | Discharge the twelve explicit `StructuralGeneratorNormalizable` fields for source composition/inverse, marked unit/counit and inverses, associator/inverse, and left/right unitors and inverses; deduce every presented quotient 2-cell has an alternating aligned/refinement path and hence semantic fullness, then 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

@@ -472,10 +472,15 @@ 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.
+Normalization naturality for both raw whiskerings is now proved by explicit
+append-isomorphism exchange and cancellation; source identity and inverse plus
+equality transport are normalizable too. The exact remaining induction basis
+is the twelve-field `StructuralGeneratorNormalizable` record: source composite
+and inverse, marked unit/counit and inverses, associator and inverse, and both
+unitors and inverses. That record already implies normalization of every raw
+cell by structural induction, but none of its unproved fields is assumed in an
+unconditional theorem. 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.
@@ -582,10 +587,11 @@ 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, 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.
+vertical-composite, original-cell, both whiskering, source-identity/inverse,
+and equality-transport normalization cases are proved. The remaining twelve
+structural generator obligations are explicit and sufficient for the complete
+induction, but remain unproved; 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