diff --git a/AXIOMS.md b/AXIOMS.md
index 78710ad..38c1eab 100644
--- a/AXIOMS.md
+++ b/AXIOMS.md
@@ -1014,6 +1014,16 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.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` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_singleton` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_singleton_inv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_singleton_symm_hom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightAssociatedPair_coherence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_twoAtoms_hom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_twoAtoms_inv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceComp` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceCompInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceComp_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceCompInv_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` |
diff --git a/BLUEPRINT.md b/BLUEPRINT.md
index 1511a58..ff1c30a 100644
--- a/BLUEPRINT.md
+++ b/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; 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 (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; pure bicategorical coherence identifies two-atomic-step normalization, so source composition/inverse normalize exactly to forward expansion/contraction; raw identity, original, source-identity/inverse, source-composition/inverse, whiskering, vertical-composite, and equality-transport cells are normalizable; `StructuralGeneratorNormalizable` now lists exactly ten remaining marked pair, associator, and unitor obligations and yields all-cell normalization by structural 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) | 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 |
+| 12 (global cost-exact complete-Segal/Rezk equivalence) | Discharge the ten explicit `StructuralGeneratorNormalizable` fields for 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
 
diff --git a/CONJECTURES.md b/CONJECTURES.md
index be5e525..524dc8f 100644
--- a/CONJECTURES.md
+++ b/CONJECTURES.md
@@ -475,9 +475,11 @@ are normalizable, and normalizability is closed under vertical composition.
 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
+has now shrunk to the ten-field `StructuralGeneratorNormalizable` record:
+marked unit/counit and inverses, associator and inverse, and both unitors and
+inverses. Source composition/inverse are now normalized exactly by executable
+forward expansion/contraction using the audited two-atomic-step coherence
+formula. The remaining 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.
@@ -588,8 +590,9 @@ 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, 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
+source-composition/inverse, and equality-transport normalization cases are
+proved. The remaining ten structural generator obligations are explicit and
+sufficient for the complete
 induction, but remain unproved; critical-pair coherence and reduced-hammock
 invariance remain open.
 
diff --git a/MODEL_MATRIX.md b/MODEL_MATRIX.md
index 36f9d2c..e526717 100644
--- a/MODEL_MATRIX.md
+++ b/MODEL_MATRIX.md
@@ -564,7 +564,7 @@ or the executable cores.
 | Presheaf universe | Type-valued presheaves on the internal groupoid | Yoneda is fully faithful; representable transformations/isomorphisms correspond to internal identity/equivalence | Semantic proof layer; Mathlib Yoneda audits with classical choice |
 | Yoneda envelope | Essential image of representables in the presheaf universe | Groupoid equivalent to the internal groupoid; inclusion factors Yoneda; the restricted Yoneda functor is a Mathlib localization at all internal identities | Noncomputable essential-image witnesses; exact ordinary localization of an already-groupoidal source, not a Rezk completion |
 | Simplicial interface nerve | Ordinary categorical nerve of the internal groupoid | Complete Kan horn filling, strict Segal, quasicategory, 2-coskeletal; vertices/edges/2-simplices encode interfaces, identities, and composition; homotopy category recovers the groupoid | Semantic proof layer; chosen fillers audit with classical choice; no complete-Segal or Rezk claim |
-| Rezk classifying diagram | Outer simplicial category of composable interface strings, followed levelwise by the ordinary nerve | Every vertical level and horizontal row is a groupoid nerve and Kan; every horizontal row is strict Segal; the whole outer diagram is naturally `n ↦ Map(Δ[n], N(M.Object))`; `Map(∂Δ[n], N(M.Object))` is the genuine matching limit; every matching map is a fibration; the actual completeness map has an explicit simplicial homotopy inverse | Semantic proof layer; exact project-local `GroupoidalCompleteSegal` and `HomotopyEquivalenceWitness` evidence proved; the full cost-exact localization, common-universe local comparison, localization-aware all-dimensional relative outer Rezk map, source/target completeness witnesses, arbitrary-2-cell one-skeleton glue, vertical local 2-simplex/composite-diagonal glue, degree-one horizontal compositor squares, degree-two vertical pasting/interchange, the explicit three-tetrahedron degree-two compositor prism, all-degree local prism coherence, arbitrary outer-string vertex/restriction comparison, relative-outer gluing of every all-degree prism source vertex, strict decoded-pair naturality for every restriction, exact side-sensitive outer/local glue for every actual target prism-face vertex, a categorical-nerve equivalence from the presented relative-zigzag mapping nerve to every actual target local nerve, strict all-degree local-map factorization, outer essential surjectivity, target-independent algebraic/simplicial presentation universality, an audited `PresentedDwyerKanCore`, an independent right-associated linear hammock mapping category equivalent to the binary presentation and actual target local nerve, an audited `LinearHammockDwyerKanCore`, an exact arbitrary-height row-grid representation of every linear-hammock simplex, exact quotient/nerve interpretation of the fixed-shape aligned multi-column fragment, an executable elementary forward/marked-pair refinement calculus, an object-level common-refinement quotient sound for semantic isomorphism, a zero-truncated thin refinement-groupoid nerve equivalent to the discrete quotient nerve, a non-thin semantic refinement-path groupoid nerve with exact edge action, its categorical/nerve equivalence to the exact refinement-generated quotient-cell image subgroupoid, and a faithful aligned-cell-augmented non-groupoidal path category containing every source 2-cell in canonical one-column form are proved; normalized whiskering/append have exact three-model formulas, normalization commutes with raw whiskering, identity/original/source-identity/transport and closure cases are proved, and a twelve-field criterion implies all-cell normalization; those twelve structural generator fields, semantic fullness, competing-move coherence, reduced-hammock invariance, standard weak-equivalence packaging, and the final Dwyer--Kan comparison remain open |
+| Rezk classifying diagram | Outer simplicial category of composable interface strings, followed levelwise by the ordinary nerve | Every vertical level and horizontal row is a groupoid nerve and Kan; every horizontal row is strict Segal; the whole outer diagram is naturally `n ↦ Map(Δ[n], N(M.Object))`; `Map(∂Δ[n], N(M.Object))` is the genuine matching limit; every matching map is a fibration; the actual completeness map has an explicit simplicial homotopy inverse | Semantic proof layer; exact project-local `GroupoidalCompleteSegal` and `HomotopyEquivalenceWitness` evidence proved; the full cost-exact localization, common-universe local comparison, localization-aware all-dimensional relative outer Rezk map, source/target completeness witnesses, arbitrary-2-cell one-skeleton glue, vertical local 2-simplex/composite-diagonal glue, degree-one horizontal compositor squares, degree-two vertical pasting/interchange, the explicit three-tetrahedron degree-two compositor prism, all-degree local prism coherence, arbitrary outer-string vertex/restriction comparison, relative-outer gluing of every all-degree prism source vertex, strict decoded-pair naturality for every restriction, exact side-sensitive outer/local glue for every actual target prism-face vertex, a categorical-nerve equivalence from the presented relative-zigzag mapping nerve to every actual target local nerve, strict all-degree local-map factorization, outer essential surjectivity, target-independent algebraic/simplicial presentation universality, an audited `PresentedDwyerKanCore`, an independent right-associated linear hammock mapping category equivalent to the binary presentation and actual target local nerve, an audited `LinearHammockDwyerKanCore`, an exact arbitrary-height row-grid representation of every linear-hammock simplex, exact quotient/nerve interpretation of the fixed-shape aligned multi-column fragment, an executable elementary forward/marked-pair refinement calculus, an object-level common-refinement quotient sound for semantic isomorphism, a zero-truncated thin refinement-groupoid nerve equivalent to the discrete quotient nerve, a non-thin semantic refinement-path groupoid nerve with exact edge action, its categorical/nerve equivalence to the exact refinement-generated quotient-cell image subgroupoid, and a faithful aligned-cell-augmented non-groupoidal path category containing every source 2-cell in canonical one-column form are proved; normalized whiskering/append have exact three-model formulas, normalization commutes with raw whiskering, identity/original/source-identity/source-composition/transport and closure cases are proved, and a ten-field criterion implies all-cell normalization; those ten marked-pair/associator/unitor fields, semantic fullness, competing-move coherence, reduced-hammock invariance, standard weak-equivalence packaging, and the final Dwyer--Kan comparison remain open |
 
 The concrete Boolean model proves that `bit tensor unit` and `unit tensor bit`
 are unequal syntax trees in Lean while tensor symmetry makes them internally
@@ -673,8 +673,8 @@ pointwise raw cells, contains every source 2-cell in canonical one-column form,
 strictly extends the refinement path nerve, and is closed under normalized
 left/right whiskering and horizontal append. Normalization now commutes with
 both raw whiskerings; raw identity/original/source-identity/inverse and
-equality-transport cases plus vertical/whiskering closure are proved. Twelve
-explicit source-composite, marked-pair, associator, and unitor obligations are
+source-composition/inverse, equality-transport cases plus vertical/whiskering
+closure are proved. Ten explicit marked-pair, associator, and unitor obligations are
 sufficient for the complete structural induction but remain open, together
 with critical-pair coherence and reduced-hammock invariance. These
 layers do not add `Equiv α β → α = β` and are not a complete presheaf model.
diff --git a/Ript/Audit/AxiomChecks.lean b/Ript/Audit/AxiomChecks.lean
index e1aaf7e..dbdcd36 100644
--- a/Ript/Audit/AxiomChecks.lean
+++ b/Ript/Audit/AxiomChecks.lean
@@ -1095,6 +1095,16 @@ set_option autoImplicit false
 #print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_transport
 #print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.transport_normalizable
 #print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizable_of_structuralGenerators
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_singleton
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_singleton_inv
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_singleton_symm_hom
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightAssociatedPair_coherence
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_twoAtoms_hom
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_twoAtoms_inv
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceComp
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceCompInv
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceComp_normalizable
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceCompInv_normalizable
 #print axioms Ript.Higher.CostExactZigzagMappingSpace.AlignedHammockGrid.linearHammockGridEquiv_simplex
 #print axioms Ript.Higher.CostExactZigzagMappingSpace.alignedHammockCore
 #print axioms Ript.Higher.CostExactZigzagMappingSpace.columnRefinementCore
diff --git a/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean b/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean
index 7c3248f..c46c4d5 100644
--- a/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean
+++ b/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean
@@ -27,7 +27,8 @@ now alternates arbitrary aligned cells with invertible refinements, retains
 all source 2-cells in one-column form, and is closed under normalized left/right
 whiskering and horizontal append. Normalization is natural for raw whiskering;
 identity, original, source-identity/inverse, composition-closure, whiskering,
-and equality-transport induction branches are complete, while twelve explicit
+source-composition/inverse, and equality-transport induction branches are
+complete, while ten explicit
 structural-generator obligations remain. Coverage of every presented quotient
 2-cell, critical-pair coherence, and reduced-hammock invariance are still
 absent, so this is not by itself the classical Dwyer--Kan hammock localization.
@@ -2394,6 +2395,106 @@ theorem normalizedCellHom_sourceIdInv {X : B} :
     exact (Presented.wordRightUnitorIso W (.nil X)).inv_hom_id
   rw [unitCancellation, AlignedCell.quotientVcomp_id_comp]
 
+/-- The source-composition comparison normalizes to executable expansion of
+one forward composite into two forward columns. -/
+@[simp]
+theorem normalizedCellHom_sourceComp {X Y Z : B}
+    (f : X ⟶ Y) (g : Y ⟶ Z) :
+    normalizedCellHom W (Cell.sourceComp (W := W) f g) =
+      ColumnRefinement.toHom W (.expandForward f g (.nil Z)) := by
+  unfold normalizedCellHom normalizedHom
+  simp only [Word.append_eq_comp, LinearWord.flatten_append,
+    Word.forward, Word.single]
+  rw [show LinearWord.normalizationIso W
+      (Word.atom (Step.forward (f ≫ g))) =
+    (Presented.wordRightUnitorIso W
+      (Word.atom (Step.forward (f ≫ g)))).symm from rfl]
+  rw [LinearWord.normalizationIso_twoAtoms_hom W
+    (Step.forward (W := W) f) (Step.forward (W := W) g)]
+  simp only [Iso.symm_inv]
+  rw [ColumnRefinement.toHom_expandForward]
+  change AlignedCell.quotientVcomp W
+      (Presented.wordRightUnitorIso W
+        (Word.atom (Step.forward (f ≫ g)))).hom
+      (AlignedCell.quotientVcomp W
+        (Presented.mk W (Cell.sourceComp (W := W) f g))
+        (AlignedCell.quotientVcomp W
+          (Presented.wordRightUnitorIso W
+            (.comp (Word.atom (Step.forward f))
+              (Word.atom (Step.forward g)))).inv
+          (Presented.wordAssociatorIso W (Word.forward W f)
+            (Word.forward W g) (.nil Z)).hom)) =
+    AlignedCell.quotientVcomp W
+      (Presented.whiskerRightHom W (.nil Z)
+        (Presented.mk W (Cell.sourceComp (W := W) f g)))
+      (Presented.wordAssociatorIso W (Word.forward W f)
+        (Word.forward W g) (.nil Z)).hom
+  rw [← AlignedCell.quotientVcomp_assoc]
+  have whiskerEquality :
+      Presented.whiskerRightHom W (.nil Z)
+          (Presented.mk W (Cell.sourceComp (W := W) f g)) =
+        AlignedCell.quotientVcomp W
+          (Presented.wordRightUnitorIso W (Word.forward W (f ≫ g))).hom
+          (AlignedCell.quotientVcomp W
+            (Presented.mk W (Cell.sourceComp (W := W) f g))
+            (Presented.wordRightUnitorIso W
+              (Word.append (W := W) (Word.forward W f)
+                (Word.forward W g))).inv) :=
+    Quot.sound (Presented.Rel.whisker_right_id_word
+      (Cell.sourceComp (W := W) f g))
+  rw [whiskerEquality]
+  simp only [AlignedCell.quotientVcomp_assoc]
+  rfl
+
+/-- The inverse source-composition comparison normalizes to executable
+contraction of two forward columns. -/
+@[simp]
+theorem normalizedCellHom_sourceCompInv {X Y Z : B}
+    (f : X ⟶ Y) (g : Y ⟶ Z) :
+    normalizedCellHom W (Cell.sourceCompInv (W := W) f g) =
+      ColumnRefinement.toHom W (.contractForward f g (.nil Z)) := by
+  unfold normalizedCellHom normalizedHom
+  simp only [Word.append_eq_comp, LinearWord.flatten_append,
+    Word.forward, Word.single]
+  rw [LinearWord.normalizationIso_twoAtoms_inv W
+    (Step.forward (W := W) f) (Step.forward (W := W) g)]
+  rw [show LinearWord.normalizationIso W
+      (Word.atom (Step.forward (f ≫ g))) =
+    (Presented.wordRightUnitorIso W
+      (Word.atom (Step.forward (f ≫ g)))).symm from rfl]
+  simp only [Iso.symm_hom]
+  rw [ColumnRefinement.toHom_contractForward]
+  change AlignedCell.quotientVcomp W
+      (AlignedCell.quotientVcomp W
+        (Presented.wordAssociatorIso W
+          (Word.forward W f) (Word.forward W g) (.nil Z)).inv
+        (Presented.wordRightUnitorIso W
+          (Word.append (W := W) (Word.forward W f)
+            (Word.forward W g))).hom)
+      (AlignedCell.quotientVcomp W
+        (Presented.mk W (Cell.sourceCompInv (W := W) f g))
+        (Presented.wordRightUnitorIso W (Word.forward W (f ≫ g))).inv) =
+    AlignedCell.quotientVcomp W
+      (Presented.wordAssociatorIso W
+        (Word.forward W f) (Word.forward W g) (.nil Z)).inv
+      (Presented.whiskerRightHom W (.nil Z)
+        (Presented.mk W (Cell.sourceCompInv (W := W) f g)))
+  rw [AlignedCell.quotientVcomp_assoc]
+  have whiskerEquality :
+      Presented.whiskerRightHom W (.nil Z)
+          (Presented.mk W (Cell.sourceCompInv (W := W) f g)) =
+        AlignedCell.quotientVcomp W
+          (Presented.wordRightUnitorIso W
+            (Word.append (W := W) (Word.forward W f)
+              (Word.forward W g))).hom
+          (AlignedCell.quotientVcomp W
+            (Presented.mk W (Cell.sourceCompInv (W := W) f g))
+            (Presented.wordRightUnitorIso W
+              (Word.forward W (f ≫ g))).inv) :=
+    Quot.sound (Presented.Rel.whisker_right_id_word
+      (Cell.sourceCompInv (W := W) f g))
+  rw [whiskerEquality]
+
 /-- Equality transport does not change normalized quotient semantics. -/
 @[simp]
 theorem normalizedCellHom_transport {X Y : B}
@@ -2522,6 +2623,20 @@ theorem sourceIdInv_normalizable {X : B} :
   rw [Normalizable, normalizedCellHom_sourceIdInv]
   exact refinement_mem_semanticImage W (.insertIdentity (.nil X))
 
+/-- Source-composition comparison is hammock-normalizable. -/
+theorem sourceComp_normalizable {X Y Z : B}
+    (f : X ⟶ Y) (g : Y ⟶ Z) :
+    Normalizable W (Cell.sourceComp (W := W) f g) := by
+  rw [Normalizable, normalizedCellHom_sourceComp]
+  exact refinement_mem_semanticImage W (.expandForward f g (.nil Z))
+
+/-- Inverse source-composition comparison is hammock-normalizable. -/
+theorem sourceCompInv_normalizable {X Y Z : B}
+    (f : X ⟶ Y) (g : Y ⟶ Z) :
+    Normalizable W (Cell.sourceCompInv (W := W) f g) := by
+  rw [Normalizable, normalizedCellHom_sourceCompInv]
+  exact refinement_mem_semanticImage W (.contractForward f g (.nil Z))
+
 /-- Equality transport preserves raw-cell normalizability. -/
 theorem transport_normalizable {X Y : B}
     {first second first' second' : Word W X Y}
@@ -2535,15 +2650,10 @@ theorem transport_normalizable {X Y : B}
 
 /-- Exact remaining generator obligations for a complete raw-cell
 normalization induction. Identity, vertical composition, original cells,
-source identities, both whiskerings, and equality transport are already
+source identities, source composition, both whiskerings, and equality transport
+are already
 discharged separately. -/
 structure StructuralGeneratorNormalizable : Prop where
-  /-- Source-composition comparison. -/
-  sourceComp : ∀ {X Y Z : B} (f : X ⟶ Y) (g : Y ⟶ Z),
-    Normalizable W (Cell.sourceComp (W := W) f g)
-  /-- Inverse source-composition comparison. -/
-  sourceCompInv : ∀ {X Y Z : B} (f : X ⟶ Y) (g : Y ⟶ Z),
-    Normalizable W (Cell.sourceCompInv (W := W) f g)
   /-- Marked unit. -/
   markedUnit : ∀ {X Y : B} (f : X ⟶ Y) (hf : W f),
     Normalizable W (Cell.markedUnit (W := W) f hf)
@@ -2593,8 +2703,8 @@ theorem normalizable_of_structuralGenerators
       exact originalCell_mem_semanticImage W alpha
   | sourceId => exact sourceId_normalizable W
   | sourceIdInv => exact sourceIdInv_normalizable W
-  | sourceComp f g => exact generators.sourceComp f g
-  | sourceCompInv f g => exact generators.sourceCompInv f g
+  | sourceComp f g => exact sourceComp_normalizable W f g
+  | sourceCompInv f g => exact sourceCompInv_normalizable W f g
   | markedUnit f hf => exact generators.markedUnit f hf
   | markedUnitInv f hf => exact generators.markedUnitInv f hf
   | markedCounit f hf => exact generators.markedCounit f hf
diff --git a/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean b/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean
index fa23c45..6333266 100644
--- a/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean
+++ b/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean
@@ -1,4 +1,5 @@
 import Ript.ForMathlib.CategoryTheory.Bicategory.MarkedZigzag
+import Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
 
 /-!
 # Linear hammock words for marked bicategories
@@ -145,6 +146,41 @@ noncomputable def toWordAppendIso {X Y Z : B}
         (Presented.wordAssociatorIso W
           (Word.atom step) (toWord W rest) (toWord W second)).symm
 
+/-- The append comparison for a singleton first row is the left-unitor
+comparison on the second row followed by inverse associativity. -/
+theorem toWordAppendIso_singleton {X Y Z : B} (step : Step W X Y)
+    (second : LinearWord W Y Z) :
+    toWordAppendIso W (.cons step (.nil Y)) second =
+      whiskerLeftIso (B := Presented.Localization W) (Word.atom step)
+          (Presented.wordLeftUnitorIso W (toWord W second)).symm ≪≫
+        (Presented.wordAssociatorIso W
+          (Word.atom step) (.nil Y) (toWord W second)).symm :=
+  rfl
+
+/-- The inverse singleton append comparison is associativity followed by the
+left unitor on the second row. -/
+theorem toWordAppendIso_singleton_inv {X Y Z : B} (step : Step W X Y)
+    (second : LinearWord W Y Z) :
+    (toWordAppendIso W (.cons step (.nil Y)) second).inv =
+      (Presented.wordAssociatorIso W
+        (Word.atom step) (.nil Y) (toWord W second)).hom ≫
+      Presented.whiskerLeftHom W (Word.atom step)
+        (Presented.wordLeftUnitorIso W (toWord W second)).hom := by
+  rw [toWordAppendIso_singleton]
+  rfl
+
+/-- The hom of the symmetric singleton append comparison is the same explicit
+associator/unitor composite. -/
+theorem toWordAppendIso_singleton_symm_hom {X Y Z : B}
+    (step : Step W X Y) (second : LinearWord W Y Z) :
+    (toWordAppendIso W (.cons step (.nil Y)) second).symm.hom =
+      (Presented.wordAssociatorIso W
+        (Word.atom step) (.nil Y) (toWord W second)).hom ≫
+      Presented.whiskerLeftHom W (Word.atom step)
+        (Presented.wordLeftUnitorIso W (toWord W second)).hom := by
+  rw [toWordAppendIso_singleton]
+  rfl
+
 /-- Every binary word is canonically isomorphic to the binary expansion of
 its flattened linear normal form. -/
 noncomputable def normalizationIso {X Y : B} (word : Word W X Y) :
@@ -186,6 +222,69 @@ theorem normalizationIso_append {X Y Z : B}
         (toWordAppendIso W (flatten W first) (flatten W second)).symm :=
   rfl
 
+/-- Pure bicategorical coherence used by normalization of a two-step linear
+row. -/
+theorem rightAssociatedPair_coherence {C : Type u} [Bicategory.{w, v} C]
+    {X Y Z : C} (first : X ⟶ Y) (second : Y ⟶ Z) :
+    (((ρ_ first).inv ▷ second) ≫
+        ((first ≫ 𝟙 Y) ◁ (ρ_ second).inv)) ≫
+      (α_ first (𝟙 Y) (second ≫ 𝟙 Z)).hom ≫
+      (first ◁ (λ_ (second ≫ 𝟙 Z)).hom) =
+    (ρ_ (first ≫ second)).inv ≫
+      (α_ first second (𝟙 Z)).hom := by
+  bicategory_coherence
+
+/-- Normalizing a binary word of two atomic steps is exactly inverse right
+unitor followed by the associator into the canonical right-associated row. -/
+theorem normalizationIso_twoAtoms_hom {X Y Z : B}
+    (first : Step W X Y) (second : Step W Y Z) :
+    (normalizationIso W (.comp (.atom first) (.atom second))).hom =
+    (Presented.wordRightUnitorIso W
+      (.comp (.atom first) (.atom second))).inv ≫
+      (Presented.wordAssociatorIso W
+        (.atom first) (.atom second) (.nil Z)).hom := by
+  rw [show normalizationIso W
+      (.comp (.atom first) (.atom second)) =
+    appendIso W (normalizationIso W (.atom first))
+        (normalizationIso W (.atom second)) ≪≫
+      (toWordAppendIso W (flatten W (.atom first))
+        (flatten W (.atom second))).symm from rfl]
+  simp only [flatten]
+  rw [normalizationIso_atom W first]
+  rw [normalizationIso_atom W second]
+  simp only [Iso.trans_hom]
+  rw [toWordAppendIso_singleton_symm_hom W first
+    (.cons second (.nil Z))]
+  unfold appendIso
+  simp only [Iso.trans_hom, Bicategory.whiskerLeftIso,
+    Bicategory.whiskerRightIso, toWord]
+  rw [show (Presented.wordRightUnitorIso W (Word.atom first)).symm.hom =
+      (Presented.wordRightUnitorIso W (Word.atom first)).inv from rfl]
+  rw [show (Presented.wordRightUnitorIso W (Word.atom second)).symm.hom =
+      (Presented.wordRightUnitorIso W (Word.atom second)).inv from rfl]
+  exact rightAssociatedPair_coherence
+    (C := Presented.Localization W) (Word.atom first) (Word.atom second)
+
+/-- Inverse of the two-atomic-step normalization: inverse associativity
+followed by the whole-word right unitor. -/
+theorem normalizationIso_twoAtoms_inv {X Y Z : B}
+    (first : Step W X Y) (second : Step W Y Z) :
+    (normalizationIso W (.comp (.atom first) (.atom second))).inv =
+      (Presented.wordAssociatorIso W
+        (.atom first) (.atom second) (.nil Z)).inv ≫
+      (Presented.wordRightUnitorIso W
+        (.comp (.atom first) (.atom second))).hom := by
+  have isoEquality :
+      normalizationIso W (.comp (.atom first) (.atom second)) =
+        (Presented.wordRightUnitorIso W
+          (.comp (.atom first) (.atom second))).symm ≪≫
+        Presented.wordAssociatorIso W
+          (.atom first) (.atom second) (.nil Z) := by
+    apply Iso.ext
+    exact normalizationIso_twoAtoms_hom W first second
+  rw [isoEquality]
+  rfl
+
 /-- Linear words form a mapping category by pulling back the quotient
 2-cell hom-sets between their binary expansions. -/
 instance category (X Y : B) : Category (LinearWord W X Y) where
diff --git a/Ript/Higher/CostExactZigzagMappingSpace.lean b/Ript/Higher/CostExactZigzagMappingSpace.lean
index 0d1d1b0..65e51e8 100644
--- a/Ript/Higher/CostExactZigzagMappingSpace.lean
+++ b/Ript/Higher/CostExactZigzagMappingSpace.lean
@@ -34,9 +34,9 @@ the refinement-path nerve faithfully, and covers every source 2-cell in its
 canonical one-column representation. Generated paths are now also closed under
 normalized left/right whiskering and horizontal append, with exact three-model
 nerve formulas. A raw-cell normalization core records the completed identity,
-original, source-identity/inverse, vertical, whiskering, and transport branches
-and a conditional all-cell induction from twelve remaining structural
-generators. Coverage of all presented quotient 2-cells, competing-move
+original, source-identity/inverse, source-composition/inverse, vertical,
+whiskering, and transport branches, plus a conditional all-cell induction from
+ten remaining structural generators. Coverage of all presented quotient 2-cells, competing-move
 coherence, and reduced-hammock invariance are still absent, so these results
 are not by themselves the final Dwyer--Kan theorem.
 -/
@@ -1389,6 +1389,20 @@ structure HammockRawCellNormalizationCore : Prop where
       (costExactArrows R)
       (Bicategory.MarkedZigzag.Cell.sourceIdInv
         (W := costExactArrows R) (X := M))
+  /-- Source-composition comparison is normalizable. -/
+  sourceComp : ∀ {M N P : ProcessModel.{u, v, w} R}
+      (f : M ⟶ N) (g : N ⟶ P),
+    Bicategory.MarkedZigzag.HammockPath.Normalizable
+      (costExactArrows R)
+      (Bicategory.MarkedZigzag.Cell.sourceComp
+        (W := costExactArrows R) f g)
+  /-- Inverse source-composition comparison is normalizable. -/
+  sourceCompInv : ∀ {M N P : ProcessModel.{u, v, w} R}
+      (f : M ⟶ N) (g : N ⟶ P),
+    Bicategory.MarkedZigzag.HammockPath.Normalizable
+      (costExactArrows R)
+      (Bicategory.MarkedZigzag.Cell.sourceCompInv
+        (W := costExactArrows R) f g)
   /-- Raw left whiskering preserves normalizability. -/
   whiskerLeft : ∀ (M N P : ProcessModel.{u, v, w} R)
       (pre : CostExactZigzag.Word (R := R) M N)
@@ -1454,6 +1468,12 @@ theorem hammockRawCellNormalizationCore :
   sourceIdInv := fun _ =>
     Bicategory.MarkedZigzag.HammockPath.sourceIdInv_normalizable
       (costExactArrows R)
+  sourceComp := fun f g =>
+    Bicategory.MarkedZigzag.HammockPath.sourceComp_normalizable
+      (costExactArrows R) f g
+  sourceCompInv := fun f g =>
+    Bicategory.MarkedZigzag.HammockPath.sourceCompInv_normalizable
+      (costExactArrows R) f g
   whiskerLeft := fun _ _ _ pre {_ _} {_} member =>
     Bicategory.MarkedZigzag.HammockPath.whiskerLeft_normalizable
       (costExactArrows R) pre member
diff --git a/docs/en/RESEARCH_STATUS.md b/docs/en/RESEARCH_STATUS.md
index c7bbf8f..265ee2b 100644
--- a/docs/en/RESEARCH_STATUS.md
+++ b/docs/en/RESEARCH_STATUS.md
@@ -396,7 +396,9 @@ cost-exact three-model nerve formulas. Raw identity/original cells are
 normalizable, and vertical composition preserves normalizability. Normalization
 naturality for raw left/right whiskering is now proved by explicit append-iso
 exchange and cancellation; source identity/inverse and equality transport are
-normalizable as well. The remaining twelve structural generator obligations
+normalizable as well. Source composition/inverse now normalize exactly to
+executable forward expansion/contraction using a pure bicategorical two-atom
+coherence formula. The remaining ten marked-pair/associator/unitor obligations
 are recorded exactly and already imply all-cell normalization conditionally,
 but are not assumed unconditionally. Semantic fullness, competing-move
 coherence, reduced-hammock invariance, standard weak-equivalence packaging, and
diff --git a/docs/en/reference/AXIOMS.md b/docs/en/reference/AXIOMS.md
index b5302a6..97eca55 100644
--- a/docs/en/reference/AXIOMS.md
+++ b/docs/en/reference/AXIOMS.md
@@ -1014,6 +1014,16 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.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` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_singleton` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_singleton_inv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_singleton_symm_hom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightAssociatedPair_coherence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_twoAtoms_hom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_twoAtoms_inv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceComp` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceCompInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceComp_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceCompInv_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` |
diff --git a/docs/en/reference/BLUEPRINT.md b/docs/en/reference/BLUEPRINT.md
index d404380..53238b2 100644
--- a/docs/en/reference/BLUEPRINT.md
+++ b/docs/en/reference/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; 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 (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; pure bicategorical coherence identifies two-atomic-step normalization, so source composition/inverse normalize exactly to forward expansion/contraction; raw identity, original, source-identity/inverse, source-composition/inverse, whiskering, vertical-composite, and equality-transport cells are normalizable; `StructuralGeneratorNormalizable` now lists exactly ten remaining marked pair, associator, and unitor obligations and yields all-cell normalization by structural 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) | 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 |
+| 12 (global cost-exact complete-Segal/Rezk equivalence) | Discharge the ten explicit `StructuralGeneratorNormalizable` fields for 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
 
diff --git a/docs/en/reference/CONJECTURES.md b/docs/en/reference/CONJECTURES.md
index f5a108e..f5d1897 100644
--- a/docs/en/reference/CONJECTURES.md
+++ b/docs/en/reference/CONJECTURES.md
@@ -475,9 +475,11 @@ are normalizable, and normalizability is closed under vertical composition.
 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
+has now shrunk to the ten-field `StructuralGeneratorNormalizable` record:
+marked unit/counit and inverses, associator and inverse, and both unitors and
+inverses. Source composition/inverse are now normalized exactly by executable
+forward expansion/contraction using the audited two-atomic-step coherence
+formula. The remaining 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.
@@ -588,8 +590,9 @@ 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, 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
+source-composition/inverse, and equality-transport normalization cases are
+proved. The remaining ten structural generator obligations are explicit and
+sufficient for the complete
 induction, but remain unproved; critical-pair coherence and reduced-hammock
 invariance remain open.
 
diff --git a/docs/en/reference/MODEL_MATRIX.md b/docs/en/reference/MODEL_MATRIX.md
index 618d811..38ba5d6 100644
--- a/docs/en/reference/MODEL_MATRIX.md
+++ b/docs/en/reference/MODEL_MATRIX.md
@@ -564,7 +564,7 @@ or the executable cores.
 | Presheaf universe | Type-valued presheaves on the internal groupoid | Yoneda is fully faithful; representable transformations/isomorphisms correspond to internal identity/equivalence | Semantic proof layer; Mathlib Yoneda audits with classical choice |
 | Yoneda envelope | Essential image of representables in the presheaf universe | Groupoid equivalent to the internal groupoid; inclusion factors Yoneda; the restricted Yoneda functor is a Mathlib localization at all internal identities | Noncomputable essential-image witnesses; exact ordinary localization of an already-groupoidal source, not a Rezk completion |
 | Simplicial interface nerve | Ordinary categorical nerve of the internal groupoid | Complete Kan horn filling, strict Segal, quasicategory, 2-coskeletal; vertices/edges/2-simplices encode interfaces, identities, and composition; homotopy category recovers the groupoid | Semantic proof layer; chosen fillers audit with classical choice; no complete-Segal or Rezk claim |
-| Rezk classifying diagram | Outer simplicial category of composable interface strings, followed levelwise by the ordinary nerve | Every vertical level and horizontal row is a groupoid nerve and Kan; every horizontal row is strict Segal; the whole outer diagram is naturally `n ↦ Map(Δ[n], N(M.Object))`; `Map(∂Δ[n], N(M.Object))` is the genuine matching limit; every matching map is a fibration; the actual completeness map has an explicit simplicial homotopy inverse | Semantic proof layer; exact project-local `GroupoidalCompleteSegal` and `HomotopyEquivalenceWitness` evidence proved; the full cost-exact localization, common-universe local comparison, localization-aware all-dimensional relative outer Rezk map, source/target completeness witnesses, arbitrary-2-cell one-skeleton glue, vertical local 2-simplex/composite-diagonal glue, degree-one horizontal compositor squares, degree-two vertical pasting/interchange, the explicit three-tetrahedron degree-two compositor prism, all-degree local prism coherence, arbitrary outer-string vertex/restriction comparison, relative-outer gluing of every all-degree prism source vertex, strict decoded-pair naturality for every restriction, exact side-sensitive outer/local glue for every actual target prism-face vertex, a categorical-nerve equivalence from the presented relative-zigzag mapping nerve to every actual target local nerve, strict all-degree local-map factorization, outer essential surjectivity, target-independent algebraic/simplicial presentation universality, an audited `PresentedDwyerKanCore`, an independent right-associated linear hammock mapping category equivalent to the binary presentation and actual target local nerve, an audited `LinearHammockDwyerKanCore`, an exact arbitrary-height row-grid representation of every linear-hammock simplex, exact quotient/nerve interpretation of the fixed-shape aligned multi-column fragment, an executable elementary forward/marked-pair refinement calculus, an object-level common-refinement quotient sound for semantic isomorphism, a zero-truncated thin refinement-groupoid nerve equivalent to the discrete quotient nerve, a non-thin semantic refinement-path groupoid nerve with exact edge action, its categorical/nerve equivalence to the exact refinement-generated quotient-cell image subgroupoid, and a faithful aligned-cell-augmented non-groupoidal path category containing every source 2-cell in canonical one-column form are proved; normalized whiskering/append have exact three-model formulas, normalization commutes with raw whiskering, identity/original/source-identity/transport and closure cases are proved, and a twelve-field criterion implies all-cell normalization; those twelve structural generator fields, semantic fullness, competing-move coherence, reduced-hammock invariance, standard weak-equivalence packaging, and the final Dwyer--Kan comparison remain open |
+| Rezk classifying diagram | Outer simplicial category of composable interface strings, followed levelwise by the ordinary nerve | Every vertical level and horizontal row is a groupoid nerve and Kan; every horizontal row is strict Segal; the whole outer diagram is naturally `n ↦ Map(Δ[n], N(M.Object))`; `Map(∂Δ[n], N(M.Object))` is the genuine matching limit; every matching map is a fibration; the actual completeness map has an explicit simplicial homotopy inverse | Semantic proof layer; exact project-local `GroupoidalCompleteSegal` and `HomotopyEquivalenceWitness` evidence proved; the full cost-exact localization, common-universe local comparison, localization-aware all-dimensional relative outer Rezk map, source/target completeness witnesses, arbitrary-2-cell one-skeleton glue, vertical local 2-simplex/composite-diagonal glue, degree-one horizontal compositor squares, degree-two vertical pasting/interchange, the explicit three-tetrahedron degree-two compositor prism, all-degree local prism coherence, arbitrary outer-string vertex/restriction comparison, relative-outer gluing of every all-degree prism source vertex, strict decoded-pair naturality for every restriction, exact side-sensitive outer/local glue for every actual target prism-face vertex, a categorical-nerve equivalence from the presented relative-zigzag mapping nerve to every actual target local nerve, strict all-degree local-map factorization, outer essential surjectivity, target-independent algebraic/simplicial presentation universality, an audited `PresentedDwyerKanCore`, an independent right-associated linear hammock mapping category equivalent to the binary presentation and actual target local nerve, an audited `LinearHammockDwyerKanCore`, an exact arbitrary-height row-grid representation of every linear-hammock simplex, exact quotient/nerve interpretation of the fixed-shape aligned multi-column fragment, an executable elementary forward/marked-pair refinement calculus, an object-level common-refinement quotient sound for semantic isomorphism, a zero-truncated thin refinement-groupoid nerve equivalent to the discrete quotient nerve, a non-thin semantic refinement-path groupoid nerve with exact edge action, its categorical/nerve equivalence to the exact refinement-generated quotient-cell image subgroupoid, and a faithful aligned-cell-augmented non-groupoidal path category containing every source 2-cell in canonical one-column form are proved; normalized whiskering/append have exact three-model formulas, normalization commutes with raw whiskering, identity/original/source-identity/source-composition/transport and closure cases are proved, and a ten-field criterion implies all-cell normalization; those ten marked-pair/associator/unitor fields, semantic fullness, competing-move coherence, reduced-hammock invariance, standard weak-equivalence packaging, and the final Dwyer--Kan comparison remain open |
 
 The concrete Boolean model proves that `bit tensor unit` and `unit tensor bit`
 are unequal syntax trees in Lean while tensor symmetry makes them internally
@@ -673,8 +673,8 @@ pointwise raw cells, contains every source 2-cell in canonical one-column form,
 strictly extends the refinement path nerve, and is closed under normalized
 left/right whiskering and horizontal append. Normalization now commutes with
 both raw whiskerings; raw identity/original/source-identity/inverse and
-equality-transport cases plus vertical/whiskering closure are proved. Twelve
-explicit source-composite, marked-pair, associator, and unitor obligations are
+source-composition/inverse, equality-transport cases plus vertical/whiskering
+closure are proved. Ten explicit marked-pair, associator, and unitor obligations are
 sufficient for the complete structural induction but remain open, together
 with critical-pair coherence and reduced-hammock invariance. These
 layers do not add `Equiv α β → α = β` and are not a complete presheaf model.
diff --git a/docs/eo/RESEARCH_STATUS.md b/docs/eo/RESEARCH_STATUS.md
index 4d05360..443b2dd 100644
--- a/docs/eo/RESEARCH_STATUS.md
+++ b/docs/eo/RESEARCH_STATUS.md
@@ -367,8 +367,10 @@ nervaj formuloj. Krudaj identecaj kaj originalaj ĉeloj estas normaligeblaj,
 kaj vertikala kunmeto konservas normaligeblecon. Normaligo nun estas nature
 kongrua kun ambaŭ krudaj whiskering-operacioj; krudaj identecaj, originalaj,
 font-identecaj/inversaj kaj transportaj kazoj, kune kun vertikala/whiskering
-fermo, estas pruvitaj. La ceteraj dek du source-composite, markitaj paroj,
-asociatoraj kaj unuitoraj generatoraj kampoj estas eksplicitaj kaj kondiĉe
+fermo, estas pruvitaj. Font-kompona/inversa estas pruvitaj per pura bikategoria
+du-atoma kohereco kaj ekzakta forward expand/contract. La ceteraj dek
+markitaj-paraj, asociatoraj kaj
+unuitoraj generatoraj kampoj estas eksplicitaj kaj kondiĉe
 implicas normaligon de ĉiu kruda ĉelo, sed ne estas senkondiĉe pruvitaj.
 Semantika pleneco, kohereco de kritikaj paroj, reduktita-hammock invariant eco
 kaj norma malfort-ekvivalenta pako restas malfermitaj.
diff --git a/docs/eo/reference/AXIOMS.md b/docs/eo/reference/AXIOMS.md
index a21eefe..4151901 100644
--- a/docs/eo/reference/AXIOMS.md
+++ b/docs/eo/reference/AXIOMS.md
@@ -1016,6 +1016,16 @@ per `scripts/sync-doc-reference-tables.sh` kaj ne estu mane redaktataj.
 | `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` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_singleton` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_singleton_inv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_singleton_symm_hom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightAssociatedPair_coherence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_twoAtoms_hom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_twoAtoms_inv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceComp` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceCompInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceComp_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceCompInv_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` |
diff --git a/docs/ja/RESEARCH_STATUS.md b/docs/ja/RESEARCH_STATUS.md
index 0205a74..43bcc04 100644
--- a/docs/ja/RESEARCH_STATUS.md
+++ b/docs/ja/RESEARCH_STATUS.md
@@ -151,7 +151,7 @@ fold は一意な解釈です。生成合同は全代数で健全で、木項モ
 
 制限付きながら真に独立した右結合 linear hammock 対象モデルもできました。typed step 列は二分 words と相互変換・平坦化され、長さを厳密に保存し、同値な mapping category、nerve の明示的ホモトピー逆、実際の対象 local nerve への直接比較を与えます。`LinearHammockDwyerKanCore` はこれを outer essential surjectivity と統合します。古典的な任意グリッド hammock または他の受理された derived 構成との比較は未解決です。
 
-任意高さの垂直 grid も明示化されました。`n`-grid は `n + 1` 行の linear hammocks、`n` 本の隣接商 2-cell 辺、全端点方程式を持ち、strict-Segal 再構成により linear hammock nerve の `n`-simplex と同値です。行、辺、復号、双方向 round trip は厳密に証明されています。固定形状の水平多列部分も形式化されました。同形の行は各共通列に一つの raw atomic 2-cell を持ち、幅と実行可能な水平 append は厳密で、商解釈は interchange により列ごとの恒等と垂直合成を保存し、任意高さの aligned grid は行と解釈済み辺を厳密に保つ genuine simplex を再構成します。基本的な前向き列 refinement も実行可能です。恒等列の挿入/削除、合成列の展開/縮約、任意の共通 prefix 下での move、推移合成、符号付き幅変化、商意味論での双方向 cancellation が証明されています。marked reverse 構造にも unit pair `f ; f⁻¹` と counit pair `f⁻¹ ; f` の実行可能な挿入/削除が加わり、符号付き幅 `±2`、厳密な意味同型、双方向 round trip、任意 prefix 安定性が証明されました。各 refinement は実行可能な逆と統一意味同型を持ちます。二本脚 common-refinement span は同値関係と行商を構成し、商等式は common-refinability と同値で、対象等式を仮定せず意味同型を与えます。0-切断 mapping 層も完成しました。包装された行は薄い common-refinement 群胚を構成し、離散行商圏と圏同値で、nerve 比較には明示的単体逆と両ホモトピーがあります。非薄意味 refinement-path 群胚は quotient-cell 意味で異なる paths を保持し、linear mapping nerve への nerve map は faithful、行対象上 essentially surjective、全 path を同型へ写し、厳密な頂点/辺式を持ちます。薄群胚への 0-切断も full かつ essentially surjective です。実際の商 2-cell と「実行可能な refinement が生成する」という存在証明は厳密な意味像群胚を構成します。path 群胚はこれと圏同値で、nerve 比較は明示的単体ホモトピー逆を持ち、完全な linear mapping category への像包含は faithful、元の意味 nerve map は厳密にこの像を経由します。さらに大きい非群胚生成 path 圏は refinement と任意の aligned raw 2-cell を交互に合成できます。意味関手と refinement 埋め込みはいずれも faithful で、旧 nerve map は厳密にこれを経由し、各始域 2-cell は right-unitor で共役された元の商 2-cell に等しい正準一列辺を持ちます。正規化された左右 whiskering と水平 append は意味同値と像所属を保存し、厳密な三モデル nerve 公式を持ちます。正規化は raw 左右 whiskering と自然に可換することが証明され、raw identity、original、source identity/逆、transport、および垂直/whiskering 閉包分岐が完成しました。残る十二の source-composite、marked pair、associator、unitor 構造生成元フィールドは明示され、条件付きで全 raw Cell 正規化を導きますが、まだ無条件には証明されていません。semantic fullness、critical-pair coherence、reduced-hammock 不変性、標準弱同値 packaging は未解決です。
+任意高さの垂直 grid も明示化されました。`n`-grid は `n + 1` 行の linear hammocks、`n` 本の隣接商 2-cell 辺、全端点方程式を持ち、strict-Segal 再構成により linear hammock nerve の `n`-simplex と同値です。行、辺、復号、双方向 round trip は厳密に証明されています。固定形状の水平多列部分も形式化されました。同形の行は各共通列に一つの raw atomic 2-cell を持ち、幅と実行可能な水平 append は厳密で、商解釈は interchange により列ごとの恒等と垂直合成を保存し、任意高さの aligned grid は行と解釈済み辺を厳密に保つ genuine simplex を再構成します。基本的な前向き列 refinement も実行可能です。恒等列の挿入/削除、合成列の展開/縮約、任意の共通 prefix 下での move、推移合成、符号付き幅変化、商意味論での双方向 cancellation が証明されています。marked reverse 構造にも unit pair `f ; f⁻¹` と counit pair `f⁻¹ ; f` の実行可能な挿入/削除が加わり、符号付き幅 `±2`、厳密な意味同型、双方向 round trip、任意 prefix 安定性が証明されました。各 refinement は実行可能な逆と統一意味同型を持ちます。二本脚 common-refinement span は同値関係と行商を構成し、商等式は common-refinability と同値で、対象等式を仮定せず意味同型を与えます。0-切断 mapping 層も完成しました。包装された行は薄い common-refinement 群胚を構成し、離散行商圏と圏同値で、nerve 比較には明示的単体逆と両ホモトピーがあります。非薄意味 refinement-path 群胚は quotient-cell 意味で異なる paths を保持し、linear mapping nerve への nerve map は faithful、行対象上 essentially surjective、全 path を同型へ写し、厳密な頂点/辺式を持ちます。薄群胚への 0-切断も full かつ essentially surjective です。実際の商 2-cell と「実行可能な refinement が生成する」という存在証明は厳密な意味像群胚を構成します。path 群胚はこれと圏同値で、nerve 比較は明示的単体ホモトピー逆を持ち、完全な linear mapping category への像包含は faithful、元の意味 nerve map は厳密にこの像を経由します。さらに大きい非群胚生成 path 圏は refinement と任意の aligned raw 2-cell を交互に合成できます。意味関手と refinement 埋め込みはいずれも faithful で、旧 nerve map は厳密にこれを経由し、各始域 2-cell は right-unitor で共役された元の商 2-cell に等しい正準一列辺を持ちます。正規化された左右 whiskering と水平 append は意味同値と像所属を保存し、厳密な三モデル nerve 公式を持ちます。正規化は raw 左右 whiskering と自然に可換することが証明され、raw identity、original、source identity/逆、source composition/逆、transport、および垂直/whiskering 閉包分岐が完成しました。source composition の正逆は純双圏二原子コヒーレンス式により forward expand/contract と厳密に一致します。残る十の marked pair、associator、unitor 構造生成元フィールドは明示され、条件付きで全 raw Cell 正規化を導きますが、まだ無条件には証明されていません。semantic fullness、critical-pair coherence、reduced-hammock 不変性、標準弱同値 packaging は未解決です。
 
 異なる資源代数のモデルは順序付き加法準同型で比較できます。直列、並列、構造、予算則が再添字
 付けされ、異種強モデル射は資源写像とともに合成します。これらは、資源代数とモデルを対象、
diff --git a/docs/ja/reference/AXIOMS.md b/docs/ja/reference/AXIOMS.md
index 1d898ea..7ab5f59 100644
--- a/docs/ja/reference/AXIOMS.md
+++ b/docs/ja/reference/AXIOMS.md
@@ -1014,6 +1014,16 @@
 | `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` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_singleton` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_singleton_inv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_singleton_symm_hom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightAssociatedPair_coherence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_twoAtoms_hom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_twoAtoms_inv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceComp` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceCompInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceComp_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceCompInv_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` |
diff --git a/docs/zh-CN/RESEARCH_STATUS.md b/docs/zh-CN/RESEARCH_STATUS.md
index dc8a3d1..1e8f24f 100644
--- a/docs/zh-CN/RESEARCH_STATUS.md
+++ b/docs/zh-CN/RESEARCH_STATUS.md
@@ -144,7 +144,7 @@ quarter/half-flip 树分别实现为概率、保留相干的随机酉量子仪
 
 现已有受限但真正独立的右结合 linear hammock 对象模型：typed step 列表与二叉 words 相互转换和扁平化，精确保留长度，并给出等价 mapping category、nerve 显式同伦逆以及到实际 target local nerve 的直接比较。`LinearHammockDwyerKanCore` 将其与 outer essential surjectivity 组合。尚缺与经典任意网格 hammock 或其他认可 derived 构造的比较。
 
-任意高度的纵向 grid 现也已显式化：`n`-grid 包含 `n + 1` 行 linear hammocks、`n` 条相邻商 2-胞腔边和全部端点方程，strict-Segal 重构将其与 linear hammock nerve 的 `n`-simplices 等价，并精确证明行、边、解码和双向 round trip。固定形状的横向多列片段也已形式化：等形行的每个公共列含一个原始原子 2-胞腔，宽度与可执行横向拼接精确，商解释通过 interchange 保持逐列恒等和纵向合成，任意高度 aligned grid 重构为具有精确行和解释边的真实 simplex。基本前向列细化也已可执行：恒等列可插入/删除，复合列可展开/收缩，move 可在任意公共前缀下提升并传递复合；带符号宽度变化精确，两个生成器对在商语义中双向抵消。marked reverse 结构现在也包含可执行的 unit pair `f ; f⁻¹` 与 counit pair `f⁻¹ ; f` 插入/删除，其带符号宽度为 `±2`，语义同构、双向 round trip 和任意前缀稳定性均已证明。每个 refinement 现有可执行逆向和统一语义同构；双腿 common-refinement span 构成等价关系及行商，商相等精确等价于可共同细化，并只推出语义同构而非对象相等。0-截断 mapping 层也已完成：包装行构成薄 common-refinement 群胚，并与离散行商范畴等价；nerve 比较具有显式单纯逆和双向同伦。非薄语义 refinement-path 群胚现保留按 quotient-cell 语义区分的路径；其 nerve map 到 linear mapping nerve 对态射 faithful、对行对象本质满、将全部路径映为同构并具有精确顶点/边公式，且到薄群胚的 0-截断 full 且本质满。实际商 2-胞腔连同“由可执行 refinement 生成”的存在见证现构成精确语义像群胚；路径群胚与其范畴等价，nerve 比较具有显式单纯同伦逆，像包含到完整 linear mapping category 忠实，原语义 nerve map 严格经过它。更大的非群胚生成路径范畴现可交替复合 refinement 与任意 aligned raw 2-胞腔；其语义及 refinement 嵌入均 faithful，旧 nerve map 严格经过它，并且每个源 2-胞腔都有一个规范单列边，其商语义是由左右规范 right-unitor 共轭的原 2-胞腔。规范左右 whiskering 与横向 append 现保持语义等价和像成员资格，并具有精确三模型 nerve 公式。正规化现已证明与 raw 左右 whiskering 自然相容；raw 恒等、original、source identity/逆、transport 及纵向/whiskering 闭包分支均已完成。剩余十二个 source-composite、marked pair、associator 和 unitor 结构生成元字段被精确登记，并在条件下推出全部 raw Cell 正规化，但尚未无条件证明；semantic fullness、critical-pair 协调、约化 hammock 不变性及标准弱等价封装仍开放。
+任意高度的纵向 grid 现也已显式化：`n`-grid 包含 `n + 1` 行 linear hammocks、`n` 条相邻商 2-胞腔边和全部端点方程，strict-Segal 重构将其与 linear hammock nerve 的 `n`-simplices 等价，并精确证明行、边、解码和双向 round trip。固定形状的横向多列片段也已形式化：等形行的每个公共列含一个原始原子 2-胞腔，宽度与可执行横向拼接精确，商解释通过 interchange 保持逐列恒等和纵向合成，任意高度 aligned grid 重构为具有精确行和解释边的真实 simplex。基本前向列细化也已可执行：恒等列可插入/删除，复合列可展开/收缩，move 可在任意公共前缀下提升并传递复合；带符号宽度变化精确，两个生成器对在商语义中双向抵消。marked reverse 结构现在也包含可执行的 unit pair `f ; f⁻¹` 与 counit pair `f⁻¹ ; f` 插入/删除，其带符号宽度为 `±2`，语义同构、双向 round trip 和任意前缀稳定性均已证明。每个 refinement 现有可执行逆向和统一语义同构；双腿 common-refinement span 构成等价关系及行商，商相等精确等价于可共同细化，并只推出语义同构而非对象相等。0-截断 mapping 层也已完成：包装行构成薄 common-refinement 群胚，并与离散行商范畴等价；nerve 比较具有显式单纯逆和双向同伦。非薄语义 refinement-path 群胚现保留按 quotient-cell 语义区分的路径；其 nerve map 到 linear mapping nerve 对态射 faithful、对行对象本质满、将全部路径映为同构并具有精确顶点/边公式，且到薄群胚的 0-截断 full 且本质满。实际商 2-胞腔连同“由可执行 refinement 生成”的存在见证现构成精确语义像群胚；路径群胚与其范畴等价，nerve 比较具有显式单纯同伦逆，像包含到完整 linear mapping category 忠实，原语义 nerve map 严格经过它。更大的非群胚生成路径范畴现可交替复合 refinement 与任意 aligned raw 2-胞腔；其语义及 refinement 嵌入均 faithful，旧 nerve map 严格经过它，并且每个源 2-胞腔都有一个规范单列边，其商语义是由左右规范 right-unitor 共轭的原 2-胞腔。规范左右 whiskering 与横向 append 现保持语义等价和像成员资格，并具有精确三模型 nerve 公式。正规化现已证明与 raw 左右 whiskering 自然相容；raw 恒等、original、source identity/逆、source composition/逆、transport 及纵向/whiskering 闭包分支均已完成。source composition 正反方向通过纯双范畴两原子协调公式精确对应 forward expand/contract。剩余十个 marked pair、associator 和 unitor 结构生成元字段被精确登记，并在条件下推出全部 raw Cell 正规化，但尚未无条件证明；semantic fullness、critical-pair 协调、约化 hammock 不变性及标准弱等价封装仍开放。
 
 模型比较不再要求全局使用同一资源代数。有序加法同态重索引串行、并行、结构和预算律；跨资源
 代数的强辫模型态射随同态复合，并在每个固定资源映射上形成单子自然变换的局部范畴。四维计算
diff --git a/docs/zh-CN/reference/AXIOMS.md b/docs/zh-CN/reference/AXIOMS.md
index 557e730..c67739b 100644
--- a/docs/zh-CN/reference/AXIOMS.md
+++ b/docs/zh-CN/reference/AXIOMS.md
@@ -1014,6 +1014,16 @@
 | `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` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_singleton` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_singleton_inv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_singleton_symm_hom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightAssociatedPair_coherence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_twoAtoms_hom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_twoAtoms_inv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceComp` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceCompInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceComp_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceCompInv_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` |