Add terminating generated hammock reductions

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` |

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
 

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

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.

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