diff --git a/AXIOMS.md b/AXIOMS.md
index efa4319..e65efdf 100644
--- a/AXIOMS.md
+++ b/AXIOMS.md
@@ -1085,6 +1085,19 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.lean`.
 | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.allCells_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
 | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.all_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
 | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.semanticEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.ColumnRefinement.toHom_reverse` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.ColumnRefinement.toHom_comp_reverse` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.ColumnRefinement.toHom_reverse_comp` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.structural_decrease` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.complexity_lt` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.toHom_eq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.wellFounded` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.terminating` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.reduces_toHom_eq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.criticalPair_toHom_eq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.joinable_toHom_eq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.exists_irreducible` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.exists_irreducible_semantic` | `[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` |
@@ -1112,6 +1125,7 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.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.hammockAdministrativeReductionCore` | `[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` |
diff --git a/BLUEPRINT.md b/BLUEPRINT.md
index 8d36a39..f0f3378 100644
--- a/BLUEPRINT.md
+++ b/BLUEPRINT.md
@@ -391,9 +391,10 @@ Every node in this graph is an existing compiled module.
 | 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; source structural and marked-pair generators normalize to executable refinements; both unitors and both associators normalize to explicit mutually inverse recursive paths; unconditional structural induction proves every raw cell normalizable; conjugating an arbitrary quotient representative yields a generated path for every linear quotient 2-cell, so the semantic functor is full, faithful, essentially surjective and a categorical equivalence, and its nerve comparison has an explicit simplicial homotopy inverse | PROVED |
+| 12 (generated hammock administrative reduction) | A directed raw-path reduction removes vertical units, right-associates composition, fuses adjacent refinement/aligned/common-prefix moves, cancels executable refinement inverses, and is closed under every path context; executable `nodeCount + leftWeight` complexity strictly decreases at every step, so the relation is well-founded and every path has an irreducible reduct; one-step and finite reductions preserve exact quotient semantics, and competing one-step moves agree semantically, while raw joinability/local confluence remains open | PROVED |
 | 12 (generated hammock Dwyer--Kan core) | Common-universe generated hammock mapping categories are categorically equivalent first to the independent linear hammock categories and then directly to the actual localization-target local hom-categories; both nerve comparisons have categorical-equivalence witnesses and explicit simplicial homotopy inverses, the direct target map factors strictly through the linear comparison, and outer essential surjectivity packages these results as an audited `GeneratedHammockDwyerKanCore` | 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) | Strengthen the proved project-local `GeneratedHammockDwyerKanCore` with critical-pair coherence and reduced-hammock homotopical invariance (or compare it to another accepted derived mapping-space construction), connect it to a standard weak-equivalence interface, and finish the standard global Dwyer--Kan/Rezk weak-equivalence and completeness theorem | OPEN_RESEARCH |
+| 12 (global cost-exact complete-Segal/Rezk equivalence) | Extend the proved terminating semantics-preserving administrative reduction to the full classical reduced arbitrary-grid move system; prove raw critical-pair joinability/local confluence and reduced-hammock homotopical invariance (or compare the generated core to another accepted derived mapping-space construction), connect the resulting `GeneratedHammockDwyerKanCore` to a standard weak-equivalence interface, and finish the standard global 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 32039a1..fa8ac38 100644
--- a/CONJECTURES.md
+++ b/CONJECTURES.md
@@ -501,8 +501,14 @@ direct categorical equivalence from generated paths to the actual target
 local hom-category. Its nerve comparison has an explicit homotopy inverse and
 factors strictly through the independent linear comparison; outer essential
 surjectivity packages this as `GeneratedHammockDwyerKanCore`. Competing
-forward/marked moves, reduced-hammock moves, and their homotopical invariance
-remain open.
+forward/marked moves now have a first terminating administrative reduction
+layer: vertical units, left nesting, adjacent refinement/aligned/common-prefix
+administration, and executable refinement inverse pairs reduce under every
+path context. `nodeCount + leftWeight` strictly decreases, every path has an
+irreducible reduct, and all finite reductions preserve quotient semantics;
+every one-step critical pair is therefore semantically coherent. Raw
+joinability/local confluence, the additional classical arbitrary-grid 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.
@@ -617,8 +623,13 @@ source-composition/inverse, and equality-transport normalization cases are
 proved; all marked unit/counit, unitor, and associator cases are proved too.
 Every raw cell is therefore normalizable, every quotient 2-cell between linear
 rows is in the generated semantic image, and the generated path category is
-equivalent to the full linear mapping category. Critical-pair coherence and
-reduced-hammock invariance remain open.
+equivalent to the full linear mapping category. Its first directed
+administrative reduction is terminating by a strictly decreasing executable
+complexity, preserves semantics for arbitrary finite sequences, and supplies
+an irreducible reduct for every path. Competing one-step reductions agree in
+quotient semantics. Raw critical-pair joinability/local confluence, the full
+classical arbitrary-grid move system, 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
diff --git a/MODEL_MATRIX.md b/MODEL_MATRIX.md
index 303e908..f12f217 100644
--- a/MODEL_MATRIX.md
+++ b/MODEL_MATRIX.md
@@ -681,5 +681,11 @@ categorical and nerve equivalence with an explicit homotopy inverse. Its
 common-universe replacement is directly equivalent to the actual target local
 hom-category, factors strictly through the linear comparison, and joins outer
 essential surjectivity in `GeneratedHammockDwyerKanCore`. Critical-pair
-coherence and reduced-hammock invariance remain open. These
+coherence and reduced-hammock invariance remain open. A first directed
+administrative reduction is nevertheless complete: its executable
+`nodeCount + leftWeight` complexity strictly decreases, every path reaches an
+irreducible reduct, all finite reductions preserve exact quotient semantics,
+and every one-step critical pair is semantically coherent. Raw joinability,
+local confluence, and the remaining classical arbitrary-grid moves are open.
+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 f437c4d..9beeffa 100644
--- a/Ript/Audit/AxiomChecks.lean
+++ b/Ript/Audit/AxiomChecks.lean
@@ -1166,6 +1166,19 @@ set_option autoImplicit false
 #print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.allCells_normalizable
 #print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.all_mem_semanticImage
 #print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.semanticEquivalence
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.ColumnRefinement.toHom_reverse
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.ColumnRefinement.toHom_comp_reverse
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.ColumnRefinement.toHom_reverse_comp
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.structural_decrease
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.complexity_lt
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.toHom_eq
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.wellFounded
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.terminating
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.reduces_toHom_eq
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.criticalPair_toHom_eq
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.joinable_toHom_eq
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.exists_irreducible
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.exists_irreducible_semantic
 #print axioms Ript.Higher.CostExactZigzagMappingSpace.AlignedHammockGrid.linearHammockGridEquiv_simplex
 #print axioms Ript.Higher.CostExactZigzagMappingSpace.alignedHammockCore
 #print axioms Ript.Higher.CostExactZigzagMappingSpace.columnRefinementCore
@@ -1193,6 +1206,7 @@ set_option autoImplicit false
 #print axioms Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_appendEdge
 #print axioms Ript.Higher.CostExactZigzagMappingSpace.hammockPathWhiskeringCore
 #print axioms Ript.Higher.CostExactZigzagMappingSpace.hammockRawCellNormalizationCore
+#print axioms Ript.Higher.CostExactZigzagMappingSpace.hammockAdministrativeReductionCore
 #print axioms Ript.Higher.CostExactZigzagMappingSpace.core
 #print axioms CategoryTheory.Pseudofunctor.homotopyFunctor
 #print axioms CategoryTheory.Pseudofunctor.homotopyFunctor_map_homMk
diff --git a/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean b/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean
index a51bd19..05ad680 100644
--- a/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean
+++ b/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean
@@ -946,6 +946,36 @@ theorem toIso_reverse {X Y : B}
   induction refinement <;> simp [reverse, toIso, *]
   all_goals (apply Iso.ext; rfl)
 
+/-- Executable reversal interprets as the inverse of the original refinement
+isomorphism. -/
+theorem toHom_reverse {X Y : B}
+    {source target : LinearWord W X Y}
+    (refinement : ColumnRefinement W source target) :
+    toHom W (reverse W refinement) = (toIso W refinement).inv := by
+  rw [toHom_eq_toIso_hom, toIso_reverse]
+  rfl
+
+/-- A refinement followed by its executable reverse is semantically identity. -/
+theorem toHom_comp_reverse {X Y : B}
+    {source target : LinearWord W X Y}
+    (refinement : ColumnRefinement W source target) :
+    AlignedCell.quotientVcomp W (toHom W refinement)
+        (toHom W (reverse W refinement)) =
+      𝟙 (LinearWord.toWord W source) := by
+  rw [toHom_eq_toIso_hom, toHom_reverse]
+  exact (toIso W refinement).hom_inv_id
+
+/-- The executable reverse followed by its refinement is also semantically
+identity. -/
+theorem toHom_reverse_comp {X Y : B}
+    {source target : LinearWord W X Y}
+    (refinement : ColumnRefinement W source target) :
+    AlignedCell.quotientVcomp W (toHom W (reverse W refinement))
+        (toHom W refinement) =
+      𝟙 (LinearWord.toWord W target) := by
+  rw [toHom_reverse, toHom_eq_toIso_hom]
+  exact (toIso W refinement).inv_hom_id
+
 /-- Any semantic inverse pair remains inverse after refinement beneath one
 common prefix column.  Iterating `under` therefore transports the generator
 round trips to an arbitrary executable prefix. -/
@@ -3518,6 +3548,290 @@ noncomputable def semanticEquivalence (X Y : B) :
     HammockPathObject W X Y ≌ LinearWord W X Y :=
   (semanticFunctor W X Y).asEquivalence
 
+/-! ## Terminating administrative reduction -/
+
+namespace AdministrativeReduction
+
+/-- Number of raw administrative constructors in a generated path. Identity
+paths contribute zero; atomic refinement/aligned moves contribute one. -/
+def nodeCount {X Y : B} {first second : LinearWord W X Y} :
+    HammockPath W first second → ℕ
+  | .identity _ => 0
+  | .vcomp alpha beta => 1 + nodeCount alpha + nodeCount beta
+  | .ofRefinement _ => 1
+  | .ofAligned _ => 1
+  | .whiskerLeft _ path => 1 + nodeCount path
+  | .whiskerRight path _ => 1 + nodeCount path
+  | .under _ path => 1 + nodeCount path
+
+/-- Weight of left-nested vertical composition. Orienting associativity to the
+right strictly decreases this component while preserving `nodeCount`. -/
+def leftWeight {X Y : B} {first second : LinearWord W X Y} :
+    HammockPath W first second → ℕ
+  | .identity _ => 0
+  | .vcomp alpha beta =>
+      leftWeight alpha + leftWeight beta + nodeCount W alpha
+  | .ofRefinement _ => 0
+  | .ofAligned _ => 0
+  | .whiskerLeft _ path => leftWeight path
+  | .whiskerRight path _ => leftWeight path
+  | .under _ path => leftWeight path
+
+/-- Executable scalar complexity for administrative reduction. -/
+def complexity {X Y : B} {first second : LinearWord W X Y}
+    (path : HammockPath W first second) : ℕ :=
+  nodeCount W path + leftWeight W path
+
+/-- One directed administrative reduction step. These moves remove vertical
+units, right-associate vertical composition, fuse adjacent executable or
+aligned moves, cancel executable refinement inverses, and fuse common-prefix
+administration. Every constructor is closed under all generated path
+contexts. -/
+inductive OneStep : ∀ {X Y : B} {first second : LinearWord W X Y},
+    HammockPath W first second → HammockPath W first second → Prop where
+  | vcomp_id_left {X Y : B} {first second : LinearWord W X Y}
+      (path : HammockPath W first second) :
+      OneStep (.vcomp (.identity first) path) path
+  | vcomp_id_right {X Y : B} {first second : LinearWord W X Y}
+      (path : HammockPath W first second) :
+      OneStep (.vcomp path (.identity second)) path
+  | vcomp_assoc {X Y : B}
+      {first second third fourth : LinearWord W X Y}
+      (alpha : HammockPath W first second)
+      (beta : HammockPath W second third)
+      (gamma : HammockPath W third fourth) :
+      OneStep (.vcomp (.vcomp alpha beta) gamma)
+        (.vcomp alpha (.vcomp beta gamma))
+  | refinement_vcomp {X Y : B}
+      {first second third : LinearWord W X Y}
+      (alpha : ColumnRefinement W first second)
+      (beta : ColumnRefinement W second third) :
+      OneStep (.vcomp (.ofRefinement alpha) (.ofRefinement beta))
+        (.ofRefinement (.vcomp alpha beta))
+  | refinement_hom_inv {X Y : B}
+      {first second : LinearWord W X Y}
+      (refinement : ColumnRefinement W first second) :
+      OneStep (.ofRefinement
+          (.vcomp refinement (ColumnRefinement.reverse W refinement)))
+        (.identity first)
+  | refinement_inv_hom {X Y : B}
+      {first second : LinearWord W X Y}
+      (refinement : ColumnRefinement W first second) :
+      OneStep (.ofRefinement
+          (.vcomp (ColumnRefinement.reverse W refinement) refinement))
+        (.identity second)
+  | aligned_vcomp {X Y : B}
+      {first second third : LinearWord W X Y}
+      (alpha : AlignedCell W first second)
+      (beta : AlignedCell W second third) :
+      OneStep (.vcomp (.ofAligned alpha) (.ofAligned beta))
+        (.ofAligned (AlignedCell.vcomp W alpha beta))
+  | under_identity {X Y Z : B} (step : Step W X Y)
+      (row : LinearWord W Y Z) :
+      OneStep (.under step (.identity row)) (.identity (.cons step row))
+  | under_vcomp {X Y Z : B} (step : Step W X Y)
+      {first second third : LinearWord W Y Z}
+      (alpha : HammockPath W first second)
+      (beta : HammockPath W second third) :
+      OneStep (.vcomp (.under step alpha) (.under step beta))
+        (.under step (.vcomp alpha beta))
+  | under_refinement {X Y Z : B} (step : Step W X Y)
+      {first second : LinearWord W Y Z}
+      (refinement : ColumnRefinement W first second) :
+      OneStep (.under step (.ofRefinement refinement))
+        (.ofRefinement (.under step refinement))
+  | vcomp_left {X Y : B}
+      {first second third : LinearWord W X Y}
+      {alpha : HammockPath W first second}
+      {alpha' : HammockPath W first second}
+      (reduction : OneStep alpha alpha')
+      (beta : HammockPath W second third) :
+      OneStep (.vcomp alpha beta) (.vcomp alpha' beta)
+  | vcomp_right {X Y : B}
+      {first second third : LinearWord W X Y}
+      (alpha : HammockPath W first second)
+      {beta : HammockPath W second third}
+      {beta' : HammockPath W second third}
+      (reduction : OneStep beta beta') :
+      OneStep (.vcomp alpha beta) (.vcomp alpha beta')
+  | whiskerLeft_context {X Y Z : B} (pre : LinearWord W X Y)
+      {first second : LinearWord W Y Z}
+      {alpha beta : HammockPath W first second}
+      (reduction : OneStep alpha beta) :
+      OneStep (.whiskerLeft pre alpha) (.whiskerLeft pre beta)
+  | whiskerRight_context {X Y Z : B}
+      {first second : LinearWord W X Y}
+      {alpha beta : HammockPath W first second}
+      (reduction : OneStep alpha beta) (post : LinearWord W Y Z) :
+      OneStep (.whiskerRight alpha post) (.whiskerRight beta post)
+  | under_context {X Y Z : B} (step : Step W X Y)
+      {first second : LinearWord W Y Z}
+      {alpha beta : HammockPath W first second}
+      (reduction : OneStep alpha beta) :
+      OneStep (.under step alpha) (.under step beta)
+
+/-- Every administrative step weakly decreases both structural components,
+and strictly decreases at least one. -/
+theorem structural_decrease {X Y : B}
+    {first second : LinearWord W X Y}
+    {source target : HammockPath W first second}
+    (reduction : OneStep W source target) :
+    nodeCount W target ≤ nodeCount W source ∧
+      leftWeight W target ≤ leftWeight W source ∧
+      (nodeCount W target < nodeCount W source ∨
+        leftWeight W target < leftWeight W source) := by
+  induction reduction <;>
+    simp only [nodeCount, leftWeight] at * <;> omega
+
+/-- Every directed administrative step strictly lowers executable
+complexity. -/
+theorem complexity_lt {X Y : B}
+    {first second : LinearWord W X Y}
+    {source target : HammockPath W first second}
+    (reduction : OneStep W source target) :
+    complexity W target < complexity W source := by
+  rcases structural_decrease W reduction with ⟨nodes, weight, strict⟩
+  unfold complexity
+  omega
+
+/-- Every directed administrative step preserves exact quotient semantics. -/
+theorem toHom_eq {X Y : B} {first second : LinearWord W X Y}
+    {source target : HammockPath W first second}
+    (reduction : OneStep W source target) :
+    toHom W source = toHom W target := by
+  induction reduction with
+  | vcomp_id_left path =>
+      exact AlignedCell.quotientVcomp_id_comp W (toHom W path)
+  | vcomp_id_right path =>
+      exact AlignedCell.quotientVcomp_comp_id W (toHom W path)
+  | vcomp_assoc alpha beta gamma =>
+      exact AlignedCell.quotientVcomp_assoc W
+        (toHom W alpha) (toHom W beta) (toHom W gamma)
+  | refinement_vcomp alpha beta =>
+      exact (ColumnRefinement.toHom_vcomp W alpha beta).symm
+  | refinement_hom_inv refinement =>
+      exact ColumnRefinement.toHom_comp_reverse W refinement
+  | refinement_inv_hom refinement =>
+      exact ColumnRefinement.toHom_reverse_comp W refinement
+  | aligned_vcomp alpha beta =>
+      exact (AlignedCell.toHom_vcomp W alpha beta).symm
+  | under_identity step row =>
+      exact Quot.sound (Presented.Rel.whisker_left_id
+        (Word.atom step) (LinearWord.toWord W row))
+  | under_vcomp step alpha beta =>
+      exact (AlignedCell.whiskerLeftHom_vcomp W (Word.atom step)
+        (toHom W alpha) (toHom W beta)).symm
+  | under_refinement step refinement => rfl
+  | vcomp_left reduction beta ih =>
+      simp only [toHom_vcomp]
+      rw [ih]
+  | vcomp_right alpha reduction ih =>
+      simp only [toHom_vcomp]
+      rw [ih]
+  | whiskerLeft_context pre reduction ih =>
+      simp only [toHom_whiskerLeft]
+      rw [ih]
+  | whiskerRight_context reduction post ih =>
+      simp only [toHom_whiskerRight]
+      rw [ih]
+  | under_context step reduction ih =>
+      simp only [toHom_under]
+      rw [ih]
+
+/-- Reflexive-transitive administrative reduction. -/
+abbrev Reduces {X Y : B} {first second : LinearWord W X Y} :=
+  Relation.ReflTransGen (@OneStep B _ W X Y first second)
+
+/-- Administrative reduction is terminating for every fixed endpoint pair. -/
+theorem wellFounded {X Y : B} {first second : LinearWord W X Y} :
+    WellFounded (fun target source : HammockPath W first second =>
+      OneStep W source target) := by
+  apply Subrelation.wf (r := (measure (complexity W)).rel)
+  · intro target source reduction
+    exact complexity_lt W reduction
+  · exact (measure (complexity W)).wf
+
+/-- Every path is accessible for the reversed one-step relation. -/
+theorem terminating {X Y : B} {first second : LinearWord W X Y}
+    (path : HammockPath W first second) :
+    Acc (fun target source : HammockPath W first second =>
+      OneStep W source target) path :=
+  (wellFounded W).apply path
+
+/-- Any finite administrative reduction sequence preserves exact quotient
+semantics. -/
+theorem reduces_toHom_eq {X Y : B} {first second : LinearWord W X Y}
+    {source target : HammockPath W first second}
+    (reduction : Reduces W source target) :
+    toHom W source = toHom W target := by
+  induction reduction using Relation.ReflTransGen.trans_induction_on with
+  | refl => rfl
+  | single step => exact toHom_eq W step
+  | trans _ _ ihLeft ihRight => exact ihLeft.trans ihRight
+
+/-- A path is administratively irreducible when no directed elementary step
+leaves it. -/
+def Irreducible {X Y : B} {first second : LinearWord W X Y}
+    (path : HammockPath W first second) : Prop :=
+  ∀ target, ¬OneStep W path target
+
+/-- A critical pair is a pair of one-step reductions with a common source. -/
+def CriticalPair {X Y : B} {first second : LinearWord W X Y}
+    (source left right : HammockPath W first second) : Prop :=
+  OneStep W source left ∧ OneStep W source right
+
+/-- Two administrative reducts are joinable when they reach a common path. -/
+def Joinable {X Y : B} {first second : LinearWord W X Y}
+    (left right : HammockPath W first second) : Prop :=
+  ∃ common, Reduces W left common ∧ Reduces W right common
+
+/-- Competing one-step administrative moves always agree in quotient
+semantics. This is semantic coherence, not yet raw joinability. -/
+theorem criticalPair_toHom_eq {X Y : B}
+    {first second : LinearWord W X Y}
+    {source left right : HammockPath W first second}
+    (critical : CriticalPair W source left right) :
+    toHom W left = toHom W right :=
+  (toHom_eq W critical.1).symm.trans (toHom_eq W critical.2)
+
+/-- Raw joinability implies equality of quotient semantics. -/
+theorem joinable_toHom_eq {X Y : B}
+    {first second : LinearWord W X Y}
+    {left right : HammockPath W first second}
+    (joinable : Joinable W left right) :
+    toHom W left = toHom W right := by
+  rcases joinable with ⟨common, leftReduction, rightReduction⟩
+  exact (reduces_toHom_eq W leftReduction).trans
+    (reduces_toHom_eq W rightReduction).symm
+
+/-- Termination gives an administratively irreducible reduct of every path. -/
+theorem exists_irreducible {X Y : B}
+    {first second : LinearWord W X Y}
+    (path : HammockPath W first second) :
+    ∃ normal, Reduces W path normal ∧ Irreducible W normal := by
+  classical
+  induction path using (wellFounded W).induction with
+  | h path ih =>
+      by_cases irreducible : Irreducible W path
+      · exact ⟨path, Relation.ReflTransGen.refl, irreducible⟩
+      · simp only [Irreducible, not_forall, Classical.not_not] at irreducible
+        rcases irreducible with ⟨next, step⟩
+        rcases ih next step with ⟨normal, reduction, normalIrreducible⟩
+        exact ⟨normal, Relation.ReflTransGen.head step reduction,
+          normalIrreducible⟩
+
+/-- Every path has an irreducible reduct with exactly the same quotient
+semantics. -/
+theorem exists_irreducible_semantic {X Y : B}
+    {first second : LinearWord W X Y}
+    (path : HammockPath W first second) :
+    ∃ normal, Reduces W path normal ∧ Irreducible W normal ∧
+      toHom W path = toHom W normal := by
+  rcases exists_irreducible W path with ⟨normal, reduction, irreducible⟩
+  exact ⟨normal, reduction, irreducible, reduces_toHom_eq W reduction⟩
+
+end AdministrativeReduction
+
 /-- Original source 2-cells are hammock-normalizable. -/
 theorem original_normalizable {X Y : B} {f g : X ⟶ Y}
     (alpha : f ⟶ g) :
diff --git a/Ript/Higher/CostExactZigzagMappingSpace.lean b/Ript/Higher/CostExactZigzagMappingSpace.lean
index 6b85978..4c45882 100644
--- a/Ript/Higher/CostExactZigzagMappingSpace.lean
+++ b/Ript/Higher/CostExactZigzagMappingSpace.lean
@@ -37,10 +37,13 @@ nerve formulas. Recursive right-unit and associator paths now normalize every
 raw generator in both directions, so structural induction covers every raw
 cell unconditionally. Every quotient 2-cell is represented by a generated
 path; the semantic functor is therefore a categorical equivalence and its
-nerve map has an explicit simplicial homotopy inverse. Competing-move
-coherence and reduced-hammock invariance are still absent, so this stronger
+nerve map has an explicit simplicial homotopy inverse. Raw competing-move
+joinability and reduced-hammock invariance are still absent, so this stronger
 mapping-space presentation is not by itself the final global Dwyer--Kan/Rezk
-theorem.
+theorem. A first terminating administrative reduction now removes categorical
+units/nesting, fuses adjacent generated moves, cancels executable refinement
+inverses, and preserves exact quotient semantics in every path context; raw
+joinability and the remaining classical arbitrary-grid moves stay open.
 -/
 
 set_option autoImplicit false
@@ -1617,6 +1620,99 @@ theorem hammockRawCellNormalizationCore :
     Bicategory.MarkedZigzag.HammockPath.allCells_normalizable
       (costExactArrows R) cell
 
+/-- Machine-facing terminating administrative reduction interface for
+cost-exact generated hammock paths. -/
+structure HammockAdministrativeReductionCore : Prop where
+  /-- Every elementary administrative step strictly lowers its executable
+  complexity. -/
+  oneStep_decreases : ∀ (M N : ProcessModel.{u, v, w} R)
+      {first second : LinearHammock M N}
+      {source target : Bicategory.MarkedZigzag.HammockPath
+        (costExactArrows R) first second},
+    Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.OneStep
+        (costExactArrows R) source target →
+      Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.complexity
+          (costExactArrows R) target <
+        Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.complexity
+          (costExactArrows R) source
+  /-- Every generated path is accessible for the reversed reduction
+  relation. -/
+  terminating : ∀ (M N : ProcessModel.{u, v, w} R)
+      {first second : LinearHammock M N}
+      (path : Bicategory.MarkedZigzag.HammockPath
+        (costExactArrows R) first second),
+    Acc (fun target source =>
+      Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.OneStep
+        (costExactArrows R) source target) path
+  /-- Every elementary step preserves exact quotient semantics. -/
+  oneStep_semantic : ∀ (M N : ProcessModel.{u, v, w} R)
+      {first second : LinearHammock M N}
+      {source target : Bicategory.MarkedZigzag.HammockPath
+        (costExactArrows R) first second},
+    Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.OneStep
+        (costExactArrows R) source target →
+      Bicategory.MarkedZigzag.HammockPath.toHom
+          (costExactArrows R) source =
+        Bicategory.MarkedZigzag.HammockPath.toHom
+          (costExactArrows R) target
+  /-- Every finite administrative reduction sequence preserves exact quotient
+  semantics. -/
+  reduces_semantic : ∀ (M N : ProcessModel.{u, v, w} R)
+      {first second : LinearHammock M N}
+      {source target : Bicategory.MarkedZigzag.HammockPath
+        (costExactArrows R) first second},
+    Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.Reduces
+        (costExactArrows R) source target →
+      Bicategory.MarkedZigzag.HammockPath.toHom
+          (costExactArrows R) source =
+      Bicategory.MarkedZigzag.HammockPath.toHom
+          (costExactArrows R) target
+  /-- Every path has an irreducible reduct with unchanged quotient
+  semantics. -/
+  normal_form : ∀ (M N : ProcessModel.{u, v, w} R)
+      {first second : LinearHammock M N}
+      (path : Bicategory.MarkedZigzag.HammockPath
+        (costExactArrows R) first second),
+    ∃ normal,
+      Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.Reduces
+          (costExactArrows R) path normal ∧
+        Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.Irreducible
+          (costExactArrows R) normal ∧
+        Bicategory.MarkedZigzag.HammockPath.toHom
+            (costExactArrows R) path =
+          Bicategory.MarkedZigzag.HammockPath.toHom
+            (costExactArrows R) normal
+
+/-- Every cost-exact model pair satisfies the terminating, semantics-
+preserving administrative reduction interface. -/
+theorem hammockAdministrativeReductionCore :
+    HammockAdministrativeReductionCore (R := R) where
+  oneStep_decreases := by
+    intro M N first second source target reduction
+    exact
+      Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.complexity_lt
+        (costExactArrows R) reduction
+  terminating := by
+    intro M N first second path
+    exact
+      Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.terminating
+        (costExactArrows R) path
+  oneStep_semantic := by
+    intro M N first second source target reduction
+    exact
+      Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.toHom_eq
+        (costExactArrows R) reduction
+  reduces_semantic := by
+    intro M N first second source target reduction
+    exact
+      Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.reduces_toHom_eq
+        (costExactArrows R) reduction
+  normal_form := by
+    intro M N first second path
+    exact
+      Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.exists_irreducible_semantic
+        (costExactArrows R) path
+
 /-- The source-defined relative mapping category is categorically equivalent
 to the actual local hom-category of the presented localization target. The
 underlying categories are definitionally the same presentation, but this
@@ -1931,6 +2027,10 @@ structure MappingSpaceCore (M N : ProcessModel.{u, v, w} R) where
   /-- Non-groupoidal generated hammock paths combining refinements with
   arbitrary aligned/source 2-cells and strictly extending refinement paths. -/
   hammockPathNerve : HammockPathNerveCore M N
+  /-- Terminating semantics-preserving administrative reduction for generated
+  hammock paths. -/
+  hammockAdministrativeReduction :
+    HammockAdministrativeReductionCore.{u, v, w} (R := R)
   /-- Common-universe generated hammock paths are categorically equivalent
   directly to the actual localization-target local hom-category. -/
   generatedTargetCategoricalEquivalence :
@@ -2027,6 +2127,7 @@ noncomputable def core (M N : ProcessModel.{u, v, w} R) :
   refinementPathNerve := refinementPathNerveCore M N
   refinementImageNerve := refinementImageNerveCore M N
   hammockPathNerve := hammockPathNerveCore M N
+  hammockAdministrativeReduction := hammockAdministrativeReductionCore
   generatedTargetCategoricalEquivalence := generatedTargetEquivalence M N
   generatedTargetNerveEquivalence := generatedTargetNerveEquivalence M N
   generatedTargetHomotopyEquivalence :=
diff --git a/docs/en/RESEARCH_STATUS.md b/docs/en/RESEARCH_STATUS.md
index 3c6a3c2..3f0a103 100644
--- a/docs/en/RESEARCH_STATUS.md
+++ b/docs/en/RESEARCH_STATUS.md
@@ -414,9 +414,16 @@ universe replacement, generated paths are now categorically equivalent
 directly to each actual localization-target local hom-category; the direct
 nerve map has an explicit homotopy inverse and factors strictly through the
 linear comparison. Together with outer essential surjectivity this forms an
-audited `GeneratedHammockDwyerKanCore`. Competing-move coherence, reduced-
+audited `GeneratedHammockDwyerKanCore`. Raw critical-pair joinability, reduced-
 hammock invariance, standard weak-equivalence packaging, and the global
-Dwyer--Kan/Rezk theorem remain.
+Dwyer--Kan/Rezk theorem remain. A first raw administrative reduction layer is
+now compiled: vertical units, left-nested composition, adjacent refinement or
+aligned moves, executable refinement inverse pairs, and common-prefix
+administration reduce in every path context. The executable
+`nodeCount + leftWeight` complexity strictly decreases, giving well-founded
+termination and a semantics-preserving irreducible reduct for every path.
+Competing one-step moves agree in quotient semantics; raw joinability/local
+confluence and the remaining classical arbitrary-grid moves are still open.
 
 The actual construction has now begun with a computable presented syntax.
 `MarkedZigzag.Word` is endpoint-indexed, permits every source 1-cell forward,
diff --git a/docs/en/reference/AXIOMS.md b/docs/en/reference/AXIOMS.md
index d052958..6422eb8 100644
--- a/docs/en/reference/AXIOMS.md
+++ b/docs/en/reference/AXIOMS.md
@@ -1085,6 +1085,19 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.lean`.
 | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.allCells_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
 | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.all_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
 | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.semanticEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.ColumnRefinement.toHom_reverse` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.ColumnRefinement.toHom_comp_reverse` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.ColumnRefinement.toHom_reverse_comp` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.structural_decrease` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.complexity_lt` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.toHom_eq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.wellFounded` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.terminating` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.reduces_toHom_eq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.criticalPair_toHom_eq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.joinable_toHom_eq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.exists_irreducible` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.exists_irreducible_semantic` | `[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` |
@@ -1112,6 +1125,7 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.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.hammockAdministrativeReductionCore` | `[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` |
diff --git a/docs/en/reference/BLUEPRINT.md b/docs/en/reference/BLUEPRINT.md
index 6299d0d..921e24f 100644
--- a/docs/en/reference/BLUEPRINT.md
+++ b/docs/en/reference/BLUEPRINT.md
@@ -391,9 +391,10 @@ Every node in this graph is an existing compiled module.
 | 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; source structural and marked-pair generators normalize to executable refinements; both unitors and both associators normalize to explicit mutually inverse recursive paths; unconditional structural induction proves every raw cell normalizable; conjugating an arbitrary quotient representative yields a generated path for every linear quotient 2-cell, so the semantic functor is full, faithful, essentially surjective and a categorical equivalence, and its nerve comparison has an explicit simplicial homotopy inverse | PROVED |
+| 12 (generated hammock administrative reduction) | A directed raw-path reduction removes vertical units, right-associates composition, fuses adjacent refinement/aligned/common-prefix moves, cancels executable refinement inverses, and is closed under every path context; executable `nodeCount + leftWeight` complexity strictly decreases at every step, so the relation is well-founded and every path has an irreducible reduct; one-step and finite reductions preserve exact quotient semantics, and competing one-step moves agree semantically, while raw joinability/local confluence remains open | PROVED |
 | 12 (generated hammock Dwyer--Kan core) | Common-universe generated hammock mapping categories are categorically equivalent first to the independent linear hammock categories and then directly to the actual localization-target local hom-categories; both nerve comparisons have categorical-equivalence witnesses and explicit simplicial homotopy inverses, the direct target map factors strictly through the linear comparison, and outer essential surjectivity packages these results as an audited `GeneratedHammockDwyerKanCore` | 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) | Strengthen the proved project-local `GeneratedHammockDwyerKanCore` with critical-pair coherence and reduced-hammock homotopical invariance (or compare it to another accepted derived mapping-space construction), connect it to a standard weak-equivalence interface, and finish the standard global Dwyer--Kan/Rezk weak-equivalence and completeness theorem | OPEN_RESEARCH |
+| 12 (global cost-exact complete-Segal/Rezk equivalence) | Extend the proved terminating semantics-preserving administrative reduction to the full classical reduced arbitrary-grid move system; prove raw critical-pair joinability/local confluence and reduced-hammock homotopical invariance (or compare the generated core to another accepted derived mapping-space construction), connect the resulting `GeneratedHammockDwyerKanCore` to a standard weak-equivalence interface, and finish the standard global 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 7345de6..5c6d197 100644
--- a/docs/en/reference/CONJECTURES.md
+++ b/docs/en/reference/CONJECTURES.md
@@ -501,8 +501,14 @@ direct categorical equivalence from generated paths to the actual target
 local hom-category. Its nerve comparison has an explicit homotopy inverse and
 factors strictly through the independent linear comparison; outer essential
 surjectivity packages this as `GeneratedHammockDwyerKanCore`. Competing
-forward/marked moves, reduced-hammock moves, and their homotopical invariance
-remain open.
+forward/marked moves now have a first terminating administrative reduction
+layer: vertical units, left nesting, adjacent refinement/aligned/common-prefix
+administration, and executable refinement inverse pairs reduce under every
+path context. `nodeCount + leftWeight` strictly decreases, every path has an
+irreducible reduct, and all finite reductions preserve quotient semantics;
+every one-step critical pair is therefore semantically coherent. Raw
+joinability/local confluence, the additional classical arbitrary-grid 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.
@@ -617,8 +623,13 @@ source-composition/inverse, and equality-transport normalization cases are
 proved; all marked unit/counit, unitor, and associator cases are proved too.
 Every raw cell is therefore normalizable, every quotient 2-cell between linear
 rows is in the generated semantic image, and the generated path category is
-equivalent to the full linear mapping category. Critical-pair coherence and
-reduced-hammock invariance remain open.
+equivalent to the full linear mapping category. Its first directed
+administrative reduction is terminating by a strictly decreasing executable
+complexity, preserves semantics for arbitrary finite sequences, and supplies
+an irreducible reduct for every path. Competing one-step reductions agree in
+quotient semantics. Raw critical-pair joinability/local confluence, the full
+classical arbitrary-grid move system, 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
diff --git a/docs/en/reference/MODEL_MATRIX.md b/docs/en/reference/MODEL_MATRIX.md
index 6ae421d..cf44c29 100644
--- a/docs/en/reference/MODEL_MATRIX.md
+++ b/docs/en/reference/MODEL_MATRIX.md
@@ -681,5 +681,11 @@ categorical and nerve equivalence with an explicit homotopy inverse. Its
 common-universe replacement is directly equivalent to the actual target local
 hom-category, factors strictly through the linear comparison, and joins outer
 essential surjectivity in `GeneratedHammockDwyerKanCore`. Critical-pair
-coherence and reduced-hammock invariance remain open. These
+coherence and reduced-hammock invariance remain open. A first directed
+administrative reduction is nevertheless complete: its executable
+`nodeCount + leftWeight` complexity strictly decreases, every path reaches an
+irreducible reduct, all finite reductions preserve exact quotient semantics,
+and every one-step critical pair is semantically coherent. Raw joinability,
+local confluence, and the remaining classical arbitrary-grid moves are open.
+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 770b36a..49d29f2 100644
--- a/docs/eo/RESEARCH_STATUS.md
+++ b/docs/eo/RESEARCH_STATUS.md
@@ -389,6 +389,15 @@ nerva mapo havas eksplicitan homotopian inverson kaj strikte faktoriĝas tra la
 generita-al-lineara kaj lineara-al-cela komparoj. Kune kun ekstera esenca
 surĵeteco tio formas la kontrolitan `GeneratedHammockDwyerKanCore`.
 
+La unua kruda administra redukta tavolo ankaŭ kompiliĝas. Ĝi direktite
+forigas vertikalajn unuojn kaj maldekstran nestadon, kunfandas apudajn
+refinement/aligned-movojn kaj komun-prefiksan administradon, kaj nuligas
+plenumeblajn refinement-inversajn parojn en ĉiu voja kunteksto. La komputebla
+`nodeCount + leftWeight` strikte malpliiĝas je ĉiu paŝo; ĉiu vojo havas
+nereblan reduktaĵon kun la sama kvocienta semantiko. Konkuraj unupaŝaj movoj
+semantike konsentas, sed kruda kunigebleco, loka kunflueco kaj la ceteraj
+klasikaj arbitra-kradaj movoj restas malfermitaj.
+
 La fakta konstruo nun komenciĝas per komputebla prezenta sintakso.
 `MarkedZigzag.Word` estas fintipita per siaj ekstremoj, permesas ĉiun fontan
 1-ĉelon antaŭen kaj nur markitan sagon malantaŭen. Kunmeto, longo, unuaj kaj
diff --git a/docs/eo/reference/AXIOMS.md b/docs/eo/reference/AXIOMS.md
index ef03411..b7f7608 100644
--- a/docs/eo/reference/AXIOMS.md
+++ b/docs/eo/reference/AXIOMS.md
@@ -1087,6 +1087,19 @@ per `scripts/sync-doc-reference-tables.sh` kaj ne estu mane redaktataj.
 | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.allCells_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
 | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.all_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
 | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.semanticEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.ColumnRefinement.toHom_reverse` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.ColumnRefinement.toHom_comp_reverse` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.ColumnRefinement.toHom_reverse_comp` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.structural_decrease` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.complexity_lt` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.toHom_eq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.wellFounded` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.terminating` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.reduces_toHom_eq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.criticalPair_toHom_eq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.joinable_toHom_eq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.exists_irreducible` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.exists_irreducible_semantic` | `[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` |
@@ -1114,6 +1127,7 @@ per `scripts/sync-doc-reference-tables.sh` kaj ne estu mane redaktataj.
 | `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.hammockAdministrativeReductionCore` | `[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` |
diff --git a/docs/ja/RESEARCH_STATUS.md b/docs/ja/RESEARCH_STATUS.md
index a787a44..2550e39 100644
--- a/docs/ja/RESEARCH_STATUS.md
+++ b/docs/ja/RESEARCH_STATUS.md
@@ -155,6 +155,8 @@ fold は一意な解釈です。生成合同は全代数で健全で、木項モ
 
 生成 hammock 圏の common-universe 版は、実際の局所化対象の local hom-category と直接圏同値になりました。対応する nerve map は明示的ホモトピー逆を持ち、generated-to-linear と linear-to-target の二段階へ厳密に分解します。outer 本質全射性と合わせて、監査済み `GeneratedHammockDwyerKanCore` を構成します。
 
+最初の raw administrative reduction 層もコンパイルされました。垂直単位、左入れ子合成、隣接 refinement/aligned move、実行可能 refinement の正逆対、共通 prefix 管理を全 path 文脈で方向付けて簡約します。実行可能な `nodeCount + leftWeight` は各 step で厳密に減少するため良基で、各 path は商意味論を厳密に保つ既約 reduct を持ちます。競合する一段階 move は商意味論上一致しますが、raw joinability、局所合流性、残りの古典的任意 grid move は未解決です。
+
 異なる資源代数のモデルは順序付き加法準同型で比較できます。直列、並列、構造、予算則が再添字
 付けされ、異種強モデル射は資源写像とともに合成します。これらは、資源代数とモデルを対象、
 資源変換と強モデル射を 1-セル、資源変換の等号とモノイダル自然変換を 2-セルとする全双圏を
diff --git a/docs/ja/reference/AXIOMS.md b/docs/ja/reference/AXIOMS.md
index df87350..6c56815 100644
--- a/docs/ja/reference/AXIOMS.md
+++ b/docs/ja/reference/AXIOMS.md
@@ -1085,6 +1085,19 @@
 | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.allCells_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
 | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.all_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
 | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.semanticEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.ColumnRefinement.toHom_reverse` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.ColumnRefinement.toHom_comp_reverse` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.ColumnRefinement.toHom_reverse_comp` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.structural_decrease` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.complexity_lt` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.toHom_eq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.wellFounded` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.terminating` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.reduces_toHom_eq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.criticalPair_toHom_eq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.joinable_toHom_eq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.exists_irreducible` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.exists_irreducible_semantic` | `[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` |
@@ -1112,6 +1125,7 @@
 | `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.hammockAdministrativeReductionCore` | `[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` |
diff --git a/docs/zh-CN/RESEARCH_STATUS.md b/docs/zh-CN/RESEARCH_STATUS.md
index 1330102..f403778 100644
--- a/docs/zh-CN/RESEARCH_STATUS.md
+++ b/docs/zh-CN/RESEARCH_STATUS.md
@@ -148,6 +148,8 @@ quarter/half-flip 树分别实现为概率、保留相干的随机酉量子仪
 
 生成 hammock 范畴的 common-universe 版本现又直接范畴等价于实际局部化目标的 local hom-category；对应 nerve map 具有显式同伦逆，并严格分解为 generated-to-linear 与 linear-to-target 两步。它与 outer 本质满性共同组成经审计的 `GeneratedHammockDwyerKanCore`。
 
+第一层 raw administrative reduction 也已编译：纵向单位、左嵌套复合、相邻 refinement/aligned move、可执行 refinement 正逆对和公共前缀管理均可在所有路径上下文中定向约化。可执行复杂度 `nodeCount + leftWeight` 每步严格下降，因此关系良基且每条路径都有保持精确商语义的不可约 reduct。竞争单步在商语义中一致；raw joinability、局部合流与其余经典任意网格 moves 仍开放。
+
 模型比较不再要求全局使用同一资源代数。有序加法同态重索引串行、并行、结构和预算律；跨资源
 代数的强辫模型态射随同态复合，并在每个固定资源映射上形成单子自然变换的局部范畴。四维计算
 成本到 `Nat` 步数的投影可执行且有定理支持。
diff --git a/docs/zh-CN/reference/AXIOMS.md b/docs/zh-CN/reference/AXIOMS.md
index 8bae86b..3274438 100644
--- a/docs/zh-CN/reference/AXIOMS.md
+++ b/docs/zh-CN/reference/AXIOMS.md
@@ -1085,6 +1085,19 @@
 | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.allCells_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
 | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.all_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
 | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.semanticEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.ColumnRefinement.toHom_reverse` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.ColumnRefinement.toHom_comp_reverse` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.ColumnRefinement.toHom_reverse_comp` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.structural_decrease` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.complexity_lt` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.toHom_eq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.wellFounded` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.terminating` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.reduces_toHom_eq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.criticalPair_toHom_eq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.joinable_toHom_eq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.exists_irreducible` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.AdministrativeReduction.exists_irreducible_semantic` | `[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` |
@@ -1112,6 +1125,7 @@
 | `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.hammockAdministrativeReductionCore` | `[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` |