From 6d6cbe42c4d7cc89b2305ff3fb8b7f9e9effb656 Mon Sep 17 00:00:00 2001 From: Amamiya Miu Date: Sat, 22 Aug 2026 18:38:34 +0800 Subject: [PATCH] feat(higher): normalize right unitor cells --- AXIOMS.md | 12 + BLUEPRINT.md | 4 +- CONJECTURES.md | 11 +- MODEL_MATRIX.md | 6 +- Ript/Audit/AxiomChecks.lean | 12 + .../MarkedZigzagAlignedHammock.lean | 267 +++++++++++++++++- .../Bicategory/MarkedZigzagLinearHammock.lean | 43 +++ Ript/Higher/CostExactZigzagMappingSpace.lean | 20 ++ docs/en/RESEARCH_STATUS.md | 7 +- docs/en/reference/AXIOMS.md | 12 + docs/en/reference/BLUEPRINT.md | 4 +- docs/en/reference/CONJECTURES.md | 11 +- docs/en/reference/MODEL_MATRIX.md | 6 +- docs/eo/RESEARCH_STATUS.md | 6 +- docs/eo/reference/AXIOMS.md | 12 + docs/ja/RESEARCH_STATUS.md | 2 +- docs/ja/reference/AXIOMS.md | 12 + docs/zh-CN/RESEARCH_STATUS.md | 2 +- docs/zh-CN/reference/AXIOMS.md | 12 + 19 files changed, 424 insertions(+), 37 deletions(-) diff --git a/AXIOMS.md b/AXIOMS.md index b8229b2..47bc4ff 100644 --- a/AXIOMS.md +++ b/AXIOMS.md @@ -1041,6 +1041,11 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.lean`. | `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_nil` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.leftUnitor_conjugation` | `[propext, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.leftUnitor_inv_conjugation` | `[propext, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_cons` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnit_step_coherence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnitor_conjugation` | `[propext, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnitor_inv_conjugation` | `[propext, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnit_inv_step_coherence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.ofEq` | `none` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.toHom_ofEq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_eq_of_rel` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | @@ -1048,6 +1053,13 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.lean`. | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_leftUnitorInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.leftUnitor_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.leftUnitorInv_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.toHom_rightUnitPath` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.toHom_rightUnitPathInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rightUnitPath_hom_inv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_rightUnitor` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_rightUnitorInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rightUnitor_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rightUnitorInv_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 306722c..2d4374c 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; pure bicategorical coherence identifies two-atomic-step normalization, so source composition/inverse normalize exactly to forward expansion/contraction; generic empty/two-atom formulas normalize marked unit/counit and inverses exactly to pair insertion/deletion; linear append right-unit/associativity equalities and computable equality paths are available, and left unitor/inverse normalize to identity via arbitrary-iso conjugation; `StructuralGeneratorNormalizable` now lists exactly four associator/right-unitor obligations and yields all-cell normalization by structural 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; generic empty/two-atom formulas normalize marked unit/counit and inverses exactly to pair insertion/deletion; linear append right-unit/associativity equalities and computable equality paths are available; left unitor/inverse normalize to identity via arbitrary-iso conjugation; recursive `rightUnitPath`/`rightUnitPathInv` give exact mutually inverse quotient semantics and normalize right unitor/inverse; `StructuralGeneratorNormalizable` now lists exactly the associator and inverse 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 four explicit `StructuralGeneratorNormalizable` fields for associator/inverse and right unitor/inverse; 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 two explicit `StructuralGeneratorNormalizable` fields for associator and inverse; 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 8cd288c..c0e5a21 100644 --- a/CONJECTURES.md +++ b/CONJECTURES.md @@ -475,8 +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 -has now shrunk to the four-field `StructuralGeneratorNormalizable` record: -associator and inverse plus right unitor and inverse. Source +has now shrunk to the two-field `StructuralGeneratorNormalizable` record: +associator and inverse. Recursive `rightUnitPath` and `rightUnitPathInv` +delete and insert a terminal empty row beneath every atomic prefix; their +quotient interpretations are mutually inverse, and raw right unitor/inverse +normalize exactly to them. Source composition/inverse are normalized exactly by executable forward expansion/contraction using the audited two-atomic-step coherence formula; generic empty/two-atom formulas now normalize marked unit/counit and @@ -595,8 +598,8 @@ 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, source-composition/inverse, and equality-transport normalization cases are -proved; all marked unit/counit and left-unitor cases are proved too. The -remaining four structural generator obligations are explicit and +proved; all marked unit/counit and both unitor cases are proved too. The +remaining two associator 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 e9a9595..d38fe16 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 structural/marked-pair/left-unitor/transport and closure cases are proved, and a four-field criterion implies all-cell normalization; those four associator/right-unitor 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 structural/marked-pair/left/right-unitor/transport and closure cases are proved, and a two-field associator criterion implies all-cell normalization; associator/inverse normalization, 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 @@ -674,8 +674,8 @@ 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 source-composition/inverse, equality-transport cases plus vertical/whiskering -closure are proved; all marked pair and left-unitor cases are proved too. Four -explicit associator and right-unitor obligations are +closure are proved; all marked pair and both unitor cases are proved too. Two +explicit associator 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 82ff8e7..dab9c12 100644 --- a/Ript/Audit/AxiomChecks.lean +++ b/Ript/Audit/AxiomChecks.lean @@ -1122,6 +1122,11 @@ set_option autoImplicit false #print axioms CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_nil #print axioms CategoryTheory.Bicategory.MarkedZigzag.LinearWord.leftUnitor_conjugation #print axioms CategoryTheory.Bicategory.MarkedZigzag.LinearWord.leftUnitor_inv_conjugation +#print axioms CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_cons +#print axioms CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnit_step_coherence +#print axioms CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnitor_conjugation +#print axioms CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnitor_inv_conjugation +#print axioms CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnit_inv_step_coherence #print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.ofEq #print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.toHom_ofEq #print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_eq_of_rel @@ -1129,6 +1134,13 @@ set_option autoImplicit false #print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_leftUnitorInv #print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.leftUnitor_normalizable #print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.leftUnitorInv_normalizable +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.toHom_rightUnitPath +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.toHom_rightUnitPathInv +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rightUnitPath_hom_inv +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_rightUnitor +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_rightUnitorInv +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rightUnitor_normalizable +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rightUnitorInv_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 ad31348..d5bd4ba 100644 --- a/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean +++ b/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean @@ -1882,6 +1882,12 @@ inductive HammockPath : ∀ {X Y : B}, (path : HammockPath first second) (post : LinearWord W Y Z) : HammockPath (LinearWord.append W first post) (LinearWord.append W second post) + /-- Whisker beneath one common atomic prefix step without introducing + singleton-row normalization comparisons. -/ + | under {X Y Z : B} (step : Step W X Y) + {first second : LinearWord W Y Z} + (path : HammockPath first second) : + HammockPath (.cons step first) (.cons step second) namespace HammockPath @@ -1898,6 +1904,8 @@ noncomputable def toHom {X Y : B} {first second : LinearWord W X Y} : | .ofAligned cell => AlignedCell.toHom W cell | .whiskerLeft pre path => normalizedWhiskerLeftHom W pre (toHom path) | .whiskerRight path post => normalizedWhiskerRightHom W post (toHom path) + | .under step path => + Presented.whiskerLeftHom W (Word.atom step) (toHom path) @[simp] theorem toHom_identity {X Y : B} (row : LinearWord W X Y) : @@ -1944,6 +1952,14 @@ theorem toHom_whiskerRight {X Y Z : B} normalizedWhiskerRightHom W post (toHom W path) := rfl +@[simp] +theorem toHom_under {X Y Z : B} (step : Step W X Y) + {first second : LinearWord W Y Z} + (path : HammockPath W first second) : + toHom W (.under step path) = + Presented.whiskerLeftHom W (Word.atom step) (toHom W path) := + rfl + /-- Horizontal append of two generated paths, implemented by right whiskering the first and left whiskering the second. -/ def append {X Y Z : B} @@ -1972,6 +1988,123 @@ theorem toHom_ofEq {X Y : B} {first second : LinearWord W X Y} subst second rfl +/-- Recursive generated path implementing the right-unit equation for a +linear row. -/ +def rightUnitPath {X Y : B} : + (row : LinearWord W X Y) → + HammockPath W (LinearWord.append W row (.nil Y)) row + | .nil X => .identity (.nil X) + | .cons step rest => .under step (rightUnitPath rest) + +/-- Recursive inverse generated path for the right-unit equation. -/ +def rightUnitPathInv {X Y : B} : + (row : LinearWord W X Y) → + HammockPath W row (LinearWord.append W row (.nil Y)) + | .nil X => .identity (.nil X) + | .cons step rest => .under step (rightUnitPathInv rest) + +/-- Recursive generated path implementing associativity of linear row +append. -/ +def associatorPath {X Y Z T : B} : + (first : LinearWord W X Y) → + (second : LinearWord W Y Z) → + (third : LinearWord W Z T) → + HammockPath W + (LinearWord.append W (LinearWord.append W first second) third) + (LinearWord.append W first (LinearWord.append W second third)) + | .nil _, second, third => .identity (LinearWord.append W second third) + | .cons step rest, second, third => + .under step (associatorPath rest second third) + +/-- Exact semantic formula for the recursive right-unit path. -/ +theorem toHom_rightUnitPath {X Y : B} (row : LinearWord W X Y) : + toHom W (rightUnitPath W row) = + AlignedCell.quotientVcomp W + (LinearWord.toWordAppendIso W row (.nil Y)).hom + (Presented.wordRightUnitorIso W (LinearWord.toWord W row)).hom := by + induction row with + | nil X => + change 𝟙 (Word.nil X) = + AlignedCell.quotientVcomp W + (Presented.wordLeftUnitorIso W (.nil X)).inv + (Presented.wordRightUnitorIso W (.nil X)).hom + have unitors : + (Presented.wordLeftUnitorIso W (.nil X)).inv = + (Presented.wordRightUnitorIso W (.nil X)).inv := by + change (λ_ (𝟙 (⟨X⟩ : Presented.Localization W))).inv = + (ρ_ (𝟙 (⟨X⟩ : Presented.Localization W))).inv + exact unitors_inv_equal + rw [unitors] + exact (Presented.wordRightUnitorIso W (.nil X)).inv_hom_id.symm + | @cons X Y Z step rest ih => + rw [LinearWord.toWordAppendIso_cons W step rest (.nil Z)] + simp only [rightUnitPath, LinearWord.append, toHom_under, + Iso.trans_hom, Bicategory.whiskerLeftIso, Iso.symm_hom] + rw [ih] + exact LinearWord.rightUnit_step_coherence + (C := Presented.Localization W) (Word.atom step) + (LinearWord.toWord W rest) + (LinearWord.toWordAppendIso W rest (.nil Z)).hom + +/-- Exact semantic formula for the inverse recursive right-unit path. -/ +theorem toHom_rightUnitPathInv {X Y : B} (row : LinearWord W X Y) : + toHom W (rightUnitPathInv W row) = + AlignedCell.quotientVcomp W + (Presented.wordRightUnitorIso W (LinearWord.toWord W row)).inv + (LinearWord.toWordAppendIso W row (.nil Y)).inv := by + induction row with + | nil X => + change 𝟙 (Word.nil X) = + AlignedCell.quotientVcomp W + (Presented.wordRightUnitorIso W (.nil X)).inv + (Presented.wordLeftUnitorIso W (.nil X)).hom + have unitors : + (Presented.wordRightUnitorIso W (.nil X)).inv = + (Presented.wordLeftUnitorIso W (.nil X)).inv := by + change (ρ_ (𝟙 (⟨X⟩ : Presented.Localization W))).inv = + (λ_ (𝟙 (⟨X⟩ : Presented.Localization W))).inv + exact unitors_inv_equal.symm + rw [unitors] + exact (Presented.wordLeftUnitorIso W (.nil X)).inv_hom_id.symm + | @cons X Y Z step rest ih => + rw [LinearWord.toWordAppendIso_cons W step rest (.nil Z)] + simp only [rightUnitPathInv, LinearWord.append, toHom_under, + Iso.trans_inv, Bicategory.whiskerLeftIso, Iso.symm_inv] + rw [ih] + exact (LinearWord.rightUnit_inv_step_coherence + (C := Presented.Localization W) (Word.atom step) + (LinearWord.toWord W rest) + (LinearWord.toWordAppendIso W rest (.nil Z)).inv).symm + +/-- The recursive right-unit path followed by its recursive inverse denotes +the identity on the row with a terminal empty suffix. -/ +theorem rightUnitPath_hom_inv {X Y : B} (row : LinearWord W X Y) : + AlignedCell.quotientVcomp W + (toHom W (rightUnitPath W row)) + (toHom W (rightUnitPathInv W row)) = + 𝟙 (LinearWord.toWord W + (LinearWord.append W row (.nil Y))) := by + induction row with + | nil X => + change (𝟙 (Word.nil X)) ≫ 𝟙 (Word.nil X) = 𝟙 (Word.nil X) + exact Category.id_comp _ + | @cons X Y Z step rest ih => + simp only [rightUnitPath, rightUnitPathInv, LinearWord.append, + toHom_under] + change AlignedCell.quotientVcomp W + (Presented.whiskerLeftHom W (Word.atom step) + (toHom W (rightUnitPath W rest))) + (Presented.whiskerLeftHom W (Word.atom step) + (toHom W (rightUnitPathInv W rest))) = + 𝟙 (Word.append (W := W) (Word.atom step) + (LinearWord.toWord W + (LinearWord.append W rest (.nil Z)))) + rw [← AlignedCell.whiskerLeftHom_vcomp W (Word.atom step)] + rw [ih] + exact Quot.sound (Presented.Rel.whisker_left_id + (Word.atom step) + (LinearWord.toWord W (LinearWord.append W rest (.nil Z)))) + /-- Exact quotient interpretation of horizontal path append. -/ @[simp] theorem toHom_append {X Y Z : B} @@ -2036,6 +2169,17 @@ theorem rel_whiskerRight {X Y Z : B} normalizedWhiskerRightHom W post (toHom W beta) rw [equality] +/-- Semantic equality is stable beneath an atomic prefix step. -/ +theorem rel_under {X Y Z : B} (step : Step W X Y) + {first second : LinearWord W Y Z} + {alpha beta : HammockPath W first second} + (equality : Rel W alpha beta) : + Rel W (.under step alpha) (.under step beta) := by + unfold Rel at equality ⊢ + change Presented.whiskerLeftHom W (Word.atom step) (toHom W alpha) = + Presented.whiskerLeftHom W (Word.atom step) (toHom W beta) + rw [equality] + /-- Semantic equality is stable under horizontal append. -/ theorem rel_append {X Y Z : B} {firstSource firstTarget : LinearWord W X Y} @@ -2759,6 +2903,99 @@ theorem normalizedCellHom_leftUnitorInv {X Y : B} (word : Word W X Y) : normalizedCellHom_id] at relationEquality exact (AlignedCell.quotientVcomp_comp_id W _).symm.trans relationEquality +/-- Raw right unitor normalizes to the recursive generated path deleting the +terminal empty row. -/ +@[simp] +theorem normalizedCellHom_rightUnitor {X Y : B} (word : Word W X Y) : + normalizedCellHom W (Cell.rightUnitor (W := W) word) = + toHom W (rightUnitPath W (LinearWord.flatten W word)) := by + unfold normalizedCellHom normalizedHom + simp only [Word.append_eq_comp, LinearWord.flatten_append] + rw [LinearWord.normalizationIso_append W word (.nil Y)] + rw [LinearWord.normalizationIso_nil W Y] + simp only [LinearWord.flatten_nil, Iso.trans_inv, Iso.symm_inv] + unfold LinearWord.appendIso + simp only [Iso.trans_inv, Bicategory.whiskerLeftIso, + Bicategory.whiskerRightIso] + let iso := LinearWord.normalizationIso W word + let comparison := LinearWord.toWordAppendIso W + (LinearWord.flatten W word) (.nil Y) + change AlignedCell.quotientVcomp W + (AlignedCell.quotientVcomp W comparison.hom + (AlignedCell.quotientVcomp W + (Presented.whiskerLeftHom W + (LinearWord.toWord W (LinearWord.flatten W word)) + (𝟙 (LinearWord.toWord W (.nil Y)))) + (Presented.whiskerRightHom W + (LinearWord.toWord W (.nil Y)) iso.inv))) + (AlignedCell.quotientVcomp W + (Presented.wordRightUnitorIso W word).hom iso.hom) = + toHom W (rightUnitPath W (LinearWord.flatten W word)) + have leftIdentity : + Presented.whiskerLeftHom W + (LinearWord.toWord W (LinearWord.flatten W word)) + (𝟙 (LinearWord.toWord W (.nil Y))) = + 𝟙 (Word.append (W := W) + (LinearWord.toWord W (LinearWord.flatten W word)) + (LinearWord.toWord W (.nil Y))) := + Quot.sound (Presented.Rel.whisker_left_id + (LinearWord.toWord W (LinearWord.flatten W word)) + (LinearWord.toWord W (.nil Y))) + rw [leftIdentity, AlignedCell.quotientVcomp_id_comp] + simp only [AlignedCell.quotientVcomp_assoc] + have conjugation : + AlignedCell.quotientVcomp W + (Presented.whiskerRightHom W + (LinearWord.toWord W (.nil Y)) iso.inv) + (AlignedCell.quotientVcomp W + (Presented.wordRightUnitorIso W word).hom iso.hom) = + (Presented.wordRightUnitorIso W + (LinearWord.toWord W (LinearWord.flatten W word))).hom := by + change (iso.inv ▷ 𝟙 (⟨Y⟩ : Presented.Localization W)) ≫ + (ρ_ word).hom ≫ iso.hom = _ + exact LinearWord.rightUnitor_conjugation + (C := Presented.Localization W) iso + rw [conjugation] + exact (toHom_rightUnitPath W (LinearWord.flatten W word)).symm + +/-- Raw inverse right unitor normalizes to the inverse recursive generated +path inserting a terminal empty row. -/ +@[simp] +theorem normalizedCellHom_rightUnitorInv {X Y : B} (word : Word W X Y) : + normalizedCellHom W (Cell.rightUnitorInv (W := W) word) = + toHom W (rightUnitPathInv W (LinearWord.flatten W word)) := by + let row := LinearWord.flatten W word + let forward := toHom W (rightUnitPath W row) + let inverse := toHom W (rightUnitPathInv W row) + let candidate : Presented.Hom W + (LinearWord.toWord W row) + (LinearWord.toWord W (LinearWord.append W row (.nil Y))) := + normalizedCellHom W (Cell.rightUnitorInv (W := W) word) + have forwardInverse : + forward ≫ inverse = + 𝟙 (LinearWord.toWord W (LinearWord.append W row (.nil Y))) := by + exact rightUnitPath_hom_inv W row + have relationEquality : + candidate ≫ forward = + 𝟙 (LinearWord.toWord W row) := by + have equality := normalizedCellHom_eq_of_rel W + (Presented.Rel.right_unitor_inv_hom (W := W) word) + rw [normalizedCellHom_vcomp, normalizedCellHom_rightUnitor, + normalizedCellHom_id] at equality + exact equality + change candidate = inverse + calc + candidate = candidate ≫ + 𝟙 (LinearWord.toWord W + (LinearWord.append W row (.nil Y))) := by + exact (AlignedCell.quotientVcomp_comp_id W candidate).symm + _ = candidate ≫ (forward ≫ inverse) := by + rw [forwardInverse] + _ = (candidate ≫ forward) ≫ inverse := (Category.assoc _ _ _).symm + _ = 𝟙 (LinearWord.toWord W row) ≫ inverse := by + rw [relationEquality] + _ = inverse := AlignedCell.quotientVcomp_id_comp W inverse + /-- Equality transport does not change normalized quotient semantics. -/ @[simp] theorem normalizedCellHom_transport {X Y : B} @@ -2941,6 +3178,20 @@ theorem leftUnitorInv_normalizable {X Y : B} (word : Word W X Y) : rw [Normalizable, normalizedCellHom_leftUnitorInv] exact ⟨.identity (LinearWord.flatten W word), rfl⟩ +/-- Right unitor is hammock-normalizable by the recursive terminal-empty-row +deletion path. -/ +theorem rightUnitor_normalizable {X Y : B} (word : Word W X Y) : + Normalizable W (Cell.rightUnitor (W := W) word) := by + rw [Normalizable, normalizedCellHom_rightUnitor] + exact ⟨rightUnitPath W (LinearWord.flatten W word), rfl⟩ + +/-- Inverse right unitor is hammock-normalizable by the recursive +terminal-empty-row insertion path. -/ +theorem rightUnitorInv_normalizable {X Y : B} (word : Word W X Y) : + Normalizable W (Cell.rightUnitorInv (W := W) word) := by + rw [Normalizable, normalizedCellHom_rightUnitorInv] + exact ⟨rightUnitPathInv W (LinearWord.flatten W word), rfl⟩ + /-- Equality transport preserves raw-cell normalizability. -/ theorem transport_normalizable {X Y : B} {first second first' second' : Word W X Y} @@ -2953,10 +3204,8 @@ theorem transport_normalizable {X Y : B} exact member /-- Exact remaining generator obligations for a complete raw-cell -normalization induction. Identity, vertical composition, original cells, -source identities, source composition, marked pairs, both whiskerings, and -left unitors, plus equality transport are already -discharged separately. -/ +normalization induction. Only the binary associator and its inverse remain; +all other raw generators and closure operations are discharged separately. -/ structure StructuralGeneratorNormalizable : Prop where /-- Binary associator. -/ associator : ∀ {X Y Z T : B} (first : Word W X Y) @@ -2966,12 +3215,6 @@ structure StructuralGeneratorNormalizable : Prop where associatorInv : ∀ {X Y Z T : B} (first : Word W X Y) (second : Word W Y Z) (third : Word W Z T), Normalizable W (Cell.associatorInv (W := W) first second third) - /-- Binary right unitor. -/ - rightUnitor : ∀ {X Y : B} (word : Word W X Y), - Normalizable W (Cell.rightUnitor (W := W) word) - /-- Inverse binary right unitor. -/ - rightUnitorInv : ∀ {X Y : B} (word : Word W X Y), - Normalizable W (Cell.rightUnitorInv (W := W) word) /-- Complete raw-cell normalization follows by structural induction from the remaining explicit structural-generator obligations. -/ @@ -3005,8 +3248,8 @@ theorem normalizable_of_structuralGenerators exact generators.associatorInv first second third | leftUnitor word => exact leftUnitor_normalizable W word | leftUnitorInv word => exact leftUnitorInv_normalizable W word - | rightUnitor word => exact generators.rightUnitor word - | rightUnitorInv word => exact generators.rightUnitorInv word + | rightUnitor word => exact rightUnitor_normalizable W word + | rightUnitorInv word => exact rightUnitorInv_normalizable W word | transport sourceEquality targetEquality cell member => exact transport_normalizable W sourceEquality targetEquality member diff --git a/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean b/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean index 1b4b008..645f647 100644 --- a/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean +++ b/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean @@ -184,6 +184,16 @@ theorem toWordAppendIso_nil {X Y : B} (second : LinearWord W X Y) : (Presented.wordLeftUnitorIso W (toWord W second)).symm := rfl +/-- Recursive equation for the append comparison under one leading step. -/ +theorem toWordAppendIso_cons {X Y Z T : B} (step : Step W X Y) + (rest : LinearWord W Y Z) (second : LinearWord W Z T) : + toWordAppendIso W (.cons step rest) second = + whiskerLeftIso (B := Presented.Localization W) (Word.atom step) + (toWordAppendIso W rest second) ≪≫ + (Presented.wordAssociatorIso W + (Word.atom step) (toWord W rest) (toWord W second)).symm := + rfl + /-- 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) @@ -287,6 +297,39 @@ theorem leftUnitor_inv_conjugation {C : Type u} [Bicategory.{w, v} C] (λ_ second).hom = 𝟙 second := by simp +/-- Coherence step for recursively transporting a right-unit comparison +beneath one leading 1-morphism. -/ +theorem rightUnit_step_coherence {C : Type u} [Bicategory.{w, v} C] + {X Y Z : C} (first : X ⟶ Y) (second : Y ⟶ Z) + {source : Y ⟶ Z} (comparison : source ⟶ second ≫ 𝟙 Z) : + first ◁ (comparison ≫ (ρ_ second).hom) = + (first ◁ comparison ≫ (α_ first second (𝟙 Z)).inv) ≫ + (ρ_ (first ≫ second)).hom := by + simp + +/-- Right-unitor naturality along an arbitrary isomorphism. -/ +theorem rightUnitor_conjugation {C : Type u} [Bicategory.{w, v} C] + {X Y : C} {first second : X ⟶ Y} (iso : first ≅ second) : + (iso.inv ▷ 𝟙 Y) ≫ (ρ_ first).hom ≫ iso.hom = + (ρ_ second).hom := by + simp + +/-- Inverse right-unitor naturality along an arbitrary isomorphism. -/ +theorem rightUnitor_inv_conjugation {C : Type u} [Bicategory.{w, v} C] + {X Y : C} {first second : X ⟶ Y} (iso : first ≅ second) : + iso.inv ≫ (ρ_ first).inv ≫ (iso.hom ▷ 𝟙 Y) = + (ρ_ second).inv := by + simp + +/-- Coherence step for the inverse recursive right-unit path. -/ +theorem rightUnit_inv_step_coherence {C : Type u} [Bicategory.{w, v} C] + {X Y Z : C} (first : X ⟶ Y) (second : Y ⟶ Z) + {target : Y ⟶ Z} (comparison : second ≫ 𝟙 Z ⟶ target) : + (ρ_ (first ≫ second)).inv ≫ (α_ first second (𝟙 Z)).hom ≫ + (first ◁ comparison) = + first ◁ ((ρ_ second).inv ≫ comparison) := by + simp + /-- 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} diff --git a/Ript/Higher/CostExactZigzagMappingSpace.lean b/Ript/Higher/CostExactZigzagMappingSpace.lean index 0e47709..9f8c341 100644 --- a/Ript/Higher/CostExactZigzagMappingSpace.lean +++ b/Ript/Higher/CostExactZigzagMappingSpace.lean @@ -1447,6 +1447,20 @@ structure HammockRawCellNormalizationCore : Prop where (costExactArrows R) (Bicategory.MarkedZigzag.Cell.leftUnitorInv (W := costExactArrows R) word) + /-- Right unitor is normalizable. -/ + rightUnitor : ∀ {M N : ProcessModel.{u, v, w} R} + (word : CostExactZigzag.Word (R := R) M N), + Bicategory.MarkedZigzag.HammockPath.Normalizable + (costExactArrows R) + (Bicategory.MarkedZigzag.Cell.rightUnitor + (W := costExactArrows R) word) + /-- Inverse right unitor is normalizable. -/ + rightUnitorInv : ∀ {M N : ProcessModel.{u, v, w} R} + (word : CostExactZigzag.Word (R := R) M N), + Bicategory.MarkedZigzag.HammockPath.Normalizable + (costExactArrows R) + (Bicategory.MarkedZigzag.Cell.rightUnitorInv + (W := costExactArrows R) word) /-- Raw left whiskering preserves normalizability. -/ whiskerLeft : ∀ (M N P : ProcessModel.{u, v, w} R) (pre : CostExactZigzag.Word (R := R) M N) @@ -1536,6 +1550,12 @@ theorem hammockRawCellNormalizationCore : leftUnitorInv := fun word => Bicategory.MarkedZigzag.HammockPath.leftUnitorInv_normalizable (costExactArrows R) word + rightUnitor := fun word => + Bicategory.MarkedZigzag.HammockPath.rightUnitor_normalizable + (costExactArrows R) word + rightUnitorInv := fun word => + Bicategory.MarkedZigzag.HammockPath.rightUnitorInv_normalizable + (costExactArrows R) word 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 edd125e..9832746 100644 --- a/docs/en/RESEARCH_STATUS.md +++ b/docs/en/RESEARCH_STATUS.md @@ -402,9 +402,10 @@ coherence formula. Generic empty/two-atom formulas now normalize marked unit/counit and inverses exactly to pair insertion/deletion. These structural obligations are further reduced: computable linear append right-unit/associativity equalities and equality paths are available, and left -unitor/inverse normalize to identity by arbitrary-iso conjugation. The -remaining four associator/right-unitor obligations already imply all-cell -normalization conditionally, +unitor/inverse normalize to identity by arbitrary-iso conjugation. Recursive +terminal-empty-row paths now normalize right unitor/inverse exactly, with +mutually inverse quotient semantics. The remaining two associator/inverse +obligations already imply all-cell normalization conditionally, but are not assumed unconditionally. Semantic fullness, competing-move coherence, reduced-hammock invariance, standard weak-equivalence packaging, and the global Dwyer--Kan/Rezk theorem remain. diff --git a/docs/en/reference/AXIOMS.md b/docs/en/reference/AXIOMS.md index 7b01d15..e33c28e 100644 --- a/docs/en/reference/AXIOMS.md +++ b/docs/en/reference/AXIOMS.md @@ -1041,6 +1041,11 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.lean`. | `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_nil` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.leftUnitor_conjugation` | `[propext, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.leftUnitor_inv_conjugation` | `[propext, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_cons` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnit_step_coherence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnitor_conjugation` | `[propext, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnitor_inv_conjugation` | `[propext, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnit_inv_step_coherence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.ofEq` | `none` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.toHom_ofEq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_eq_of_rel` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | @@ -1048,6 +1053,13 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.lean`. | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_leftUnitorInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.leftUnitor_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.leftUnitorInv_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.toHom_rightUnitPath` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.toHom_rightUnitPathInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rightUnitPath_hom_inv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_rightUnitor` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_rightUnitorInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rightUnitor_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rightUnitorInv_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 3da79ab..374486e 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; pure bicategorical coherence identifies two-atomic-step normalization, so source composition/inverse normalize exactly to forward expansion/contraction; generic empty/two-atom formulas normalize marked unit/counit and inverses exactly to pair insertion/deletion; linear append right-unit/associativity equalities and computable equality paths are available, and left unitor/inverse normalize to identity via arbitrary-iso conjugation; `StructuralGeneratorNormalizable` now lists exactly four associator/right-unitor obligations and yields all-cell normalization by structural 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; generic empty/two-atom formulas normalize marked unit/counit and inverses exactly to pair insertion/deletion; linear append right-unit/associativity equalities and computable equality paths are available; left unitor/inverse normalize to identity via arbitrary-iso conjugation; recursive `rightUnitPath`/`rightUnitPathInv` give exact mutually inverse quotient semantics and normalize right unitor/inverse; `StructuralGeneratorNormalizable` now lists exactly the associator and inverse 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 four explicit `StructuralGeneratorNormalizable` fields for associator/inverse and right unitor/inverse; 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 two explicit `StructuralGeneratorNormalizable` fields for associator and inverse; 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 2d3d0cc..fdccb8b 100644 --- a/docs/en/reference/CONJECTURES.md +++ b/docs/en/reference/CONJECTURES.md @@ -475,8 +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 -has now shrunk to the four-field `StructuralGeneratorNormalizable` record: -associator and inverse plus right unitor and inverse. Source +has now shrunk to the two-field `StructuralGeneratorNormalizable` record: +associator and inverse. Recursive `rightUnitPath` and `rightUnitPathInv` +delete and insert a terminal empty row beneath every atomic prefix; their +quotient interpretations are mutually inverse, and raw right unitor/inverse +normalize exactly to them. Source composition/inverse are normalized exactly by executable forward expansion/contraction using the audited two-atomic-step coherence formula; generic empty/two-atom formulas now normalize marked unit/counit and @@ -595,8 +598,8 @@ 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, source-composition/inverse, and equality-transport normalization cases are -proved; all marked unit/counit and left-unitor cases are proved too. The -remaining four structural generator obligations are explicit and +proved; all marked unit/counit and both unitor cases are proved too. The +remaining two associator 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 df45c43..a454cc9 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 structural/marked-pair/left-unitor/transport and closure cases are proved, and a four-field criterion implies all-cell normalization; those four associator/right-unitor 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 structural/marked-pair/left/right-unitor/transport and closure cases are proved, and a two-field associator criterion implies all-cell normalization; associator/inverse normalization, 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 @@ -674,8 +674,8 @@ 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 source-composition/inverse, equality-transport cases plus vertical/whiskering -closure are proved; all marked pair and left-unitor cases are proved too. Four -explicit associator and right-unitor obligations are +closure are proved; all marked pair and both unitor cases are proved too. Two +explicit associator 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 5ed0384..e00ff86 100644 --- a/docs/eo/RESEARCH_STATUS.md +++ b/docs/eo/RESEARCH_STATUS.md @@ -372,8 +372,10 @@ du-atoma kohereco kaj ekzakta forward expand/contract. Ĝeneralaj malplena- vorto/du-atoma-ciklo formuloj normaligas markitajn unit/counit kaj inversojn per ekzakta para enmeto/forigo. Linearaj append-right-unit/asocieco kaj komputeblaj egalecvojoj estas aldonitaj; left-unitor kaj inverso normaligas al -identeco per arbitra-izomorfia konjugacio. La ceteraj kvar asociatoraj kaj -right-unitoraj generatoraj kampoj estas eksplicitaj kaj kondiĉe +identeco per arbitra-izomorfia konjugacio. Rekursiaj vojoj por forigi/enmeti +finan malplenan vicon nun ekzakte normaligas right-unitor kaj ĝian inverson, +kaj iliaj kvocientaj semantikoj estas reciproke inversaj. La ceteraj du +asociatoraj 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 17c2050..f6bafdf 100644 --- a/docs/eo/reference/AXIOMS.md +++ b/docs/eo/reference/AXIOMS.md @@ -1043,6 +1043,11 @@ per `scripts/sync-doc-reference-tables.sh` kaj ne estu mane redaktataj. | `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_nil` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.leftUnitor_conjugation` | `[propext, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.leftUnitor_inv_conjugation` | `[propext, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_cons` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnit_step_coherence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnitor_conjugation` | `[propext, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnitor_inv_conjugation` | `[propext, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnit_inv_step_coherence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.ofEq` | `none` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.toHom_ofEq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_eq_of_rel` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | @@ -1050,6 +1055,13 @@ per `scripts/sync-doc-reference-tables.sh` kaj ne estu mane redaktataj. | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_leftUnitorInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.leftUnitor_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.leftUnitorInv_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.toHom_rightUnitPath` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.toHom_rightUnitPathInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rightUnitPath_hom_inv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_rightUnitor` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_rightUnitorInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rightUnitor_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rightUnitorInv_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 a953ea8..b085395 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/逆、source composition/逆、transport、および垂直/whiskering 閉包分岐が完成しました。source composition の正逆は純双圏二原子コヒーレンス式により forward expand/contract と厳密に一致し、一般の空 word/二原子閉路式により marked unit/counit とその逆も pair insert/delete と厳密に一致します。linear append の right-unit/associativity 等式と計算可能な equality path が追加され、left unitor とその逆は任意同型の共役消去により恒等へ正規化されます。残る四の associator 正逆と right 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 と厳密に一致し、一般の空 word/二原子閉路式により marked unit/counit とその逆も pair insert/delete と厳密に一致します。linear append の right-unit/associativity 等式と計算可能な equality path が追加され、left unitor とその逆は任意同型の共役消去により恒等へ正規化されます。末尾空行を削除/挿入する再帰的 path が right unitor とその逆を厳密に正規化し、両 path の商意味論は互いに逆です。`StructuralGeneratorNormalizable` には associator 正逆の二フィールドだけが残り、条件付きで全 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 ddf5d9f..46c8655 100644 --- a/docs/ja/reference/AXIOMS.md +++ b/docs/ja/reference/AXIOMS.md @@ -1041,6 +1041,11 @@ | `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_nil` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.leftUnitor_conjugation` | `[propext, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.leftUnitor_inv_conjugation` | `[propext, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_cons` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnit_step_coherence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnitor_conjugation` | `[propext, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnitor_inv_conjugation` | `[propext, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnit_inv_step_coherence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.ofEq` | `none` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.toHom_ofEq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_eq_of_rel` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | @@ -1048,6 +1053,13 @@ | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_leftUnitorInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.leftUnitor_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.leftUnitorInv_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.toHom_rightUnitPath` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.toHom_rightUnitPathInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rightUnitPath_hom_inv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_rightUnitor` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_rightUnitorInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rightUnitor_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rightUnitorInv_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 6df708c..03710a1 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/逆、source composition/逆、transport 及纵向/whiskering 闭包分支均已完成。source composition 正反方向通过纯双范畴两原子协调公式精确对应 forward expand/contract；通用空 word/两原子闭环公式又将 marked unit/counit 及其逆精确对应 pair insert/delete。线性 append 的右单位/结合等式与可计算 equality path 已建立，left unitor 及其逆通过任意同构共轭精确正规化为恒等。剩余四个 associator 正反与 right 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；通用空 word/两原子闭环公式又将 marked unit/counit 及其逆精确对应 pair insert/delete。线性 append 的右单位/结合等式与可计算 equality path 已建立，left unitor 及其逆通过任意同构共轭精确正规化为恒等。递归的终端空行删除/插入路径现精确正规化 right unitor 及其逆，并且两条路径的商语义互逆。`StructuralGeneratorNormalizable` 只剩 associator 正反两个字段，它们在条件下推出全部 raw Cell 正规化，但尚未无条件证明；semantic fullness、critical-pair 协调、约化 hammock 不变性及标准弱等价封装仍开放。 模型比较不再要求全局使用同一资源代数。有序加法同态重索引串行、并行、结构和预算律；跨资源 代数的强辫模型态射随同态复合，并在每个固定资源映射上形成单子自然变换的局部范畴。四维计算 diff --git a/docs/zh-CN/reference/AXIOMS.md b/docs/zh-CN/reference/AXIOMS.md index 714ff97..faa9a29 100644 --- a/docs/zh-CN/reference/AXIOMS.md +++ b/docs/zh-CN/reference/AXIOMS.md @@ -1041,6 +1041,11 @@ | `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_nil` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.leftUnitor_conjugation` | `[propext, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.leftUnitor_inv_conjugation` | `[propext, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.toWordAppendIso_cons` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnit_step_coherence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnitor_conjugation` | `[propext, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnitor_inv_conjugation` | `[propext, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.rightUnit_inv_step_coherence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.ofEq` | `none` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.toHom_ofEq` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_eq_of_rel` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | @@ -1048,6 +1053,13 @@ | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_leftUnitorInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.leftUnitor_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.leftUnitorInv_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.toHom_rightUnitPath` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.toHom_rightUnitPathInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rightUnitPath_hom_inv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_rightUnitor` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_rightUnitorInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rightUnitor_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rightUnitorInv_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` |