From 9a04ed57e3644def600b4227ea97a31182b329d2 Mon Sep 17 00:00:00 2001 From: Amamiya Miu Date: Sat, 22 Aug 2026 13:28:54 +0800 Subject: [PATCH] feat(higher): characterize refinement semantic image --- AXIOMS.md | 12 ++ BLUEPRINT.md | 3 +- CONJECTURES.md | 22 ++- MODEL_MATRIX.md | 9 +- Ript/Audit/AxiomChecks.lean | 12 ++ .../MarkedZigzagAlignedHammock.lean | 180 +++++++++++++++++ Ript/Higher/CostExactZigzagMappingSpace.lean | 182 +++++++++++++++++- docs/en/RESEARCH_STATUS.md | 13 +- docs/en/reference/AXIOMS.md | 12 ++ docs/en/reference/BLUEPRINT.md | 3 +- docs/en/reference/CONJECTURES.md | 22 ++- docs/en/reference/MODEL_MATRIX.md | 9 +- docs/eo/RESEARCH_STATUS.md | 8 +- docs/eo/reference/AXIOMS.md | 12 ++ docs/ja/RESEARCH_STATUS.md | 2 +- docs/ja/reference/AXIOMS.md | 12 ++ docs/zh-CN/RESEARCH_STATUS.md | 2 +- docs/zh-CN/reference/AXIOMS.md | 12 ++ 18 files changed, 494 insertions(+), 33 deletions(-) diff --git a/AXIOMS.md b/AXIOMS.md index e62eee4..a8d0809 100644 --- a/AXIOMS.md +++ b/AXIOMS.md @@ -963,6 +963,13 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.lean`. | `CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.semanticFunctor_map_isIso` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.toThinFunctor_full` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.toThinFunctor_essSurj` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.isGroupoid` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.inclusion_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_full` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.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` | | `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` | @@ -973,6 +980,11 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.lean`. | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_vertex` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_edge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathNerveCore` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageNerveEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageHomotopyEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_factorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageComparison_edge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementImageNerveCore` | `[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 f9c6fe1..39647c6 100644 --- a/BLUEPRINT.md +++ b/BLUEPRINT.md @@ -389,8 +389,9 @@ Every node in this graph is an existing compiled module. | 12 (common-refinement row quotient) | Every executable refinement has an executable reverse with negated signed width and one unified semantic isomorphism whose forward map is the quotient-cell interpretation; explicit two-leg common-refinement spans are reflexive, symmetric, and transitive; their setoid quotient identifies every refinement endpoint, quotient equality is exactly common-refinability, and every quotient equality yields a semantic isomorphism without assuming object equality | PROVED | | 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 (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) | Characterize or enlarge the faithful non-thin refinement-path image inside the full linear mapping category, prove critical-pair coherence and reduced-hammock homotopical invariance (or compare it 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 that the exact refinement-generated semantic image covers the required derived/hammock mapping core (or characterize and add the missing linear quotient 2-cells), prove critical-pair coherence and reduced-hammock homotopical invariance (or compare it 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 5fefbc7..3aa9829 100644 --- a/CONJECTURES.md +++ b/CONJECTURES.md @@ -459,10 +459,15 @@ isomorphism, not Lean object equality. A non-thin semantic refinement-path groupoid is now compiled as well: paths are quotiented only by equality of their quotient-cell interpretations, executable reversal gives inverses, and the semantic functor into the linear mapping category is faithful and -essentially surjective on row objects with exact nerve edge action. The -remaining classical gap is fullness or an exact image characterization, -coherence for competing forward/marked moves, reduced-hammock moves, and their -homotopical invariance. +essentially surjective on row objects with exact nerve edge action. Its exact +semantic image has now been internalized as the subgroupoid of actual quotient +2-cells carrying an executable-refinement witness: paths are equivalent to +this image, the image inclusion is faithful, the nerve equivalence has an +explicit simplicial homotopy inverse, and semantic interpretation factors +through it strictly. The remaining classical gap is proving that this exact +image covers the required derived/hammock core (or adding the missing linear +quotient 2-cells), together with coherence for competing forward/marked moves, +reduced-hammock moves, and their homotopical invariance. 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. @@ -562,9 +567,12 @@ and semantic inverse laws. Their object-level common-refinement quotient and semantic-isomorphism soundness are now proved. A quotient mapping nerve, in the precise 0-truncated sense, is also proved via the thin refinement groupoid/discrete-quotient nerve equivalence. A non-thin refinement-path nerve, -with faithful exact semantic action, is now proved too. Fullness/image -characterization, critical-pair coherence, and reduced-hammock invariance -remain open. +with faithful exact semantic action, is now proved too. It is categorically +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. Coverage of the required +derived/hammock mapping core by this exact image, 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 4aa5dd5..a4fcb1d 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, and a non-thin semantic refinement-path groupoid nerve faithfully and object-essentially-surjectively mapped into the linear mapping nerve with exact edge action are proved; fullness/image characterization, 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, and its categorical/nerve equivalence to the exact refinement-generated quotient-cell image subgroupoid with faithful linear inclusion and strict semantic factorization are proved; coverage of the required derived/hammock core by that exact image, 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 @@ -665,6 +665,9 @@ to the discrete row quotient, and the nerve map has an explicit simplicial homotopy inverse. The non-thin semantic path groupoid and its faithful, object-essentially-surjective nerve map now compile, with exact refinement-edge interpretation and full zero-truncation onto the thin -groupoid. What remains is fullness or an exact image characterization, -critical-pair coherence, and reduced-hammock invariance. These +groupoid. Its exact refinement-generated quotient-cell image is now a +subgroupoid equivalent to the path groupoid, with a faithful inclusion into +the full linear mapping category and a strictly factored semantic nerve map. +What remains is coverage of the required derived/hammock core by that exact +image, 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 8bac3e0..093d4f3 100644 --- a/Ript/Audit/AxiomChecks.lean +++ b/Ript/Audit/AxiomChecks.lean @@ -1044,6 +1044,13 @@ set_option autoImplicit false #print axioms CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.semanticFunctor_map_isIso #print axioms CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.toThinFunctor_full #print axioms CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.toThinFunctor_essSurj +#print axioms CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.isGroupoid +#print axioms CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.inclusion_faithful +#print axioms CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_full +#print axioms CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_faithful +#print axioms CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_essSurj +#print axioms CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathEquivalence +#print axioms CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.semanticFunctor_factorization #print axioms Ript.Higher.CostExactZigzagMappingSpace.AlignedHammockGrid.linearHammockGridEquiv_simplex #print axioms Ript.Higher.CostExactZigzagMappingSpace.alignedHammockCore #print axioms Ript.Higher.CostExactZigzagMappingSpace.columnRefinementCore @@ -1054,6 +1061,11 @@ set_option autoImplicit false #print axioms Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_vertex #print axioms Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_edge #print axioms Ript.Higher.CostExactZigzagMappingSpace.refinementPathNerveCore +#print axioms Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageNerveEquivalence +#print axioms Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageHomotopyEquivalence +#print axioms Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_factorization +#print axioms Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageComparison_edge +#print axioms Ript.Higher.CostExactZigzagMappingSpace.refinementImageNerveCore #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 280688b..2b937d2 100644 --- a/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean +++ b/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean @@ -1358,4 +1358,184 @@ instance toThinFunctor_essSurj (X Y : B) : end RefinementPath +/-! ## Exact refinement-generated semantic image -/ + +/-- Wrapper for rows in the refinement-generated semantic image subgroupoid +of the linear mapping category. -/ +structure RefinementImageObject (X Y : B) where + /-- Underlying linear row. -/ + row : LinearWord W X Y + +namespace RefinementImage + +/-- A quotient 2-cell together with the proposition that it is generated by +an executable column refinement. -/ +abbrev Hom {X Y : B} (first second : LinearWord W X Y) := + { hom : Presented.Hom W (LinearWord.toWord W first) + (LinearWord.toWord W second) // + ∃ refinement : ColumnRefinement W first second, + ColumnRefinement.toHom W refinement = hom } + +/-- Forget the generating-refinement witness while retaining the represented +quotient 2-cell. -/ +def underlying {X Y : B} {first second : LinearWord W X Y} : + Hom W first second → + Presented.Hom W (LinearWord.toWord W first) + (LinearWord.toWord W second) := + Subtype.val + +/-- Refinement-generated semantic morphisms form a category. -/ +instance category (X Y : B) : Category (RefinementImageObject W X Y) where + Hom first second := Hom W first.row second.row + id first := ⟨𝟙 (LinearWord.toWord W first.row), + ⟨.identity first.row, ColumnRefinement.toHom_identity W first.row⟩⟩ + comp alpha beta := + ⟨AlignedCell.quotientVcomp W alpha.1 beta.1, by + rcases alpha.2 with ⟨alphaRefinement, hAlpha⟩ + rcases beta.2 with ⟨betaRefinement, hBeta⟩ + refine ⟨.vcomp alphaRefinement betaRefinement, ?_⟩ + rw [ColumnRefinement.toHom_vcomp, hAlpha, hBeta]⟩ + id_comp morphism := by + apply Subtype.ext + exact @Category.id_comp (Word W X Y) (Presented.wordCategory W X Y) + _ _ morphism.1 + comp_id morphism := by + apply Subtype.ext + exact @Category.comp_id (Word W X Y) (Presented.wordCategory W X Y) + _ _ morphism.1 + assoc alpha beta gamma := by + apply Subtype.ext + change AlignedCell.quotientVcomp W + (AlignedCell.quotientVcomp W alpha.1 beta.1) gamma.1 = + AlignedCell.quotientVcomp W alpha.1 + (AlignedCell.quotientVcomp W beta.1 gamma.1) + exact @Category.assoc (Word W X Y) (Presented.wordCategory W X Y) + _ _ _ _ alpha.1 beta.1 gamma.1 + +/-- The refinement-generated semantic image is a groupoid. -/ +instance isGroupoid (X Y : B) : IsGroupoid (RefinementImageObject W X Y) where + all_isIso {first second} morphism := by + change Hom W first.row second.row at morphism + rcases morphism.2 with ⟨refinement, hRefinement⟩ + let inverse : Hom W second.row first.row := + ⟨ColumnRefinement.toHom W (ColumnRefinement.reverse W refinement), + ⟨ColumnRefinement.reverse W refinement, rfl⟩⟩ + refine ⟨⟨inverse, ?_, ?_⟩⟩ + · apply Subtype.ext + change AlignedCell.quotientVcomp W morphism.1 inverse.1 = + 𝟙 (LinearWord.toWord W _) + rw [← hRefinement] + change AlignedCell.quotientVcomp W + (ColumnRefinement.toHom W refinement) + (ColumnRefinement.toHom W + (ColumnRefinement.reverse W refinement)) = + 𝟙 (LinearWord.toWord W first.row) + rw [ColumnRefinement.toHom_eq_toIso_hom, + ColumnRefinement.toHom_eq_toIso_hom, + ColumnRefinement.toIso_reverse] + exact (ColumnRefinement.toIso W refinement).hom_inv_id + · apply Subtype.ext + change AlignedCell.quotientVcomp W inverse.1 morphism.1 = + 𝟙 (LinearWord.toWord W _) + rw [← hRefinement] + change AlignedCell.quotientVcomp W + (ColumnRefinement.toHom W + (ColumnRefinement.reverse W refinement)) + (ColumnRefinement.toHom W refinement) = + 𝟙 (LinearWord.toWord W second.row) + rw [ColumnRefinement.toHom_eq_toIso_hom, + ColumnRefinement.toIso_reverse, + ColumnRefinement.toHom_eq_toIso_hom] + exact (ColumnRefinement.toIso W refinement).inv_hom_id + +/-- Faithful inclusion of the exact refinement-generated image into the full +linear mapping category. -/ +def inclusion (X Y : B) : + RefinementImageObject W X Y ⥤ LinearWord W X Y where + obj row := row.row + map := underlying W + map_id _ := rfl + map_comp _ _ := rfl + +instance inclusion_faithful (X Y : B) : (inclusion W X Y).Faithful where + map_injective {first second} alpha beta equality := by + change Hom W first.row second.row at alpha beta + exact Subtype.ext equality + +/-- Convert a semantic refinement path to the corresponding morphism in its +exact generated image. -/ +def ofPath {X Y : B} + {first second : RefinementPathObject W X Y} : + (first ⟶ second) → Hom W first.row second.row := + Quotient.lift + (fun refinement => + ⟨ColumnRefinement.toHom W refinement, ⟨refinement, rfl⟩⟩) + (fun _ _ equality => Subtype.ext equality) + +/-- The semantic refinement-path groupoid maps onto its exact generated image. -/ +def pathFunctor (X Y : B) : + RefinementPathObject W X Y ⥤ RefinementImageObject W X Y where + obj row := ⟨row.row⟩ + map := ofPath W + map_id _ := by + apply Subtype.ext + exact ColumnRefinement.toHom_identity W _ + map_comp alpha beta := by + apply Subtype.ext + rcases alpha with ⟨alpha⟩ + rcases beta with ⟨beta⟩ + exact ColumnRefinement.toHom_vcomp W alpha beta + +instance pathFunctor_faithful (X Y : B) : (pathFunctor W X Y).Faithful where + map_injective {first second} alpha beta equality := by + rcases alpha with ⟨alpha⟩ + rcases beta with ⟨beta⟩ + apply Quotient.sound + change RefinementPath.Rel W alpha beta + change (⟨ColumnRefinement.toHom W alpha, ⟨alpha, rfl⟩⟩ : + Hom W first.row second.row) = + (⟨ColumnRefinement.toHom W beta, ⟨beta, rfl⟩⟩ : + Hom W first.row second.row) at equality + exact congrArg Subtype.val equality + +instance pathFunctor_full (X Y : B) : (pathFunctor W X Y).Full where + map_surjective {first second} morphism := by + change Hom W first.row second.row at morphism + rcases morphism.2 with ⟨refinement, hRefinement⟩ + refine ⟨Quotient.mk (RefinementPath.setoid W first.row second.row) + refinement, ?_⟩ + apply Subtype.ext + exact hRefinement + +instance pathFunctor_essSurj (X Y : B) : (pathFunctor W X Y).EssSurj where + mem_essImage row := by + refine ⟨⟨row.row⟩, ?_⟩ + exact ⟨Iso.refl row⟩ + +instance pathFunctor_isEquivalence (X Y : B) : + (pathFunctor W X Y).IsEquivalence where + faithful := inferInstance + full := inferInstance + essSurj := inferInstance + +/-- Equivalence between semantic refinement paths and their exact generated +image subgroupoid. -/ +noncomputable def pathEquivalence (X Y : B) : + RefinementPathObject W X Y ≌ RefinementImageObject W X Y := + (pathFunctor W X Y).asEquivalence + +/-- The original semantic functor factors strictly through its exact generated +image. -/ +theorem semanticFunctor_factorization (X Y : B) : + RefinementPath.semanticFunctor W X Y = + pathFunctor W X Y ⋙ inclusion W X Y := by + apply Functor.hext + · intro row + rfl + · intro first second path + rcases path with ⟨refinement⟩ + rfl + +end RefinementImage + end CategoryTheory.Bicategory.MarkedZigzag diff --git a/Ript/Higher/CostExactZigzagMappingSpace.lean b/Ript/Higher/CostExactZigzagMappingSpace.lean index 5eda939..fc8f792 100644 --- a/Ript/Higher/CostExactZigzagMappingSpace.lean +++ b/Ript/Higher/CostExactZigzagMappingSpace.lean @@ -25,10 +25,13 @@ signed width and semantic round trips. Common-refinement spans now generate a row quotient whose equality is sound for semantic isomorphism. A quotient thin groupoid/nerve is now equivalent to the discrete quotient with an explicit simplicial homotopy inverse. A non-thin semantic refinement-path groupoid nerve -now maps faithfully and object-essentially-surjectively into the linear mapping -nerve with exact edge action. Fullness/image characterization, competing-move -coherence, and reduced-hammock invariance are still absent, so these results -are not by themselves the final Dwyer--Kan theorem. +is now equivalent to its exact refinement-generated semantic image subgroupoid. +The image includes faithfully into the full linear mapping category, the +original semantic nerve map factors through it strictly, and generator edges +retain their literal quotient-2-cell interpretations. Coverage of all linear +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 @@ -818,6 +821,173 @@ theorem refinementPathNerveCore (M N : ProcessModel.{u, v, w} R) : maps_vertex := refinementPathSemanticComparison_vertex maps_edge := refinementPathSemanticComparison_edge +/-! ## Exact refinement-generated semantic image nerve -/ + +/-- The exact semantic image category whose morphisms are precisely quotient +2-cells generated by executable column refinements. -/ +abbrev RefinementImage + (M N : ProcessModel.{u, v, w} R) := + Bicategory.MarkedZigzag.RefinementImageObject + (costExactArrows R) M N + +/-- Nerve of the exact refinement-generated semantic image subgroupoid. -/ +abbrev RefinementImageNerve + (M N : ProcessModel.{u, v, w} R) := + CategoryTheory.nerve (RefinementImage M N) + +/-- Categorical equivalence from semantic refinement paths onto their exact +generated semantic image. -/ +noncomputable def refinementPathImageEquivalence + (M N : ProcessModel.{u, v, w} R) : + Bicategory.MarkedZigzag.RefinementPathObject + (costExactArrows R) M N ≌ + RefinementImage M N := + Bicategory.MarkedZigzag.RefinementImage.pathEquivalence + (costExactArrows R) M N + +/-- Nerve comparison from semantic refinement paths to their exact generated +semantic image. -/ +noncomputable def refinementPathImageComparison + (M N : ProcessModel.{u, v, w} R) := + CategoryTheory.nerveMap + (refinementPathImageEquivalence M N).functor + +/-- Faithful nerve inclusion of the generated semantic image into the full +linear hammock mapping nerve. -/ +def refinementImageInclusionComparison + (M N : ProcessModel.{u, v, w} R) := + CategoryTheory.nerveMap + (Bicategory.MarkedZigzag.RefinementImage.inclusion + (costExactArrows R) M N) + +/-- Categorical-nerve equivalence evidence for semantic refinement paths and +their exact generated image. -/ +noncomputable def refinementPathImageNerveEquivalence + (M N : ProcessModel.{u, v, w} R) : + SSet.NerveEquivalenceWitness (refinementPathImageComparison M N) := + SSet.NerveEquivalenceWitness.ofEquivalence + (refinementPathImageEquivalence M N) + +/-- Explicit simplicial inverse and both homotopies for the path-to-image +comparison. -/ +noncomputable def refinementPathImageHomotopyEquivalence + (M N : ProcessModel.{u, v, w} R) : + SSet.HomotopyEquivalenceWitness (refinementPathImageComparison M N) := + SSet.HomotopyEquivalenceWitness.ofCategoryEquivalence + (refinementPathImageEquivalence M N) + +/-- Exact object action of the refinement-path-to-image nerve comparison. -/ +theorem refinementPathImageComparison_vertex + {M N : ProcessModel.{u, v, w} R} + (row : LinearHammock M N) : + (refinementPathImageComparison M N).app (op ⦋0⦌) + (ComposableArrows.mk₀ + (⟨row⟩ : Bicategory.MarkedZigzag.RefinementPathObject + (costExactArrows R) M N)) = + ComposableArrows.mk₀ + (⟨row⟩ : RefinementImage M N) := by + exact CategoryTheory.nerveMap_app_mk₀ _ _ + +/-- Exact edge action: an executable refinement path maps to the same +quotient 2-cell equipped with its generating-refinement witness. -/ +theorem refinementPathImageComparison_edge + {M N : ProcessModel.{u, v, w} R} + {first second : LinearHammock M N} + (refinement : HammockColumnRefinement first second) : + (refinementPathImageComparison M N).app (op ⦋1⦌) + (ComposableArrows.mk₁ + (Quotient.mk + (Bicategory.MarkedZigzag.RefinementPath.setoid + (costExactArrows R) first second) refinement)) = + ComposableArrows.mk₁ + (⟨Bicategory.MarkedZigzag.ColumnRefinement.toHom + (costExactArrows R) refinement, + ⟨refinement, rfl⟩⟩ : + Bicategory.MarkedZigzag.RefinementImage.Hom + (costExactArrows R) first second) := by + exact CategoryTheory.nerveMap_app_mk₁ _ _ + +/-- The image inclusion forgets only the generating-refinement witness on an +edge and preserves its quotient 2-cell literally. -/ +theorem refinementImageInclusionComparison_edge + {M N : ProcessModel.{u, v, w} R} + {first second : RefinementImage M N} + (morphism : first ⟶ second) : + (refinementImageInclusionComparison M N).app (op ⦋1⦌) + (ComposableArrows.mk₁ morphism) = + ComposableArrows.mk₁ + (Bicategory.MarkedZigzag.RefinementImage.underlying + (costExactArrows R) morphism) := by + exact CategoryTheory.nerveMap_app_mk₁ _ _ + +/-- The original semantic refinement-path nerve map factors strictly through +the exact generated image nerve and its faithful inclusion. -/ +theorem refinementPathSemanticComparison_factorization + (M N : ProcessModel.{u, v, w} R) : + refinementPathSemanticComparison M N = + refinementPathImageComparison M N ≫ + refinementImageInclusionComparison M N := by + change CategoryTheory.nerveMap + (Bicategory.MarkedZigzag.RefinementPath.semanticFunctor + (costExactArrows R) M N) = _ + rw [Bicategory.MarkedZigzag.RefinementImage.semanticFunctor_factorization] + rfl + +/-- Machine-facing core for the exact refinement-generated semantic image. +It records the subgroupoid boundary, categorical and simplicial equivalence, +faithful inclusion, strict semantic factorization, and exact generator action. -/ +structure RefinementImageNerveCore + (M N : ProcessModel.{u, v, w} R) : Prop where + /-- The exact generated image is a groupoid. -/ + image_groupoid : IsGroupoid (RefinementImage M N) + /-- Its inclusion into the full linear mapping category is faithful. -/ + inclusion_faithful : + (Bicategory.MarkedZigzag.RefinementImage.inclusion + (costExactArrows R) M N).Faithful + /-- Semantic paths are categorically equivalent to their exact image. -/ + path_equivalence : Nonempty + (Bicategory.MarkedZigzag.RefinementPathObject + (costExactArrows R) M N ≌ RefinementImage M N) + /-- Their nerves are categorically equivalent. -/ + nerve_equivalence : Nonempty + (SSet.NerveEquivalenceWitness (refinementPathImageComparison M N)) + /-- The nerve comparison has an explicit inverse and both homotopies. -/ + homotopy_equivalence : Nonempty + (SSet.HomotopyEquivalenceWitness (refinementPathImageComparison M N)) + /-- The semantic nerve map factors strictly through the image inclusion. -/ + semantic_factorization : + refinementPathSemanticComparison M N = + refinementPathImageComparison M N ≫ + refinementImageInclusionComparison M N + /-- Exact action on each executable generator edge. -/ + maps_edge : ∀ {first second : LinearHammock M N} + (refinement : HammockColumnRefinement first second), + (refinementPathImageComparison M N).app (op ⦋1⦌) + (ComposableArrows.mk₁ + (Quotient.mk + (Bicategory.MarkedZigzag.RefinementPath.setoid + (costExactArrows R) first second) refinement)) = + ComposableArrows.mk₁ + (⟨Bicategory.MarkedZigzag.ColumnRefinement.toHom + (costExactArrows R) refinement, + ⟨refinement, rfl⟩⟩ : + Bicategory.MarkedZigzag.RefinementImage.Hom + (costExactArrows R) first second) + +/-- Every cost-exact model pair satisfies the exact generated-image nerve +comparison. -/ +theorem refinementImageNerveCore + (M N : ProcessModel.{u, v, w} R) : + RefinementImageNerveCore M N where + image_groupoid := inferInstance + inclusion_faithful := inferInstance + path_equivalence := ⟨refinementPathImageEquivalence M N⟩ + nerve_equivalence := ⟨refinementPathImageNerveEquivalence M N⟩ + homotopy_equivalence := ⟨refinementPathImageHomotopyEquivalence M N⟩ + semantic_factorization := + refinementPathSemanticComparison_factorization M N + maps_edge := refinementPathImageComparison_edge + /-- 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 @@ -1053,6 +1223,9 @@ structure MappingSpaceCore (M N : ProcessModel.{u, v, w} R) where /-- Non-thin semantic refinement-path groupoid nerve with faithful exact edge interpretation. -/ refinementPathNerve : RefinementPathNerveCore M N + /-- Exact refinement-generated semantic image subgroupoid, its equivalence + with semantic paths, and its faithful inclusion into the full linear nerve. -/ + refinementImageNerve : RefinementImageNerveCore M N /-- Arbitrary-height row-grid representation of every linear hammock nerve simplex. -/ linearGridRepresentation : ∀ n : ℕ, @@ -1129,6 +1302,7 @@ noncomputable def core (M N : ProcessModel.{u, v, w} R) : commonRefinement := commonRefinementCore M N thinRefinementNerve := thinRefinementNerveCore M N refinementPathNerve := refinementPathNerveCore M N + refinementImageNerve := refinementImageNerveCore M N linearGridRepresentation := linearHammockGridEquiv M N linearNerveEquivalence := linearComparisonNerveEquivalence M N linearHomotopyEquivalence := linearComparisonHomotopyEquivalence M N diff --git a/docs/en/RESEARCH_STATUS.md b/docs/en/RESEARCH_STATUS.md index 1208a6e..69bfbbc 100644 --- a/docs/en/RESEARCH_STATUS.md +++ b/docs/en/RESEARCH_STATUS.md @@ -380,10 +380,15 @@ refinement-path groupoid now retains paths modulo equality of quotient-cell interpretations. Its semantic nerve map into the linear mapping nerve is faithful and essentially surjective on row objects, maps every path to an isomorphism, and has exact vertex/edge action; its zero-truncation to the thin -groupoid is full and essentially surjective. Fullness or an exact semantic -image characterization, competing-move coherence, reduced-hammock invariance, -standard weak-equivalence packaging, and the global Dwyer--Kan/Rezk theorem -remain. +groupoid is full and essentially surjective. The exact semantic image is now +internalized as the subgroupoid of actual quotient 2-cells carrying an +executable-refinement witness. Semantic paths are categorically equivalent to +this image; the nerve comparison has an explicit simplicial homotopy inverse, +the image inclusion into the full linear mapping category is faithful, and the +original semantic nerve map factors through it strictly. Coverage of the +required derived/hammock mapping core by this exact image, 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 5adbbd6..64b7907 100644 --- a/docs/en/reference/AXIOMS.md +++ b/docs/en/reference/AXIOMS.md @@ -963,6 +963,13 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.lean`. | `CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.semanticFunctor_map_isIso` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.toThinFunctor_full` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.toThinFunctor_essSurj` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.isGroupoid` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.inclusion_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_full` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.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` | | `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` | @@ -973,6 +980,11 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.lean`. | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_vertex` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_edge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathNerveCore` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageNerveEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageHomotopyEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_factorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageComparison_edge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementImageNerveCore` | `[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 3d13f5a..ee25209 100644 --- a/docs/en/reference/BLUEPRINT.md +++ b/docs/en/reference/BLUEPRINT.md @@ -389,8 +389,9 @@ Every node in this graph is an existing compiled module. | 12 (common-refinement row quotient) | Every executable refinement has an executable reverse with negated signed width and one unified semantic isomorphism whose forward map is the quotient-cell interpretation; explicit two-leg common-refinement spans are reflexive, symmetric, and transitive; their setoid quotient identifies every refinement endpoint, quotient equality is exactly common-refinability, and every quotient equality yields a semantic isomorphism without assuming object equality | PROVED | | 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 (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) | Characterize or enlarge the faithful non-thin refinement-path image inside the full linear mapping category, prove critical-pair coherence and reduced-hammock homotopical invariance (or compare it 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 that the exact refinement-generated semantic image covers the required derived/hammock mapping core (or characterize and add the missing linear quotient 2-cells), prove critical-pair coherence and reduced-hammock homotopical invariance (or compare it 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 ea8b407..274e4d9 100644 --- a/docs/en/reference/CONJECTURES.md +++ b/docs/en/reference/CONJECTURES.md @@ -459,10 +459,15 @@ isomorphism, not Lean object equality. A non-thin semantic refinement-path groupoid is now compiled as well: paths are quotiented only by equality of their quotient-cell interpretations, executable reversal gives inverses, and the semantic functor into the linear mapping category is faithful and -essentially surjective on row objects with exact nerve edge action. The -remaining classical gap is fullness or an exact image characterization, -coherence for competing forward/marked moves, reduced-hammock moves, and their -homotopical invariance. +essentially surjective on row objects with exact nerve edge action. Its exact +semantic image has now been internalized as the subgroupoid of actual quotient +2-cells carrying an executable-refinement witness: paths are equivalent to +this image, the image inclusion is faithful, the nerve equivalence has an +explicit simplicial homotopy inverse, and semantic interpretation factors +through it strictly. The remaining classical gap is proving that this exact +image covers the required derived/hammock core (or adding the missing linear +quotient 2-cells), together with coherence for competing forward/marked moves, +reduced-hammock moves, and their homotopical invariance. 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. @@ -562,9 +567,12 @@ and semantic inverse laws. Their object-level common-refinement quotient and semantic-isomorphism soundness are now proved. A quotient mapping nerve, in the precise 0-truncated sense, is also proved via the thin refinement groupoid/discrete-quotient nerve equivalence. A non-thin refinement-path nerve, -with faithful exact semantic action, is now proved too. Fullness/image -characterization, critical-pair coherence, and reduced-hammock invariance -remain open. +with faithful exact semantic action, is now proved too. It is categorically +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. Coverage of the required +derived/hammock mapping core by this exact image, 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 037ac91..ea083fd 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, and a non-thin semantic refinement-path groupoid nerve faithfully and object-essentially-surjectively mapped into the linear mapping nerve with exact edge action are proved; fullness/image characterization, 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, and its categorical/nerve equivalence to the exact refinement-generated quotient-cell image subgroupoid with faithful linear inclusion and strict semantic factorization are proved; coverage of the required derived/hammock core by that exact image, 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 @@ -665,6 +665,9 @@ to the discrete row quotient, and the nerve map has an explicit simplicial homotopy inverse. The non-thin semantic path groupoid and its faithful, object-essentially-surjective nerve map now compile, with exact refinement-edge interpretation and full zero-truncation onto the thin -groupoid. What remains is fullness or an exact image characterization, -critical-pair coherence, and reduced-hammock invariance. These +groupoid. Its exact refinement-generated quotient-cell image is now a +subgroupoid equivalent to the path groupoid, with a faithful inclusion into +the full linear mapping category and a strictly factored semantic nerve map. +What remains is coverage of the required derived/hammock core by that exact +image, 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 5099dc1..ffb2f32 100644 --- a/docs/eo/RESEARCH_STATUS.md +++ b/docs/eo/RESEARCH_STATUS.md @@ -352,7 +352,13 @@ nun konservas vojojn modulo egaleco de iliaj kvocient-ĉelaj interpretoj. Ĝia nerva mapo al la lineara map-nervo estas fidela kaj esence surĵeta je vicaj objektoj, sendas ĉiun vojon al izomorfio, kaj havas ekzaktajn verticajn/eĝajn formulojn; la nul-tranĉo al la maldika grupoido estas plena kaj esence -surĵeta. Restas pleneco aŭ ekzakta bilda karakterizo, kohereco de kritikaj +surĵeta. Faktaj kvocientaj 2-ĉeloj kun ekzista atestilo de plenumebla rafinado +nun formas la ekzaktan semantikan bildgrupoidon. La voja grupoido estas +kategorie ekvivalenta al ĝi; la nerva komparo havas eksplicitan simplician +homotopian inverson, la bildinkludo en la plenan linearan mapkategorion estas +fidela, kaj la origina semantika nervomapo strikte faktoriĝas tra ĝi. Restas +pruvi ke tiu ekzakta bildo kovras la bezonatan derivitan/hammock-an mapkernon +(aŭ aldoni la mankantajn linearajn kvocientajn 2-ĉelojn), kohereco de kritikaj paroj, reduktita-hammock invariant eco kaj norma malfort-ekvivalenta pako. La fakta konstruo nun komenciĝas per komputebla prezenta sintakso. diff --git a/docs/eo/reference/AXIOMS.md b/docs/eo/reference/AXIOMS.md index febe261..3e8ebf6 100644 --- a/docs/eo/reference/AXIOMS.md +++ b/docs/eo/reference/AXIOMS.md @@ -965,6 +965,13 @@ per `scripts/sync-doc-reference-tables.sh` kaj ne estu mane redaktataj. | `CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.semanticFunctor_map_isIso` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.toThinFunctor_full` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.toThinFunctor_essSurj` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.isGroupoid` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.inclusion_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_full` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.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` | | `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` | @@ -975,6 +982,11 @@ per `scripts/sync-doc-reference-tables.sh` kaj ne estu mane redaktataj. | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_vertex` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_edge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathNerveCore` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageNerveEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageHomotopyEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_factorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageComparison_edge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementImageNerveCore` | `[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 f124b8e..e366031 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 です。fullness/厳密 image 記述、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 は厳密にこの像を経由します。未解決なのは、この厳密像が必要な derived/hammock mapping core を被覆すること（または不足する線形商 2-cell の追加）、critical-pair coherence、reduced-hammock 不変性、標準弱同値 packaging です。 異なる資源代数のモデルは順序付き加法準同型で比較できます。直列、並列、構造、予算則が再添字 付けされ、異種強モデル射は資源写像とともに合成します。これらは、資源代数とモデルを対象、 diff --git a/docs/ja/reference/AXIOMS.md b/docs/ja/reference/AXIOMS.md index 31224e8..29b5e29 100644 --- a/docs/ja/reference/AXIOMS.md +++ b/docs/ja/reference/AXIOMS.md @@ -963,6 +963,13 @@ | `CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.semanticFunctor_map_isIso` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.toThinFunctor_full` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.toThinFunctor_essSurj` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.isGroupoid` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.inclusion_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_full` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.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` | | `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` | @@ -973,6 +980,11 @@ | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_vertex` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_edge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathNerveCore` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageNerveEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageHomotopyEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_factorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageComparison_edge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementImageNerveCore` | `[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 e0b41d8..6a994bb 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 且本质满。仍缺 fullness/精确 image 刻画、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 严格经过它。仍缺证明该精确像覆盖所需 derived/hammock mapping core（或补充缺失的线性商 2-胞腔）、critical-pair 协调、约化 hammock 不变性及标准弱等价封装。 模型比较不再要求全局使用同一资源代数。有序加法同态重索引串行、并行、结构和预算律；跨资源 代数的强辫模型态射随同态复合，并在每个固定资源映射上形成单子自然变换的局部范畴。四维计算 diff --git a/docs/zh-CN/reference/AXIOMS.md b/docs/zh-CN/reference/AXIOMS.md index efa76ac..24ae2e5 100644 --- a/docs/zh-CN/reference/AXIOMS.md +++ b/docs/zh-CN/reference/AXIOMS.md @@ -963,6 +963,13 @@ | `CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.semanticFunctor_map_isIso` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.toThinFunctor_full` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | | `CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.toThinFunctor_essSurj` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.isGroupoid` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.inclusion_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_full` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.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` | | `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` | @@ -973,6 +980,11 @@ | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_vertex` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_edge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathNerveCore` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageNerveEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageHomotopyEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_factorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageComparison_edge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` | +| `Ript.Higher.CostExactZigzagMappingSpace.refinementImageNerveCore` | `[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` |