diff --git a/AXIOMS.md b/AXIOMS.md index b4533d8..e1c85f8 100644 --- a/AXIOMS.md +++ b/AXIOMS.md @@ -970,15 +970,29 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.lean`. | `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_essSurj` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.semanticFunctor_factorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_vcomp` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.semanticFunctor_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinementFunctor_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_vcomp` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.semanticFunctor_faithful` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinementFunctor_faithful` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinementSemanticFunctor_factorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.inSemanticImage_iff_exists_map` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinement_mem_semanticImage` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.aligned_mem_semanticImage` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.inSemanticImage_iff_exists_map` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinement_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.aligned_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.originalAlignedCell_toHom` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.originalCell_mem_semanticImage` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.originalCell_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedWhiskerLeftHom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedWhiskerRightHom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_whiskerLeft` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_whiskerRight` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_append` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerLeft_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerRight_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.append_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_id` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_vcomp` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_original` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.identity_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.vcomp_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.original_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `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` | @@ -998,6 +1012,10 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.lean`. | `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_originalEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_hammockFactorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.hammockPathNerveCore` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_whiskerLeftEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_whiskerRightEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_appendEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathWhiskeringCore` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.core` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `CategoryTheory.Pseudofunctor.homotopyFunctor` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/PseudofunctorHomotopy.lean` | | `CategoryTheory.Pseudofunctor.homotopyFunctor_map_homMk` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/PseudofunctorHomotopy.lean` | diff --git a/BLUEPRINT.md b/BLUEPRINT.md index 42b3c0c..1e5e4c9 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; its semantic functor into the full linear mapping category is faithful and object-essentially-surjective, the refinement-path groupoid embeds faithfully and factors strictly through it, every aligned cell lies in its exact semantic image, and every source 2-cell has a canonical one-column representative equal to the original quotient cell conjugated by right-unitors; the induced cost-exact nerve maps have exact refinement/aligned/source-edge formulas | PROVED | +| 12 (aligned-cell-augmented hammock paths) | A non-groupoidal generated path syntax alternates executable refinements with arbitrary aligned raw 2-cells and vertical composition, then quotients only by equality of quotient-cell semantics; normalized left/right whiskering enters and leaves binary append through canonical linear-normal-form isomorphisms, horizontal append composes those operations, and semantic equality/image membership are closed under all three; the semantic functor is faithful and object-essentially-surjective, refinement paths embed faithfully and factor strictly, every source 2-cell has a canonical one-column representative, raw identity/original cells are normalizable and normalizability is closed under vertical composition; cost-exact three-model nerve maps have exact whiskering/append edge formulas | PROVED | | 12 (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) | Normalize every presented quotient 2-cell into alternating aligned-cell/refinement hammock paths (or characterize the remaining missing generators), 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) | Prove normalization-isomorphism naturality for raw left/right whiskering, normalize the remaining structural raw-cell generators and hence every presented quotient 2-cell into alternating aligned-cell/refinement hammock paths, prove critical-pair coherence and reduced-hammock homotopical invariance (or compare the generated path category to another accepted derived mapping-space construction), connect that comparison to a standard weak-equivalence interface, and finish the standard Dwyer--Kan/Rezk weak-equivalence and completeness theorem | OPEN_RESEARCH | ## Finite deterministic copy-discard theorem records diff --git a/CONJECTURES.md b/CONJECTURES.md index af43ace..2ddcce3 100644 --- a/CONJECTURES.md +++ b/CONJECTURES.md @@ -468,11 +468,14 @@ through it strictly. A larger non-groupoidal path category now alternates refinements with arbitrary aligned raw 2-cells. Its semantics is faithful, the refinement subsystem embeds faithfully and factors strictly, and every source 2-cell has a canonical one-column representative whose quotient semantics is -the original 2-cell conjugated by right-unitors. The remaining classical gap -is normalizing every presented quotient 2-cell into these alternating paths -(or identifying the missing generators), together with coherence for -competing forward/marked moves, reduced-hammock moves, and their homotopical -invariance. +the original 2-cell conjugated by right-unitors. The path calculus is now +closed under normalized left/right whiskering and horizontal append, with +exact cost-exact three-model nerve formulas. Raw identities and original cells +are normalizable, and normalizability is closed under vertical composition. +The next missing induction law is naturality of the chosen normalization +isomorphisms with raw whiskering; after it, the remaining structural generators +must be normalized before fullness can be claimed. Competing forward/marked +moves, reduced-hammock moves, and their homotopical invariance remain open. 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. @@ -577,9 +580,12 @@ and simplicially equivalent to the exact subgroupoid of refinement-generated quotient 2-cells, which includes faithfully in the full linear mapping category and strictly factors the semantic nerve map. The aligned-cell- augmented path category now adds arbitrary pointwise raw cells, contains every -source 2-cell in one-column form, and strictly extends refinement paths. -Normalization of all presented quotient 2-cells into this generated category, -critical-pair coherence, and reduced-hammock invariance remain open. +source 2-cell in one-column form, strictly extends refinement paths, and is +closed under normalized left/right whiskering and horizontal append. Identity, +vertical-composite, and original-cell normalization cases are proved. +Normalization-isomorphism naturality for raw whiskering and the remaining +structural generators, critical-pair coherence, and reduced-hammock invariance +remain open. The first complete construction against that predicate is now kernel checked. Identity precomposition is an adjoint equivalence of pseudofunctors and an diff --git a/MODEL_MATRIX.md b/MODEL_MATRIX.md index 1eaf153..f263d32 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 with strict refinement-nerve factorization are proved; normalization of every presented quotient 2-cell into the generated hammock paths, 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, closed under normalized left/right whiskering and horizontal append, with exact three-model nerve formulas and proved identity/vertical/original raw-cell normalization cases are proved; normalization-isomorphism naturality for raw whiskering, the remaining structural-cell normalization cases, 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 @@ -670,7 +670,9 @@ subgroupoid equivalent to the path groupoid, with a faithful inclusion into the full linear mapping category and a strictly factored semantic nerve map. The aligned-cell-augmented non-groupoidal path category now adds arbitrary pointwise raw cells, contains every source 2-cell in canonical one-column form, -and strictly extends the refinement path nerve. What remains is normalization -of every presented quotient 2-cell into these generated paths, critical-pair -coherence, and reduced-hammock invariance. These +strictly extends the refinement path nerve, and is closed under normalized +left/right whiskering and horizontal append. Raw identities and original cells +are normalizable and vertical composition preserves normalizability. What +remains is normalization-isomorphism naturality for raw whiskering, the other +structural generators, 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 2fae6f3..bc697ac 100644 --- a/Ript/Audit/AxiomChecks.lean +++ b/Ript/Audit/AxiomChecks.lean @@ -1060,6 +1060,20 @@ set_option autoImplicit false #print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.aligned_mem_semanticImage #print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.originalAlignedCell_toHom #print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.originalCell_mem_semanticImage +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedWhiskerLeftHom +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedWhiskerRightHom +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_whiskerLeft +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_whiskerRight +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_append +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerLeft_mem_semanticImage +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerRight_mem_semanticImage +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.append_mem_semanticImage +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_id +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_vcomp +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_original +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.identity_normalizable +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.vcomp_normalizable +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.original_normalizable #print axioms Ript.Higher.CostExactZigzagMappingSpace.AlignedHammockGrid.linearHammockGridEquiv_simplex #print axioms Ript.Higher.CostExactZigzagMappingSpace.alignedHammockCore #print axioms Ript.Higher.CostExactZigzagMappingSpace.columnRefinementCore @@ -1079,6 +1093,10 @@ set_option autoImplicit false #print axioms Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_originalEdge #print axioms Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_hammockFactorization #print axioms Ript.Higher.CostExactZigzagMappingSpace.hammockPathNerveCore +#print axioms Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_whiskerLeftEdge +#print axioms Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_whiskerRightEdge +#print axioms Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_appendEdge +#print axioms Ript.Higher.CostExactZigzagMappingSpace.hammockPathWhiskeringCore #print axioms Ript.Higher.CostExactZigzagMappingSpace.core #print axioms CategoryTheory.Pseudofunctor.homotopyFunctor #print axioms CategoryTheory.Pseudofunctor.homotopyFunctor_map_homMk diff --git a/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean b/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean index 2cdaae7..b532584 100644 --- a/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean +++ b/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean @@ -23,10 +23,11 @@ equivalent to the discrete row quotient. A non-thin semantic refinement-path groupoid now retains paths up to equality of their quotient-cell semantics and embeds faithfully into the linear mapping category. Its exact generated image is internalized as a subgroupoid. A larger non-groupoidal hammock-path syntax -now alternates arbitrary aligned cells with invertible refinements, retaining -all source 2-cells in one-column form. Coverage of every presented quotient -2-cell, critical-pair coherence, and reduced-hammock invariance are still -absent, so this is not by itself the classical Dwyer--Kan hammock localization. +now alternates arbitrary aligned cells with invertible refinements, retains +all source 2-cells in one-column form, and is closed under normalized left/right +whiskering and horizontal append. Coverage of every presented quotient 2-cell, +critical-pair coherence, and reduced-hammock invariance are still absent, so +this is not by itself the classical Dwyer--Kan hammock localization. -/ set_option autoImplicit false @@ -1548,8 +1549,57 @@ structure HammockPathObject (X Y : B) where /-- Underlying linear row. -/ row : LinearWord W X Y +namespace HammockPath + +/-- Left whiskering of a quotient 2-cell between linear normal forms. The +canonical append isomorphisms enter the binary word presentation and return +to the right-associated linear normal form. -/ +noncomputable def normalizedWhiskerLeftHom {X Y Z : B} + (pre : LinearWord W X Y) {first second : LinearWord W Y Z} + (alpha : Presented.Hom W (LinearWord.toWord W first) + (LinearWord.toWord W second)) : + Presented.Hom W + (LinearWord.toWord W (LinearWord.append W pre first)) + (LinearWord.toWord W (LinearWord.append W pre second)) := + AlignedCell.quotientVcomp W + (LinearWord.toWordAppendIso W pre first).hom + (AlignedCell.quotientVcomp W + (Presented.whiskerLeftHom W (LinearWord.toWord W pre) alpha) + (LinearWord.toWordAppendIso W pre second).inv) + +/-- Right whiskering of a quotient 2-cell between linear normal forms, with +canonical transport through binary word append. -/ +noncomputable def normalizedWhiskerRightHom {X Y Z : B} + {first second : LinearWord W X Y} (post : LinearWord W Y Z) + (alpha : Presented.Hom W (LinearWord.toWord W first) + (LinearWord.toWord W second)) : + Presented.Hom W + (LinearWord.toWord W (LinearWord.append W first post)) + (LinearWord.toWord W (LinearWord.append W second post)) := + AlignedCell.quotientVcomp W + (LinearWord.toWordAppendIso W first post).hom + (AlignedCell.quotientVcomp W + (Presented.whiskerRightHom W (LinearWord.toWord W post) alpha) + (LinearWord.toWordAppendIso W second post).inv) + +/-- Transport an arbitrary raw presented cell to the linear normal forms of +its two binary word endpoints. -/ +noncomputable def normalizedCellHom {X Y : B} + {first second : Word W X Y} (cell : Cell W first second) : + Presented.Hom W + (LinearWord.toWord W (LinearWord.flatten W first)) + (LinearWord.toWord W (LinearWord.flatten W second)) := + AlignedCell.quotientVcomp W + (LinearWord.normalizationIso W first).inv + (AlignedCell.quotientVcomp W + (Presented.mk W cell) + (LinearWord.normalizationIso W second).hom) + +end HammockPath + /-- A generated hammock path may apply an invertible structural refinement, -an arbitrary aligned raw 2-cell, or a vertical composite of such moves. -/ +an arbitrary aligned raw 2-cell, normalized whiskering, or a vertical +composite of such moves. -/ inductive HammockPath : ∀ {X Y : B}, LinearWord W X Y → LinearWord W X Y → Type max u v w where /-- Empty vertical path. -/ @@ -1565,11 +1615,23 @@ inductive HammockPath : ∀ {X Y : B}, /-- An arbitrary componentwise aligned raw 2-cell. -/ | ofAligned {X Y : B} {first second : LinearWord W X Y} (cell : AlignedCell W first second) : HammockPath first second + /-- Whisker a generated path on the left by a fixed linear row. -/ + | whiskerLeft {X Y Z : B} (pre : LinearWord W X Y) + {first second : LinearWord W Y Z} + (path : HammockPath first second) : + HammockPath (LinearWord.append W pre first) + (LinearWord.append W pre second) + /-- Whisker a generated path on the right by a fixed linear row. -/ + | whiskerRight {X Y Z : B} {first second : LinearWord W X Y} + (path : HammockPath first second) (post : LinearWord W Y Z) : + HammockPath (LinearWord.append W first post) + (LinearWord.append W second post) namespace HammockPath -/-- Interpret a generated hammock path as one quotient 2-cell. -/ -def toHom {X Y : B} {first second : LinearWord W X Y} : +/-- Interpret a generated hammock path as one quotient 2-cell. Normalized +whiskering is semantic and therefore intentionally noncomputable. -/ +noncomputable def toHom {X Y : B} {first second : LinearWord W X Y} : HammockPath W first second → Presented.Hom W (LinearWord.toWord W first) (LinearWord.toWord W second) @@ -1578,6 +1640,8 @@ def toHom {X Y : B} {first second : LinearWord W X Y} : AlignedCell.quotientVcomp W (toHom alpha) (toHom beta) | .ofRefinement refinement => ColumnRefinement.toHom W refinement | .ofAligned cell => AlignedCell.toHom W cell + | .whiskerLeft pre path => normalizedWhiskerLeftHom W pre (toHom path) + | .whiskerRight path post => normalizedWhiskerRightHom W post (toHom path) @[simp] theorem toHom_identity {X Y : B} (row : LinearWord W X Y) : @@ -1608,6 +1672,48 @@ theorem toHom_ofAligned {X Y : B} toHom W (.ofAligned cell) = AlignedCell.toHom W cell := rfl +@[simp] +theorem toHom_whiskerLeft {X Y Z : B} (pre : LinearWord W X Y) + {first second : LinearWord W Y Z} + (path : HammockPath W first second) : + toHom W (.whiskerLeft pre path) = + normalizedWhiskerLeftHom W pre (toHom W path) := + rfl + +@[simp] +theorem toHom_whiskerRight {X Y Z : B} + {first second : LinearWord W X Y} + (path : HammockPath W first second) (post : LinearWord W Y Z) : + toHom W (.whiskerRight path post) = + normalizedWhiskerRightHom W post (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} + {firstSource firstTarget : LinearWord W X Y} + {secondSource secondTarget : LinearWord W Y Z} + (first : HammockPath W firstSource firstTarget) + (second : HammockPath W secondSource secondTarget) : + HammockPath W + (LinearWord.append W firstSource secondSource) + (LinearWord.append W firstTarget secondTarget) := + .vcomp (.whiskerRight first secondSource) + (.whiskerLeft firstTarget second) + +/-- Exact quotient interpretation of horizontal path append. -/ +@[simp] +theorem toHom_append {X Y Z : B} + {firstSource firstTarget : LinearWord W X Y} + {secondSource secondTarget : LinearWord W Y Z} + (first : HammockPath W firstSource firstTarget) + (second : HammockPath W secondSource secondTarget) : + toHom W (append W first second) = + AlignedCell.quotientVcomp W + (normalizedWhiskerRightHom W secondSource (toHom W first)) + (normalizedWhiskerLeftHom W firstTarget (toHom W second)) := + rfl + /-- Generated paths are semantically equal when their quotient 2-cell interpretations agree. -/ def Rel {X Y : B} {first second : LinearWord W X Y} @@ -1637,6 +1743,40 @@ theorem rel_vcomp {X Y : B} AlignedCell.quotientVcomp W (toHom W alpha') (toHom W beta') rw [hAlpha, hBeta] +/-- Semantic equality is stable under normalized left whiskering. -/ +theorem rel_whiskerLeft {X Y Z : B} (pre : LinearWord W X Y) + {first second : LinearWord W Y Z} + {alpha beta : HammockPath W first second} + (equality : Rel W alpha beta) : + Rel W (.whiskerLeft pre alpha) (.whiskerLeft pre beta) := by + unfold Rel at equality ⊢ + change normalizedWhiskerLeftHom W pre (toHom W alpha) = + normalizedWhiskerLeftHom W pre (toHom W beta) + rw [equality] + +/-- Semantic equality is stable under normalized right whiskering. -/ +theorem rel_whiskerRight {X Y Z : B} + {first second : LinearWord W X Y} (post : LinearWord W Y Z) + {alpha beta : HammockPath W first second} + (equality : Rel W alpha beta) : + Rel W (.whiskerRight alpha post) (.whiskerRight beta post) := by + unfold Rel at equality ⊢ + change normalizedWhiskerRightHom W post (toHom W alpha) = + normalizedWhiskerRightHom W post (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} + {secondSource secondTarget : LinearWord W Y Z} + {first first' : HammockPath W firstSource firstTarget} + {second second' : HammockPath W secondSource secondTarget} + (hFirst : Rel W first first') (hSecond : Rel W second second') : + Rel W (append W first second) (append W first' second') := by + apply rel_vcomp W + · exact rel_whiskerRight W secondSource hFirst + · exact rel_whiskerLeft W firstTarget hSecond + /-- Aligned-cell-augmented semantic paths form a category. -/ instance category (X Y : B) : Category (HammockPathObject W X Y) where Hom first second := Hom W first.row second.row @@ -1667,7 +1807,7 @@ instance category (X Y : B) : Category (HammockPathObject W X Y) where exact Category.assoc _ _ _ /-- Faithful semantic interpretation into the full linear mapping category. -/ -def semanticFunctor (X Y : B) : +noncomputable def semanticFunctor (X Y : B) : HammockPathObject W X Y ⥤ LinearWord W X Y where obj row := row.row map := Quotient.lift (toHom W) @@ -1771,6 +1911,12 @@ def InSemanticImage {X Y : B} {first second : LinearWord W X Y} (LinearWord.toWord W second)) : Prop := ∃ path : HammockPath W first second, toHom W path = morphism +/-- A raw cell is hammock-normalizable when its transport between the linear +normal forms of its endpoints lies in the generated semantic image. -/ +def Normalizable {X Y : B} {first second : Word W X Y} + (cell : Cell W first second) : Prop := + InSemanticImage W (normalizedCellHom W cell) + /-- Exact image characterization through morphisms of the semantic path category. -/ theorem inSemanticImage_iff_exists_map {X Y : B} @@ -1802,6 +1948,87 @@ theorem aligned_mem_semanticImage {X Y : B} InSemanticImage W (AlignedCell.toHom W cell) := ⟨.ofAligned cell, rfl⟩ +/-- The semantic image is closed under vertical composition. -/ +theorem vcomp_mem_semanticImage {X Y : B} + {first middle last : LinearWord W X Y} + {alpha : Presented.Hom W (LinearWord.toWord W first) + (LinearWord.toWord W middle)} + {beta : Presented.Hom W (LinearWord.toWord W middle) + (LinearWord.toWord W last)} + (hAlpha : InSemanticImage W alpha) + (hBeta : InSemanticImage W beta) : + InSemanticImage W (AlignedCell.quotientVcomp W alpha beta) := by + rcases hAlpha with ⟨alphaPath, hAlpha⟩ + rcases hBeta with ⟨betaPath, hBeta⟩ + exact ⟨.vcomp alphaPath betaPath, by rw [toHom_vcomp, hAlpha, hBeta]⟩ + +/-- The semantic image is closed under normalized left whiskering. -/ +theorem whiskerLeft_mem_semanticImage {X Y Z : B} + (pre : LinearWord W X Y) {first second : LinearWord W Y Z} + {morphism : Presented.Hom W (LinearWord.toWord W first) + (LinearWord.toWord W second)} + (member : InSemanticImage W morphism) : + InSemanticImage W (normalizedWhiskerLeftHom W pre morphism) := by + rcases member with ⟨path, equality⟩ + exact ⟨.whiskerLeft pre path, by rw [toHom_whiskerLeft, equality]⟩ + +/-- The semantic image is closed under normalized right whiskering. -/ +theorem whiskerRight_mem_semanticImage {X Y Z : B} + {first second : LinearWord W X Y} (post : LinearWord W Y Z) + {morphism : Presented.Hom W (LinearWord.toWord W first) + (LinearWord.toWord W second)} + (member : InSemanticImage W morphism) : + InSemanticImage W (normalizedWhiskerRightHom W post morphism) := by + rcases member with ⟨path, equality⟩ + exact ⟨.whiskerRight path post, by rw [toHom_whiskerRight, equality]⟩ + +/-- The semantic image is closed under horizontal append of represented +quotient 2-cells. -/ +theorem append_mem_semanticImage {X Y Z : B} + {firstSource firstTarget : LinearWord W X Y} + {secondSource secondTarget : LinearWord W Y Z} + {first : Presented.Hom W (LinearWord.toWord W firstSource) + (LinearWord.toWord W firstTarget)} + {second : Presented.Hom W (LinearWord.toWord W secondSource) + (LinearWord.toWord W secondTarget)} + (hFirst : InSemanticImage W first) + (hSecond : InSemanticImage W second) : + InSemanticImage W + (AlignedCell.quotientVcomp W + (normalizedWhiskerRightHom W secondSource first) + (normalizedWhiskerLeftHom W firstTarget second)) := by + rcases hFirst with ⟨firstPath, firstEquality⟩ + rcases hSecond with ⟨secondPath, secondEquality⟩ + refine ⟨append W firstPath secondPath, ?_⟩ + rw [toHom_append, firstEquality, secondEquality] + +/-- Normalizing a raw identity cell gives the identity of the linear normal +form. -/ +@[simp] +theorem normalizedCellHom_id {X Y : B} (word : Word W X Y) : + normalizedCellHom W (Cell.id word) = + 𝟙 (LinearWord.toWord W (LinearWord.flatten W word)) := by + change (LinearWord.normalizationIso W word).inv ≫ + (𝟙 word) ≫ (LinearWord.normalizationIso W word).hom = _ + simp + +/-- Normalization preserves vertical composition of raw cells exactly. -/ +@[simp] +theorem normalizedCellHom_vcomp {X Y : B} + {first middle last : Word W X Y} + (alpha : Cell W first middle) (beta : Cell W middle last) : + normalizedCellHom W (.vcomp alpha beta) = + AlignedCell.quotientVcomp W + (normalizedCellHom W alpha) (normalizedCellHom W beta) := by + change (LinearWord.normalizationIso W first).inv ≫ + (Presented.mk W alpha ≫ Presented.mk W beta) ≫ + (LinearWord.normalizationIso W last).hom = + ((LinearWord.normalizationIso W first).inv ≫ + Presented.mk W alpha ≫ (LinearWord.normalizationIso W middle).hom) ≫ + ((LinearWord.normalizationIso W middle).inv ≫ + Presented.mk W beta ≫ (LinearWord.normalizationIso W last).hom) + simp [Category.assoc] + /-- One-step linear row representing a source 1-cell. -/ def forwardRow {X Y : B} (f : X ⟶ Y) : LinearWord W X Y := .cons (.forward f) (.nil Y) @@ -1856,6 +2083,42 @@ theorem originalCell_mem_semanticImage {X Y : B} {f g : X ⟶ Y} (AlignedCell.toHom W (originalAlignedCell W alpha)) := aligned_mem_semanticImage W (originalAlignedCell W alpha) +/-- Normalizing an original source 2-cell recovers its canonical aligned +one-column interpretation. -/ +@[simp] +theorem normalizedCellHom_original {X Y : B} {f g : X ⟶ Y} + (alpha : f ⟶ g) : + normalizedCellHom W (Cell.original (W := W) alpha) = + AlignedCell.toHom W (originalAlignedCell W alpha) := by + change AlignedCell.quotientVcomp W + (Presented.wordRightUnitorIso W (Word.forward W f)).hom + (AlignedCell.quotientVcomp W + (Presented.mk W (Cell.original (W := W) alpha)) + (Presented.wordRightUnitorIso W (Word.forward W g)).inv) = _ + exact (originalAlignedCell_toHom W alpha).symm + +/-- Raw identity cells are hammock-normalizable. -/ +theorem identity_normalizable {X Y : B} (word : Word W X Y) : + Normalizable W (Cell.id word) := by + rw [Normalizable, normalizedCellHom_id] + exact ⟨.identity (LinearWord.flatten W word), rfl⟩ + +/-- Vertical composites of normalizable raw cells remain normalizable. -/ +theorem vcomp_normalizable {X Y : B} + {first middle last : Word W X Y} + {alpha : Cell W first middle} {beta : Cell W middle last} + (hAlpha : Normalizable W alpha) (hBeta : Normalizable W beta) : + Normalizable W (.vcomp alpha beta) := by + rw [Normalizable, normalizedCellHom_vcomp] + exact vcomp_mem_semanticImage W hAlpha hBeta + +/-- Original source 2-cells are hammock-normalizable. -/ +theorem original_normalizable {X Y : B} {f g : X ⟶ Y} + (alpha : f ⟶ g) : + Normalizable W (Cell.original (W := W) alpha) := by + rw [Normalizable, normalizedCellHom_original] + exact originalCell_mem_semanticImage W alpha + end HammockPath end CategoryTheory.Bicategory.MarkedZigzag diff --git a/Ript/Higher/CostExactZigzagMappingSpace.lean b/Ript/Higher/CostExactZigzagMappingSpace.lean index 143397c..d00d6d0 100644 --- a/Ript/Higher/CostExactZigzagMappingSpace.lean +++ b/Ript/Higher/CostExactZigzagMappingSpace.lean @@ -31,9 +31,11 @@ original semantic nerve map factors through it strictly, and generator edges retain their literal quotient-2-cell interpretations. A larger non-groupoidal generated hammock-path nerve now adds arbitrary aligned raw cells, contains the refinement-path nerve faithfully, and covers every source 2-cell in its -canonical one-column representation. Coverage of all presented quotient -2-cells, competing-move coherence, and reduced-hammock invariance are still -absent, so these results are not by themselves the final Dwyer--Kan theorem. +canonical one-column representation. Generated paths are now also closed under +normalized left/right whiskering and horizontal append, with exact three-model +nerve formulas. Coverage of all presented quotient 2-cells, competing-move +coherence, and reduced-hammock invariance are still absent, so these results +are not by themselves the final Dwyer--Kan theorem. -/ set_option autoImplicit false @@ -1001,7 +1003,7 @@ abbrev GeneratedHammockPath /-- Nerve map from generated hammock paths into the full linear mapping nerve. -/ -def hammockPathSemanticComparison +noncomputable def hammockPathSemanticComparison (M N : ProcessModel.{u, v, w} R) := CategoryTheory.nerveMap (Bicategory.MarkedZigzag.HammockPath.semanticFunctor @@ -1072,6 +1074,90 @@ theorem hammockPathSemanticComparison_alignedEdge (costExactArrows R) cell) := by exact CategoryTheory.nerveMap_app_mk₁ _ _ +/-- Exact semantic action on a generated path whiskered on the left by a +fixed linear row. -/ +theorem hammockPathSemanticComparison_whiskerLeftEdge + {M N P : ProcessModel.{u, v, w} R} + (pre : LinearHammock M N) + {first second : LinearHammock N P} + (path : Bicategory.MarkedZigzag.HammockPath + (costExactArrows R) first second) : + (hammockPathSemanticComparison M P).app (op ⦋1⦌) + (ComposableArrows.mk₁ + (Quotient.mk + (Bicategory.MarkedZigzag.HammockPath.setoid + (costExactArrows R) + (Bicategory.MarkedZigzag.LinearWord.append + (costExactArrows R) pre first) + (Bicategory.MarkedZigzag.LinearWord.append + (costExactArrows R) pre second)) + (Bicategory.MarkedZigzag.HammockPath.whiskerLeft pre path))) = + ComposableArrows.mk₁ + (Bicategory.MarkedZigzag.HammockPath.normalizedWhiskerLeftHom + (costExactArrows R) pre + (Bicategory.MarkedZigzag.HammockPath.toHom + (costExactArrows R) path)) := by + exact CategoryTheory.nerveMap_app_mk₁ _ _ + +/-- Exact semantic action on a generated path whiskered on the right by a +fixed linear row. -/ +theorem hammockPathSemanticComparison_whiskerRightEdge + {M N P : ProcessModel.{u, v, w} R} + {first second : LinearHammock M N} + (path : Bicategory.MarkedZigzag.HammockPath + (costExactArrows R) first second) + (post : LinearHammock N P) : + (hammockPathSemanticComparison M P).app (op ⦋1⦌) + (ComposableArrows.mk₁ + (Quotient.mk + (Bicategory.MarkedZigzag.HammockPath.setoid + (costExactArrows R) + (Bicategory.MarkedZigzag.LinearWord.append + (costExactArrows R) first post) + (Bicategory.MarkedZigzag.LinearWord.append + (costExactArrows R) second post)) + (Bicategory.MarkedZigzag.HammockPath.whiskerRight path post))) = + ComposableArrows.mk₁ + (Bicategory.MarkedZigzag.HammockPath.normalizedWhiskerRightHom + (costExactArrows R) post + (Bicategory.MarkedZigzag.HammockPath.toHom + (costExactArrows R) path)) := by + exact CategoryTheory.nerveMap_app_mk₁ _ _ + +/-- Exact semantic action on horizontal append of two generated hammock +paths. -/ +theorem hammockPathSemanticComparison_appendEdge + {M N P : ProcessModel.{u, v, w} R} + {firstSource firstTarget : LinearHammock M N} + {secondSource secondTarget : LinearHammock N P} + (first : Bicategory.MarkedZigzag.HammockPath + (costExactArrows R) firstSource firstTarget) + (second : Bicategory.MarkedZigzag.HammockPath + (costExactArrows R) secondSource secondTarget) : + (hammockPathSemanticComparison M P).app (op ⦋1⦌) + (ComposableArrows.mk₁ + (Quotient.mk + (Bicategory.MarkedZigzag.HammockPath.setoid + (costExactArrows R) + (Bicategory.MarkedZigzag.LinearWord.append + (costExactArrows R) firstSource secondSource) + (Bicategory.MarkedZigzag.LinearWord.append + (costExactArrows R) firstTarget secondTarget)) + (Bicategory.MarkedZigzag.HammockPath.append + (costExactArrows R) first second))) = + ComposableArrows.mk₁ + (Bicategory.MarkedZigzag.AlignedCell.quotientVcomp + (costExactArrows R) + (Bicategory.MarkedZigzag.HammockPath.normalizedWhiskerRightHom + (costExactArrows R) secondSource + (Bicategory.MarkedZigzag.HammockPath.toHom + (costExactArrows R) first)) + (Bicategory.MarkedZigzag.HammockPath.normalizedWhiskerLeftHom + (costExactArrows R) firstTarget + (Bicategory.MarkedZigzag.HammockPath.toHom + (costExactArrows R) second))) := by + exact CategoryTheory.nerveMap_app_mk₁ _ _ + /-- Exact semantic action on a source 2-cell in its canonical one-column linear representation. -/ theorem hammockPathSemanticComparison_originalEdge @@ -1174,6 +1260,90 @@ theorem hammockPathNerveCore (M N : ProcessModel.{u, v, w} R) : maps_aligned := hammockPathSemanticComparison_alignedEdge maps_original := hammockPathSemanticComparison_originalEdge +/-- Machine-facing exact three-model whiskering and append interface for the +generated hammock-path nerves. -/ +structure HammockPathWhiskeringCore + (M N P : ProcessModel.{u, v, w} R) : Prop where + /-- Exact action on every left-whiskered generated path. -/ + maps_whiskerLeft : ∀ (pre : LinearHammock M N) + {first second : LinearHammock N P} + (path : Bicategory.MarkedZigzag.HammockPath + (costExactArrows R) first second), + (hammockPathSemanticComparison M P).app (op ⦋1⦌) + (ComposableArrows.mk₁ + (Quotient.mk + (Bicategory.MarkedZigzag.HammockPath.setoid + (costExactArrows R) + (Bicategory.MarkedZigzag.LinearWord.append + (costExactArrows R) pre first) + (Bicategory.MarkedZigzag.LinearWord.append + (costExactArrows R) pre second)) + (Bicategory.MarkedZigzag.HammockPath.whiskerLeft pre path))) = + ComposableArrows.mk₁ + (Bicategory.MarkedZigzag.HammockPath.normalizedWhiskerLeftHom + (costExactArrows R) pre + (Bicategory.MarkedZigzag.HammockPath.toHom + (costExactArrows R) path)) + /-- Exact action on every right-whiskered generated path. -/ + maps_whiskerRight : ∀ {first second : LinearHammock M N} + (path : Bicategory.MarkedZigzag.HammockPath + (costExactArrows R) first second) + (post : LinearHammock N P), + (hammockPathSemanticComparison M P).app (op ⦋1⦌) + (ComposableArrows.mk₁ + (Quotient.mk + (Bicategory.MarkedZigzag.HammockPath.setoid + (costExactArrows R) + (Bicategory.MarkedZigzag.LinearWord.append + (costExactArrows R) first post) + (Bicategory.MarkedZigzag.LinearWord.append + (costExactArrows R) second post)) + (Bicategory.MarkedZigzag.HammockPath.whiskerRight path post))) = + ComposableArrows.mk₁ + (Bicategory.MarkedZigzag.HammockPath.normalizedWhiskerRightHom + (costExactArrows R) post + (Bicategory.MarkedZigzag.HammockPath.toHom + (costExactArrows R) path)) + /-- Exact action on horizontal append. -/ + maps_append : ∀ + {firstSource firstTarget : LinearHammock M N} + {secondSource secondTarget : LinearHammock N P} + (first : Bicategory.MarkedZigzag.HammockPath + (costExactArrows R) firstSource firstTarget) + (second : Bicategory.MarkedZigzag.HammockPath + (costExactArrows R) secondSource secondTarget), + (hammockPathSemanticComparison M P).app (op ⦋1⦌) + (ComposableArrows.mk₁ + (Quotient.mk + (Bicategory.MarkedZigzag.HammockPath.setoid + (costExactArrows R) + (Bicategory.MarkedZigzag.LinearWord.append + (costExactArrows R) firstSource secondSource) + (Bicategory.MarkedZigzag.LinearWord.append + (costExactArrows R) firstTarget secondTarget)) + (Bicategory.MarkedZigzag.HammockPath.append + (costExactArrows R) first second))) = + ComposableArrows.mk₁ + (Bicategory.MarkedZigzag.AlignedCell.quotientVcomp + (costExactArrows R) + (Bicategory.MarkedZigzag.HammockPath.normalizedWhiskerRightHom + (costExactArrows R) secondSource + (Bicategory.MarkedZigzag.HammockPath.toHom + (costExactArrows R) first)) + (Bicategory.MarkedZigzag.HammockPath.normalizedWhiskerLeftHom + (costExactArrows R) firstTarget + (Bicategory.MarkedZigzag.HammockPath.toHom + (costExactArrows R) second))) + +/-- Every cost-exact model triple satisfies the exact generated-path +whiskering and append interface. -/ +theorem hammockPathWhiskeringCore + (M N P : ProcessModel.{u, v, w} R) : + HammockPathWhiskeringCore M N P where + maps_whiskerLeft := hammockPathSemanticComparison_whiskerLeftEdge + maps_whiskerRight := hammockPathSemanticComparison_whiskerRightEdge + maps_append := hammockPathSemanticComparison_appendEdge + /-- The source-defined relative mapping category is categorically equivalent to the actual local hom-category of the presented localization target. The underlying categories are definitionally the same presentation, but this diff --git a/docs/en/RESEARCH_STATUS.md b/docs/en/RESEARCH_STATUS.md index 150ad48..989073c 100644 --- a/docs/en/RESEARCH_STATUS.md +++ b/docs/en/RESEARCH_STATUS.md @@ -390,10 +390,14 @@ non-groupoidal generated path category now alternates refinements with arbitrary aligned raw 2-cells. Its semantics and the refinement embedding are faithful, the old nerve map factors through it strictly, and every source 2-cell has a canonical one-column edge equal to the original quotient cell -conjugated by right-unitors. Normalization of every presented quotient 2-cell -into these paths, competing-move coherence, reduced-hammock invariance, -standard weak-equivalence packaging, and the global Dwyer--Kan/Rezk theorem -remain. +conjugated by right-unitors. Normalized left/right whiskering and horizontal +append now preserve semantic equality and image membership and have exact +cost-exact three-model nerve formulas. Raw identity/original cells are +normalizable, and vertical composition preserves normalizability. The next +missing induction law is naturality of normalization isomorphisms with raw +whiskering; remaining structural generators, competing-move coherence, +reduced-hammock invariance, standard weak-equivalence packaging, and the global +Dwyer--Kan/Rezk theorem remain. The actual construction has now begun with a computable presented syntax. `MarkedZigzag.Word` is endpoint-indexed, permits every source 1-cell forward, diff --git a/docs/en/reference/AXIOMS.md b/docs/en/reference/AXIOMS.md index 842219f..cf8fc2d 100644 --- a/docs/en/reference/AXIOMS.md +++ b/docs/en/reference/AXIOMS.md @@ -970,15 +970,29 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.lean`. | `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_essSurj` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.semanticFunctor_factorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_vcomp` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.semanticFunctor_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinementFunctor_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_vcomp` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.semanticFunctor_faithful` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinementFunctor_faithful` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinementSemanticFunctor_factorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.inSemanticImage_iff_exists_map` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinement_mem_semanticImage` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.aligned_mem_semanticImage` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.inSemanticImage_iff_exists_map` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinement_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.aligned_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.originalAlignedCell_toHom` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.originalCell_mem_semanticImage` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.originalCell_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedWhiskerLeftHom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedWhiskerRightHom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_whiskerLeft` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_whiskerRight` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_append` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerLeft_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerRight_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.append_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_id` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_vcomp` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_original` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.identity_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.vcomp_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.original_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `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` | @@ -998,6 +1012,10 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.lean`. | `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_originalEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_hammockFactorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.hammockPathNerveCore` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_whiskerLeftEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_whiskerRightEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_appendEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathWhiskeringCore` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.core` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `CategoryTheory.Pseudofunctor.homotopyFunctor` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/PseudofunctorHomotopy.lean` | | `CategoryTheory.Pseudofunctor.homotopyFunctor_map_homMk` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/PseudofunctorHomotopy.lean` | diff --git a/docs/en/reference/BLUEPRINT.md b/docs/en/reference/BLUEPRINT.md index 9a2d327..35cbf2b 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; its semantic functor into the full linear mapping category is faithful and object-essentially-surjective, the refinement-path groupoid embeds faithfully and factors strictly through it, every aligned cell lies in its exact semantic image, and every source 2-cell has a canonical one-column representative equal to the original quotient cell conjugated by right-unitors; the induced cost-exact nerve maps have exact refinement/aligned/source-edge formulas | PROVED | +| 12 (aligned-cell-augmented hammock paths) | A non-groupoidal generated path syntax alternates executable refinements with arbitrary aligned raw 2-cells and vertical composition, then quotients only by equality of quotient-cell semantics; normalized left/right whiskering enters and leaves binary append through canonical linear-normal-form isomorphisms, horizontal append composes those operations, and semantic equality/image membership are closed under all three; the semantic functor is faithful and object-essentially-surjective, refinement paths embed faithfully and factor strictly, every source 2-cell has a canonical one-column representative, raw identity/original cells are normalizable and normalizability is closed under vertical composition; cost-exact three-model nerve maps have exact whiskering/append edge formulas | PROVED | | 12 (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) | Normalize every presented quotient 2-cell into alternating aligned-cell/refinement hammock paths (or characterize the remaining missing generators), 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) | Prove normalization-isomorphism naturality for raw left/right whiskering, normalize the remaining structural raw-cell generators and hence every presented quotient 2-cell into alternating aligned-cell/refinement hammock paths, prove critical-pair coherence and reduced-hammock homotopical invariance (or compare the generated path category to another accepted derived mapping-space construction), connect that comparison to a standard weak-equivalence interface, and finish the standard Dwyer--Kan/Rezk weak-equivalence and completeness theorem | OPEN_RESEARCH | ## Finite deterministic copy-discard theorem records diff --git a/docs/en/reference/CONJECTURES.md b/docs/en/reference/CONJECTURES.md index bc661de..b01f2a4 100644 --- a/docs/en/reference/CONJECTURES.md +++ b/docs/en/reference/CONJECTURES.md @@ -468,11 +468,14 @@ through it strictly. A larger non-groupoidal path category now alternates refinements with arbitrary aligned raw 2-cells. Its semantics is faithful, the refinement subsystem embeds faithfully and factors strictly, and every source 2-cell has a canonical one-column representative whose quotient semantics is -the original 2-cell conjugated by right-unitors. The remaining classical gap -is normalizing every presented quotient 2-cell into these alternating paths -(or identifying the missing generators), together with coherence for -competing forward/marked moves, reduced-hammock moves, and their homotopical -invariance. +the original 2-cell conjugated by right-unitors. The path calculus is now +closed under normalized left/right whiskering and horizontal append, with +exact cost-exact three-model nerve formulas. Raw identities and original cells +are normalizable, and normalizability is closed under vertical composition. +The next missing induction law is naturality of the chosen normalization +isomorphisms with raw whiskering; after it, the remaining structural generators +must be normalized before fullness can be claimed. Competing forward/marked +moves, reduced-hammock moves, and their homotopical invariance remain open. 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. @@ -577,9 +580,12 @@ and simplicially equivalent to the exact subgroupoid of refinement-generated quotient 2-cells, which includes faithfully in the full linear mapping category and strictly factors the semantic nerve map. The aligned-cell- augmented path category now adds arbitrary pointwise raw cells, contains every -source 2-cell in one-column form, and strictly extends refinement paths. -Normalization of all presented quotient 2-cells into this generated category, -critical-pair coherence, and reduced-hammock invariance remain open. +source 2-cell in one-column form, strictly extends refinement paths, and is +closed under normalized left/right whiskering and horizontal append. Identity, +vertical-composite, and original-cell normalization cases are proved. +Normalization-isomorphism naturality for raw whiskering and the remaining +structural generators, critical-pair coherence, and reduced-hammock invariance +remain open. The first complete construction against that predicate is now kernel checked. Identity precomposition is an adjoint equivalence of pseudofunctors and an diff --git a/docs/en/reference/MODEL_MATRIX.md b/docs/en/reference/MODEL_MATRIX.md index 6ace4ce..dde1ba3 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 with strict refinement-nerve factorization are proved; normalization of every presented quotient 2-cell into the generated hammock paths, 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, closed under normalized left/right whiskering and horizontal append, with exact three-model nerve formulas and proved identity/vertical/original raw-cell normalization cases are proved; normalization-isomorphism naturality for raw whiskering, the remaining structural-cell normalization cases, 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 @@ -670,7 +670,9 @@ subgroupoid equivalent to the path groupoid, with a faithful inclusion into the full linear mapping category and a strictly factored semantic nerve map. The aligned-cell-augmented non-groupoidal path category now adds arbitrary pointwise raw cells, contains every source 2-cell in canonical one-column form, -and strictly extends the refinement path nerve. What remains is normalization -of every presented quotient 2-cell into these generated paths, critical-pair -coherence, and reduced-hammock invariance. These +strictly extends the refinement path nerve, and is closed under normalized +left/right whiskering and horizontal append. Raw identities and original cells +are normalizable and vertical composition preserves normalizability. What +remains is normalization-isomorphism naturality for raw whiskering, the other +structural generators, 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 cb0dba9..9d4a0f6 100644 --- a/docs/eo/RESEARCH_STATUS.md +++ b/docs/eo/RESEARCH_STATUS.md @@ -361,9 +361,13 @@ negrupoida generita vojkategorio nun alternas rafinadojn kun arbitraj vicigitaj krudaj 2-ĉeloj. Ĝiaj semantiko kaj rafinada enmeto estas fidelaj, la malnova nervomapo strikte faktoriĝas tra ĝi, kaj ĉiu fonta 2-ĉelo havas kanonan unukolumnan eĝon egalan al la origina kvocienta ĉelo konjugita per dekstraj -unuigiloj. Restas normaligi ĉiun prezentitan kvocientan 2-ĉelon en tiajn vojojn -(aŭ identigi mankantajn generatorojn), kohereco de kritikaj paroj, -reduktita-hammock invariant eco kaj norma malfort-ekvivalenta pako. +unuigiloj. Normaligitaj maldekstra/dekstra whiskering kaj horizontala append +nun konservas semantikan egalecon kaj bildanecon, kun ekzaktaj tri-modelaj +nervaj formuloj. Krudaj identecaj kaj originalaj ĉeloj estas normaligeblaj, +kaj vertikala kunmeto konservas normaligeblecon. Restas pruvi naturecon de la +normaligaj izomorfioj rilate al kruda whiskering, normaligi la aliajn +strukturajn generatorojn, koherecon de kritikaj paroj, reduktita-hammock +invariant econ kaj norman malfort-ekvivalentan pakon. La fakta konstruo nun komenciĝas per komputebla prezenta sintakso. `MarkedZigzag.Word` estas fintipita per siaj ekstremoj, permesas ĉiun fontan diff --git a/docs/eo/reference/AXIOMS.md b/docs/eo/reference/AXIOMS.md index de7beb5..4eb346c 100644 --- a/docs/eo/reference/AXIOMS.md +++ b/docs/eo/reference/AXIOMS.md @@ -972,15 +972,29 @@ per `scripts/sync-doc-reference-tables.sh` kaj ne estu mane redaktataj. | `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_essSurj` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.semanticFunctor_factorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_vcomp` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.semanticFunctor_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinementFunctor_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_vcomp` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.semanticFunctor_faithful` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinementFunctor_faithful` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinementSemanticFunctor_factorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.inSemanticImage_iff_exists_map` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinement_mem_semanticImage` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.aligned_mem_semanticImage` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.inSemanticImage_iff_exists_map` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinement_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.aligned_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.originalAlignedCell_toHom` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.originalCell_mem_semanticImage` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.originalCell_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedWhiskerLeftHom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedWhiskerRightHom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_whiskerLeft` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_whiskerRight` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_append` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerLeft_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerRight_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.append_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_id` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_vcomp` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_original` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.identity_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.vcomp_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.original_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `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` | @@ -1000,6 +1014,10 @@ per `scripts/sync-doc-reference-tables.sh` kaj ne estu mane redaktataj. | `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_originalEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_hammockFactorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.hammockPathNerveCore` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_whiskerLeftEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_whiskerRightEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_appendEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathWhiskeringCore` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.core` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `CategoryTheory.Pseudofunctor.homotopyFunctor` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/PseudofunctorHomotopy.lean` | | `CategoryTheory.Pseudofunctor.homotopyFunctor_map_homMk` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/PseudofunctorHomotopy.lean` | diff --git a/docs/ja/RESEARCH_STATUS.md b/docs/ja/RESEARCH_STATUS.md index e826a00..fb77141 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 に等しい正準一列辺を持ちます。未解決なのは、全 presented quotient 2-cell をこの path に正規化すること（または不足生成元の同定）、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 identity/original cell は正規化可能で、垂直合成は正規化可能性を保存します。未解決なのは、正規化同型の raw whiskering に対する自然性、残る構造生成元の正規化、critical-pair coherence、reduced-hammock 不変性、標準弱同値 packaging です。 異なる資源代数のモデルは順序付き加法準同型で比較できます。直列、並列、構造、予算則が再添字 付けされ、異種強モデル射は資源写像とともに合成します。これらは、資源代数とモデルを対象、 diff --git a/docs/ja/reference/AXIOMS.md b/docs/ja/reference/AXIOMS.md index e3fb86c..bb0dd32 100644 --- a/docs/ja/reference/AXIOMS.md +++ b/docs/ja/reference/AXIOMS.md @@ -970,15 +970,29 @@ | `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_essSurj` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.semanticFunctor_factorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_vcomp` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.semanticFunctor_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinementFunctor_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_vcomp` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.semanticFunctor_faithful` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinementFunctor_faithful` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinementSemanticFunctor_factorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.inSemanticImage_iff_exists_map` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinement_mem_semanticImage` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.aligned_mem_semanticImage` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.inSemanticImage_iff_exists_map` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinement_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.aligned_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.originalAlignedCell_toHom` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.originalCell_mem_semanticImage` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.originalCell_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedWhiskerLeftHom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedWhiskerRightHom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_whiskerLeft` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_whiskerRight` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_append` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerLeft_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerRight_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.append_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_id` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_vcomp` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_original` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.identity_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.vcomp_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.original_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `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` | @@ -998,6 +1012,10 @@ | `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_originalEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_hammockFactorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.hammockPathNerveCore` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_whiskerLeftEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_whiskerRightEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_appendEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathWhiskeringCore` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.core` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `CategoryTheory.Pseudofunctor.homotopyFunctor` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/PseudofunctorHomotopy.lean` | | `CategoryTheory.Pseudofunctor.homotopyFunctor_map_homMk` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/PseudofunctorHomotopy.lean` | diff --git a/docs/zh-CN/RESEARCH_STATUS.md b/docs/zh-CN/RESEARCH_STATUS.md index 9fe123e..40577ea 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-胞腔。仍缺把每个 presented quotient 2-cell 规范化为这类路径（或识别剩余生成元）、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 恒等与 original 胞腔已可正规化，纵向复合保持可正规化性。仍缺证明正规化同构对 raw whiskering 的自然性、正规化其余结构生成元、critical-pair 协调、约化 hammock 不变性及标准弱等价封装。 模型比较不再要求全局使用同一资源代数。有序加法同态重索引串行、并行、结构和预算律；跨资源 代数的强辫模型态射随同态复合，并在每个固定资源映射上形成单子自然变换的局部范畴。四维计算 diff --git a/docs/zh-CN/reference/AXIOMS.md b/docs/zh-CN/reference/AXIOMS.md index edd4d59..c530616 100644 --- a/docs/zh-CN/reference/AXIOMS.md +++ b/docs/zh-CN/reference/AXIOMS.md @@ -970,15 +970,29 @@ | `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_essSurj` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.semanticFunctor_factorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_vcomp` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.semanticFunctor_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinementFunctor_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_vcomp` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.semanticFunctor_faithful` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinementFunctor_faithful` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinementSemanticFunctor_factorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.inSemanticImage_iff_exists_map` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinement_mem_semanticImage` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.aligned_mem_semanticImage` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.inSemanticImage_iff_exists_map` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.refinement_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.aligned_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.originalAlignedCell_toHom` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | -| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.originalCell_mem_semanticImage` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.originalCell_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedWhiskerLeftHom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedWhiskerRightHom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_whiskerLeft` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_whiskerRight` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.rel_append` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerLeft_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerRight_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.append_mem_semanticImage` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_id` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_vcomp` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_original` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.identity_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.vcomp_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.original_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `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` | @@ -998,6 +1012,10 @@ | `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_originalEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_hammockFactorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.hammockPathNerveCore` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_whiskerLeftEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_whiskerRightEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathSemanticComparison_appendEdge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.hammockPathWhiskeringCore` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.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` |