diff --git a/AXIOMS.md b/AXIOMS.md index e1c85f8..78710ad 100644 --- a/AXIOMS.md +++ b/AXIOMS.md @@ -993,6 +993,27 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.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` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.flatten_forward` | `none` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.flatten_backward` | `none` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_atom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_nil` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_append` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.AlignedCell.quotientVcomp_assoc` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.appendIso_inv_whiskerLeft_appendIso_hom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.appendIso_inv_whiskerRight_appendIso_hom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedHom_whiskerLeft` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedHom_whiskerRight` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_whiskerLeft` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_whiskerRight` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerLeft_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerRight_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceId` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceIdInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceId_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceIdInv_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_transport` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.transport_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizable_of_structuralGenerators` | `[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` | @@ -1016,6 +1037,7 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.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.hammockRawCellNormalizationCore` | `[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 1e5e4c9..1511a58 100644 --- a/BLUEPRINT.md +++ b/BLUEPRINT.md @@ -390,9 +390,9 @@ Every node in this graph is an existing compiled module. | 12 (zero-truncated common-refinement mapping nerve) | Wrapped rows form a thin common-refinement groupoid; its canonical functor to the discrete row quotient is faithful, full, essentially surjective, and hence a categorical equivalence; the induced nerve map has categorical-nerve equivalence evidence, an explicit simplicial inverse and both homotopies, and exact row-vertex action | PROVED | | 12 (non-thin semantic refinement-path nerve) | Refinement syntax modulo equality of quotient-cell interpretations forms a non-thin groupoid; executable reversal supplies inverses; its semantic functor into the linear mapping category is faithful and essentially surjective on row objects, maps every path to an isomorphism, and induces a nerve map with exact row-vertex and arbitrary-refinement-edge action; the zero-truncation functor to the thin groupoid is full and essentially surjective | PROVED | | 12 (exact refinement-generated semantic image) | Actual quotient 2-cells equipped with existence of an executable refinement generator form a non-thin image subgroupoid of the linear mapping category; inclusion is faithful, the semantic refinement-path functor is full, faithful, essentially surjective and hence an equivalence onto this exact image, and the induced nerve equivalence has an explicit simplicial homotopy inverse, exact generator-edge action, and strict factorization of the original semantic nerve map | PROVED | -| 12 (aligned-cell-augmented hammock paths) | A non-groupoidal generated path syntax alternates executable refinements with arbitrary aligned raw 2-cells and vertical composition, then quotients only by equality of quotient-cell semantics; normalized left/right whiskering enters and leaves binary append through canonical linear-normal-form isomorphisms, horizontal append composes those operations, and semantic equality/image membership are closed under all three; 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 (aligned-cell-augmented hammock paths) | A non-groupoidal generated path syntax alternates executable refinements with arbitrary aligned raw 2-cells and vertical composition, then quotients only by equality of quotient-cell semantics; normalized left/right whiskering enters and leaves binary append through canonical linear-normal-form isomorphisms, horizontal append composes those operations, and semantic equality/image membership are closed under all three; explicit append-isomorphism exchange/cancellation proves normalization naturality for raw left/right whiskering; raw identity, original, source-identity/inverse, whiskering, vertical-composite, and equality-transport cells are normalizable; `StructuralGeneratorNormalizable` lists exactly the remaining source-composite, marked pair, associator, and unitor obligations and yields all-cell normalization by structural induction; the cost-exact core records these completed branches and conditional induction | PROVED | | 12 (cost-exact two-layer global comparison) | Pseudofunctor-induced functor on homotopy categories; localization-aware relative Rezk map and auxiliary ordinary outer map into the actual marked-zigzag target; explicit source/target outer completeness homotopy equivalences; marked outer arrows factoring through the target actual-equivalence space; packaging with the exact non-groupoidal local nerve comparison; exact vertex, identity, horizontal-composition, associator, and left/right-unitor gluing; arbitrary invertible local 2-cell decoding; explicit pentagon and triangle compatibility | PROVED | -| 12 (global cost-exact complete-Segal/Rezk equivalence) | 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 | +| 12 (global cost-exact complete-Segal/Rezk equivalence) | Discharge the twelve explicit `StructuralGeneratorNormalizable` fields for source composition/inverse, marked unit/counit and inverses, associator/inverse, and left/right unitors and inverses; deduce every presented quotient 2-cell has an alternating aligned/refinement path and hence semantic fullness, then prove critical-pair coherence and reduced-hammock homotopical invariance (or compare the generated path category to another accepted derived mapping-space construction), connect that comparison to a standard weak-equivalence interface, and finish the standard Dwyer--Kan/Rezk weak-equivalence and completeness theorem | OPEN_RESEARCH | ## Finite deterministic copy-discard theorem records diff --git a/CONJECTURES.md b/CONJECTURES.md index 2ddcce3..be5e525 100644 --- a/CONJECTURES.md +++ b/CONJECTURES.md @@ -472,10 +472,15 @@ 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. +Normalization naturality for both raw whiskerings is now proved by explicit +append-isomorphism exchange and cancellation; source identity and inverse plus +equality transport are normalizable too. The exact remaining induction basis +is the twelve-field `StructuralGeneratorNormalizable` record: source composite +and inverse, marked unit/counit and inverses, associator and inverse, and both +unitors and inverses. That record already implies normalization of every raw +cell by structural induction, but none of its unproved fields is assumed in an +unconditional theorem. 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. @@ -582,10 +587,11 @@ 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, 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. +vertical-composite, original-cell, both whiskering, source-identity/inverse, +and equality-transport normalization cases are proved. The remaining twelve +structural generator obligations are explicit and sufficient for the complete +induction, but remain unproved; 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 f263d32..36f9d2c 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, 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 | +| Rezk classifying diagram | Outer simplicial category of composable interface strings, followed levelwise by the ordinary nerve | Every vertical level and horizontal row is a groupoid nerve and Kan; every horizontal row is strict Segal; the whole outer diagram is naturally `n ↦ Map(Δ[n], N(M.Object))`; `Map(∂Δ[n], N(M.Object))` is the genuine matching limit; every matching map is a fibration; the actual completeness map has an explicit simplicial homotopy inverse | Semantic proof layer; exact project-local `GroupoidalCompleteSegal` and `HomotopyEquivalenceWitness` evidence proved; the full cost-exact localization, common-universe local comparison, localization-aware all-dimensional relative outer Rezk map, source/target completeness witnesses, arbitrary-2-cell one-skeleton glue, vertical local 2-simplex/composite-diagonal glue, degree-one horizontal compositor squares, degree-two vertical pasting/interchange, the explicit three-tetrahedron degree-two compositor prism, all-degree local prism coherence, arbitrary outer-string vertex/restriction comparison, relative-outer gluing of every all-degree prism source vertex, strict decoded-pair naturality for every restriction, exact side-sensitive outer/local glue for every actual target prism-face vertex, a categorical-nerve equivalence from the presented relative-zigzag mapping nerve to every actual target local nerve, strict all-degree local-map factorization, outer essential surjectivity, target-independent algebraic/simplicial presentation universality, an audited `PresentedDwyerKanCore`, an independent right-associated linear hammock mapping category equivalent to the binary presentation and actual target local nerve, an audited `LinearHammockDwyerKanCore`, an exact arbitrary-height row-grid representation of every linear-hammock simplex, exact quotient/nerve interpretation of the fixed-shape aligned multi-column fragment, an executable elementary forward/marked-pair refinement calculus, an object-level common-refinement quotient sound for semantic isomorphism, a zero-truncated thin refinement-groupoid nerve equivalent to the discrete quotient nerve, a non-thin semantic refinement-path groupoid nerve with exact edge action, its categorical/nerve equivalence to the exact refinement-generated quotient-cell image subgroupoid, and a faithful aligned-cell-augmented non-groupoidal path category containing every source 2-cell in canonical one-column form are proved; normalized whiskering/append have exact three-model formulas, normalization commutes with raw whiskering, identity/original/source-identity/transport and closure cases are proved, and a twelve-field criterion implies all-cell normalization; those twelve structural generator fields, semantic fullness, competing-move coherence, reduced-hammock invariance, standard weak-equivalence packaging, and the final Dwyer--Kan comparison remain open | The concrete Boolean model proves that `bit tensor unit` and `unit tensor bit` are unequal syntax trees in Lean while tensor symmetry makes them internally @@ -671,8 +671,10 @@ 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, 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 +left/right whiskering and horizontal append. Normalization now commutes with +both raw whiskerings; raw identity/original/source-identity/inverse and +equality-transport cases plus vertical/whiskering closure are proved. Twelve +explicit source-composite, marked-pair, associator, and unitor obligations are +sufficient for the complete structural induction but remain open, together +with critical-pair coherence and reduced-hammock invariance. These layers do not add `Equiv α β → α = β` and are not a complete presheaf model. diff --git a/Ript/Audit/AxiomChecks.lean b/Ript/Audit/AxiomChecks.lean index bc697ac..e1aaf7e 100644 --- a/Ript/Audit/AxiomChecks.lean +++ b/Ript/Audit/AxiomChecks.lean @@ -1074,6 +1074,27 @@ set_option autoImplicit false #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 CategoryTheory.Bicategory.MarkedZigzag.LinearWord.flatten_forward +#print axioms CategoryTheory.Bicategory.MarkedZigzag.LinearWord.flatten_backward +#print axioms CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_atom +#print axioms CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_nil +#print axioms CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_append +#print axioms CategoryTheory.Bicategory.MarkedZigzag.AlignedCell.quotientVcomp_assoc +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.appendIso_inv_whiskerLeft_appendIso_hom +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.appendIso_inv_whiskerRight_appendIso_hom +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedHom_whiskerLeft +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedHom_whiskerRight +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_whiskerLeft +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_whiskerRight +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerLeft_normalizable +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerRight_normalizable +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceId +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceIdInv +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceId_normalizable +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceIdInv_normalizable +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_transport +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.transport_normalizable +#print axioms CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizable_of_structuralGenerators #print axioms Ript.Higher.CostExactZigzagMappingSpace.AlignedHammockGrid.linearHammockGridEquiv_simplex #print axioms Ript.Higher.CostExactZigzagMappingSpace.alignedHammockCore #print axioms Ript.Higher.CostExactZigzagMappingSpace.columnRefinementCore @@ -1097,6 +1118,7 @@ set_option autoImplicit false #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.hammockRawCellNormalizationCore #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 b532584..7c3248f 100644 --- a/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean +++ b/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean @@ -25,9 +25,12 @@ 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, 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. +whiskering and horizontal append. Normalization is natural for raw whiskering; +identity, original, source-identity/inverse, composition-closure, whiskering, +and equality-transport induction branches are complete, while twelve explicit +structural-generator obligations remain. 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 @@ -175,6 +178,31 @@ def quotientVcomp {X Y : B} {first middle last : Word W X Y} (Presented.wordCategory W X Y).toCategoryStruct first middle last alpha beta +/-- Explicit associativity of quotient vertical composition. -/ +theorem quotientVcomp_assoc {X Y : B} + {first second third fourth : Word W X Y} + (alpha : Presented.Hom W first second) + (beta : Presented.Hom W second third) + (gamma : Presented.Hom W third fourth) : + quotientVcomp W (quotientVcomp W alpha beta) gamma = + quotientVcomp W alpha (quotientVcomp W beta gamma) := + @Category.assoc (Word W X Y) (Presented.wordCategory W X Y) + _ _ _ _ alpha beta gamma + +/-- Explicit left identity law for quotient vertical composition. -/ +theorem quotientVcomp_id_comp {X Y : B} {first second : Word W X Y} + (alpha : Presented.Hom W first second) : + quotientVcomp W (𝟙 first) alpha = alpha := + @Category.id_comp (Word W X Y) (Presented.wordCategory W X Y) + first second alpha + +/-- Explicit right identity law for quotient vertical composition. -/ +theorem quotientVcomp_comp_id {X Y : B} {first second : Word W X Y} + (alpha : Presented.Hom W first second) : + quotientVcomp W alpha (𝟙 second) = alpha := + @Category.comp_id (Word W X Y) (Presented.wordCategory W X Y) + first second alpha + /-- Quotient interpretation of an aligned hammock in the linear mapping category. -/ def toHom {X Y : B} {source target : LinearWord W X Y} @@ -1551,6 +1579,114 @@ structure HammockPathObject (X Y : B) where namespace HammockPath +/-- Naturality of binary append isomorphisms around a left-whiskered +quotient 2-cell. -/ +theorem appendIso_inv_whiskerLeft_appendIso_hom {X Y Z : B} + {pre pre' : Word W X Y} + {first first' second second' : Word W Y Z} + (left : pre ≅ pre') (source : first ≅ first') + (target : second ≅ second') + (alpha : Presented.Hom W first second) : + (LinearWord.appendIso W left source).inv ≫ + Presented.whiskerLeftHom W pre alpha ≫ + (LinearWord.appendIso W left target).hom = + Presented.whiskerLeftHom W pre' + (source.inv ≫ alpha ≫ target.hom) := by + simp only [LinearWord.appendIso, Iso.trans_hom, Iso.trans_inv, + Bicategory.whiskerLeftIso, Bicategory.whiskerRightIso] + simp only [Category.assoc] + change AlignedCell.quotientVcomp W + (Presented.whiskerLeftHom W pre' source.inv) + (AlignedCell.quotientVcomp W + (Presented.whiskerRightHom W first left.inv) + (AlignedCell.quotientVcomp W + (Presented.whiskerLeftHom W pre alpha) + (AlignedCell.quotientVcomp W + (Presented.whiskerRightHom W second left.hom) + (Presented.whiskerLeftHom W pre' target.hom)))) = + Presented.whiskerLeftHom W pre' + (AlignedCell.quotientVcomp W source.inv + (AlignedCell.quotientVcomp W alpha target.hom)) + rw [← AlignedCell.quotientVcomp_assoc W + (Presented.whiskerRightHom W first left.inv) + (Presented.whiskerLeftHom W pre alpha)] + rw [← AlignedCell.whisker_exchange W left.inv alpha] + rw [AlignedCell.quotientVcomp_assoc] + rw [← AlignedCell.quotientVcomp_assoc W + (Presented.whiskerRightHom W second left.inv) + (Presented.whiskerRightHom W second left.hom)] + rw [← AlignedCell.whiskerRightHom_vcomp W second left.inv left.hom] + have leftCancellation : + AlignedCell.quotientVcomp W left.inv left.hom = 𝟙 pre' := + left.inv_hom_id + rw [leftCancellation] + have whiskerIdentity : + Presented.whiskerRightHom W second (𝟙 pre') = + 𝟙 (Word.append (W := W) pre' second) := + Quot.sound (Presented.Rel.whisker_right_id pre' second) + rw [whiskerIdentity, AlignedCell.quotientVcomp_id_comp] + rw [← AlignedCell.whiskerLeftHom_vcomp W pre' alpha target.hom] + rw [← AlignedCell.whiskerLeftHom_vcomp W pre' source.inv + (AlignedCell.quotientVcomp W alpha target.hom)] + +/-- Naturality of binary append isomorphisms around a right-whiskered +quotient 2-cell. -/ +theorem appendIso_inv_whiskerRight_appendIso_hom {X Y Z : B} + {first first' second second' : Word W X Y} + {post post' : Word W Y Z} + (source : first ≅ first') (target : second ≅ second') + (right : post ≅ post') + (alpha : Presented.Hom W first second) : + (LinearWord.appendIso W source right).inv ≫ + Presented.whiskerRightHom W post alpha ≫ + (LinearWord.appendIso W target right).hom = + Presented.whiskerRightHom W post' + (source.inv ≫ alpha ≫ target.hom) := by + simp only [LinearWord.appendIso, Iso.trans_hom, Iso.trans_inv, + Bicategory.whiskerLeftIso, Bicategory.whiskerRightIso] + simp only [Category.assoc] + change AlignedCell.quotientVcomp W + (Presented.whiskerLeftHom W first' right.inv) + (AlignedCell.quotientVcomp W + (Presented.whiskerRightHom W post source.inv) + (AlignedCell.quotientVcomp W + (Presented.whiskerRightHom W post alpha) + (AlignedCell.quotientVcomp W + (Presented.whiskerRightHom W post target.hom) + (Presented.whiskerLeftHom W second' right.hom)))) = + Presented.whiskerRightHom W post' + (AlignedCell.quotientVcomp W source.inv + (AlignedCell.quotientVcomp W alpha target.hom)) + rw [← AlignedCell.quotientVcomp_assoc W + (Presented.whiskerRightHom W post alpha) + (Presented.whiskerRightHom W post target.hom)] + rw [← AlignedCell.whiskerRightHom_vcomp W post alpha target.hom] + rw [← AlignedCell.quotientVcomp_assoc W + (Presented.whiskerRightHom W post source.inv) + (Presented.whiskerRightHom W post + (AlignedCell.quotientVcomp W alpha target.hom))] + rw [← AlignedCell.whiskerRightHom_vcomp W post source.inv + (AlignedCell.quotientVcomp W alpha target.hom)] + rw [← AlignedCell.quotientVcomp_assoc W + (Presented.whiskerLeftHom W first' right.inv) + (Presented.whiskerRightHom W post + (AlignedCell.quotientVcomp W source.inv + (AlignedCell.quotientVcomp W alpha target.hom)))] + rw [AlignedCell.whisker_exchange W + (AlignedCell.quotientVcomp W source.inv + (AlignedCell.quotientVcomp W alpha target.hom)) right.inv] + rw [AlignedCell.quotientVcomp_assoc] + rw [← AlignedCell.whiskerLeftHom_vcomp W second' right.inv right.hom] + have rightCancellation : + AlignedCell.quotientVcomp W right.inv right.hom = 𝟙 post' := + right.inv_hom_id + rw [rightCancellation] + have whiskerIdentity : + Presented.whiskerLeftHom W second' (𝟙 post') = + 𝟙 (Word.append (W := W) second' post') := + Quot.sound (Presented.Rel.whisker_left_id second' post') + rw [whiskerIdentity, AlignedCell.quotientVcomp_comp_id] + /-- 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. -/ @@ -1582,19 +1718,129 @@ noncomputable def normalizedWhiskerRightHom {X Y Z : B} (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) : +/-- Transport an arbitrary quotient 2-cell to the linear normal forms of its +two binary word endpoints. -/ +noncomputable def normalizedHom {X Y : B} + {first second : Word W X Y} (alpha : Presented.Hom 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) + alpha (LinearWord.normalizationIso W second).hom) +/-- 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)) := + normalizedHom W (Presented.mk W cell) + +/-- Normalization commutes exactly with raw left whiskering. -/ +theorem normalizedHom_whiskerLeft {X Y Z : B} (pre : Word W X Y) + {first second : Word W Y Z} (alpha : Presented.Hom W first second) : + normalizedHom W (Presented.whiskerLeftHom W pre alpha) = + normalizedWhiskerLeftHom W (LinearWord.flatten W pre) + (normalizedHom W alpha) := by + unfold normalizedHom normalizedWhiskerLeftHom + simp only [Word.append_eq_comp, LinearWord.flatten_append] + rw [LinearWord.normalizationIso_append W pre first] + rw [LinearWord.normalizationIso_append W pre second] + simp only [Iso.trans_hom, Iso.trans_inv, Iso.symm_hom, Iso.symm_inv] + let sourceComparison := (LinearWord.toWordAppendIso W + (LinearWord.flatten W pre) (LinearWord.flatten W first)).hom + let targetComparison := (LinearWord.toWordAppendIso W + (LinearWord.flatten W pre) (LinearWord.flatten W second)).inv + let sourceAppend := (LinearWord.appendIso W + (LinearWord.normalizationIso W pre) + (LinearWord.normalizationIso W first)).inv + let targetAppend := (LinearWord.appendIso W + (LinearWord.normalizationIso W pre) + (LinearWord.normalizationIso W second)).hom + let whiskered := Presented.whiskerLeftHom W pre alpha + let normalized := Presented.whiskerLeftHom W + (LinearWord.toWord W (LinearWord.flatten W pre)) + (AlignedCell.quotientVcomp W (LinearWord.normalizationIso W first).inv + (AlignedCell.quotientVcomp W alpha + (LinearWord.normalizationIso W second).hom)) + change AlignedCell.quotientVcomp W + (AlignedCell.quotientVcomp W sourceComparison sourceAppend) + (AlignedCell.quotientVcomp W whiskered + (AlignedCell.quotientVcomp W targetAppend targetComparison)) = + AlignedCell.quotientVcomp W sourceComparison + (AlignedCell.quotientVcomp W normalized targetComparison) + calc + _ = AlignedCell.quotientVcomp W sourceComparison + (AlignedCell.quotientVcomp W + (AlignedCell.quotientVcomp W sourceAppend + (AlignedCell.quotientVcomp W whiskered targetAppend)) + targetComparison) := by + simp only [AlignedCell.quotientVcomp_assoc] + _ = AlignedCell.quotientVcomp W sourceComparison + (AlignedCell.quotientVcomp W normalized targetComparison) := by + rw [show AlignedCell.quotientVcomp W sourceAppend + (AlignedCell.quotientVcomp W whiskered targetAppend) = normalized by + dsimp [sourceAppend, whiskered, targetAppend, normalized] + exact appendIso_inv_whiskerLeft_appendIso_hom W + (LinearWord.normalizationIso W pre) + (LinearWord.normalizationIso W first) + (LinearWord.normalizationIso W second) alpha] + +/-- Normalization commutes exactly with raw right whiskering. -/ +theorem normalizedHom_whiskerRight {X Y Z : B} + {first second : Word W X Y} (alpha : Presented.Hom W first second) + (post : Word W Y Z) : + normalizedHom W (Presented.whiskerRightHom W post alpha) = + normalizedWhiskerRightHom W (LinearWord.flatten W post) + (normalizedHom W alpha) := by + unfold normalizedHom normalizedWhiskerRightHom + simp only [Word.append_eq_comp, LinearWord.flatten_append] + rw [LinearWord.normalizationIso_append W first post] + rw [LinearWord.normalizationIso_append W second post] + simp only [Iso.trans_hom, Iso.trans_inv, Iso.symm_hom, Iso.symm_inv] + let sourceComparison := (LinearWord.toWordAppendIso W + (LinearWord.flatten W first) (LinearWord.flatten W post)).hom + let targetComparison := (LinearWord.toWordAppendIso W + (LinearWord.flatten W second) (LinearWord.flatten W post)).inv + let sourceAppend := (LinearWord.appendIso W + (LinearWord.normalizationIso W first) + (LinearWord.normalizationIso W post)).inv + let targetAppend := (LinearWord.appendIso W + (LinearWord.normalizationIso W second) + (LinearWord.normalizationIso W post)).hom + let whiskered := Presented.whiskerRightHom W post alpha + let normalized := Presented.whiskerRightHom W + (LinearWord.toWord W (LinearWord.flatten W post)) + (AlignedCell.quotientVcomp W (LinearWord.normalizationIso W first).inv + (AlignedCell.quotientVcomp W alpha + (LinearWord.normalizationIso W second).hom)) + change AlignedCell.quotientVcomp W + (AlignedCell.quotientVcomp W sourceComparison sourceAppend) + (AlignedCell.quotientVcomp W whiskered + (AlignedCell.quotientVcomp W targetAppend targetComparison)) = + AlignedCell.quotientVcomp W sourceComparison + (AlignedCell.quotientVcomp W normalized targetComparison) + calc + _ = AlignedCell.quotientVcomp W sourceComparison + (AlignedCell.quotientVcomp W + (AlignedCell.quotientVcomp W sourceAppend + (AlignedCell.quotientVcomp W whiskered targetAppend)) + targetComparison) := by + simp only [AlignedCell.quotientVcomp_assoc] + _ = AlignedCell.quotientVcomp W sourceComparison + (AlignedCell.quotientVcomp W normalized targetComparison) := by + rw [show AlignedCell.quotientVcomp W sourceAppend + (AlignedCell.quotientVcomp W whiskered targetAppend) = normalized by + dsimp [sourceAppend, whiskered, targetAppend, normalized] + exact appendIso_inv_whiskerRight_appendIso_hom W + (LinearWord.normalizationIso W first) + (LinearWord.normalizationIso W second) + (LinearWord.normalizationIso W post) alpha] + end HammockPath /-- A generated hammock path may apply an invertible structural refinement, @@ -2029,6 +2275,142 @@ theorem normalizedCellHom_vcomp {X Y : B} Presented.mk W beta ≫ (LinearWord.normalizationIso W last).hom) simp [Category.assoc] +/-- Raw left whiskering is transported exactly to normalized left +whiskering. -/ +@[simp] +theorem normalizedCellHom_whiskerLeft {X Y Z : B} + (pre : Word W X Y) {first second : Word W Y Z} + (cell : Cell W first second) : + normalizedCellHom W (.whiskerLeft pre cell) = + normalizedWhiskerLeftHom W (LinearWord.flatten W pre) + (normalizedCellHom W cell) := by + exact normalizedHom_whiskerLeft W pre (Presented.mk W cell) + +/-- Raw right whiskering is transported exactly to normalized right +whiskering. -/ +@[simp] +theorem normalizedCellHom_whiskerRight {X Y Z : B} + {first second : Word W X Y} (cell : Cell W first second) + (post : Word W Y Z) : + normalizedCellHom W (.whiskerRight cell post) = + normalizedWhiskerRightHom W (LinearWord.flatten W post) + (normalizedCellHom W cell) := by + exact normalizedHom_whiskerRight W (Presented.mk W cell) post + +/-- The source-identity comparison normalizes to executable deletion of one +forward identity column. -/ +@[simp] +theorem normalizedCellHom_sourceId {X : B} : + normalizedCellHom W (Cell.sourceId (W := W) (X := X)) = + ColumnRefinement.toHom W (.deleteIdentity (.nil X)) := by + unfold normalizedCellHom normalizedHom + simp only [LinearWord.flatten_forward, LinearWord.flatten] + rw [show LinearWord.normalizationIso W (Word.forward W (𝟙 X)) = + (Presented.wordRightUnitorIso W (Word.forward W (𝟙 X))).symm from rfl] + rw [LinearWord.normalizationIso_nil W X] + simp only [Iso.symm_inv, Iso.refl_hom] + rw [ColumnRefinement.toHom_deleteIdentity] + change AlignedCell.quotientVcomp W + (Presented.wordRightUnitorIso W (Word.forward W (𝟙 X))).hom + (AlignedCell.quotientVcomp W + (Presented.mk W (Cell.sourceId (W := W))) (𝟙 (Word.nil X))) = + AlignedCell.quotientVcomp W + (Presented.whiskerRightHom W (.nil X) + (Presented.mk W (Cell.sourceId (W := W)))) + (Presented.wordLeftUnitorIso W (.nil X)).hom + rw [AlignedCell.quotientVcomp_comp_id] + have whiskerEquality : + Presented.whiskerRightHom W (.nil X) + (Presented.mk W (Cell.sourceId (W := W))) = + AlignedCell.quotientVcomp W + (Presented.wordRightUnitorIso W (Word.forward W (𝟙 X))).hom + (AlignedCell.quotientVcomp W + (Presented.mk W (Cell.sourceId (W := W))) + (Presented.wordRightUnitorIso W (.nil X)).inv) := + Quot.sound (Presented.Rel.whisker_right_id_word + (Cell.sourceId (W := W))) + rw [whiskerEquality] + rw [AlignedCell.quotientVcomp_assoc] + rw [AlignedCell.quotientVcomp_assoc W + (Presented.mk W (Cell.sourceId (W := W))) + (Presented.wordRightUnitorIso W (.nil X)).inv + (Presented.wordLeftUnitorIso W (.nil X)).hom] + have unitCancellation : + AlignedCell.quotientVcomp W + (Presented.wordRightUnitorIso W (.nil X)).inv + (Presented.wordLeftUnitorIso W (.nil X)).hom = + 𝟙 (Word.nil X) := by + change (ρ_ (𝟙 (⟨X⟩ : Presented.Localization W))).inv ≫ + (λ_ (𝟙 (⟨X⟩ : Presented.Localization W))).hom = _ + rw [← unitors_inv_equal] + exact (Presented.wordLeftUnitorIso W (.nil X)).inv_hom_id + rw [unitCancellation, AlignedCell.quotientVcomp_comp_id] + +/-- The inverse source-identity comparison normalizes to executable insertion +of one forward identity column. -/ +@[simp] +theorem normalizedCellHom_sourceIdInv {X : B} : + normalizedCellHom W (Cell.sourceIdInv (W := W) (X := X)) = + ColumnRefinement.toHom W (.insertIdentity (.nil X)) := by + unfold normalizedCellHom normalizedHom + simp only [LinearWord.flatten_forward, LinearWord.flatten] + rw [LinearWord.normalizationIso_nil W X] + rw [show LinearWord.normalizationIso W (Word.forward W (𝟙 X)) = + (Presented.wordRightUnitorIso W (Word.forward W (𝟙 X))).symm from rfl] + simp only [Iso.refl_inv, Iso.symm_hom] + rw [ColumnRefinement.toHom_insertIdentity] + change AlignedCell.quotientVcomp W (𝟙 (Word.nil X)) + (AlignedCell.quotientVcomp W + (Presented.mk W (Cell.sourceIdInv (W := W))) + (Presented.wordRightUnitorIso W (Word.forward W (𝟙 X))).inv) = + AlignedCell.quotientVcomp W + (Presented.wordLeftUnitorIso W (.nil X)).inv + (Presented.whiskerRightHom W (.nil X) + (Presented.mk W (Cell.sourceIdInv (W := W)))) + rw [AlignedCell.quotientVcomp_id_comp] + have whiskerEquality : + Presented.whiskerRightHom W (.nil X) + (Presented.mk W (Cell.sourceIdInv (W := W))) = + AlignedCell.quotientVcomp W + (Presented.wordRightUnitorIso W (.nil X)).hom + (AlignedCell.quotientVcomp W + (Presented.mk W (Cell.sourceIdInv (W := W))) + (Presented.wordRightUnitorIso W + (Word.forward W (𝟙 X))).inv) := + Quot.sound (Presented.Rel.whisker_right_id_word + (Cell.sourceIdInv (W := W))) + rw [whiskerEquality] + rw [← AlignedCell.quotientVcomp_assoc W + (Presented.wordLeftUnitorIso W (.nil X)).inv + (Presented.wordRightUnitorIso W (.nil X)).hom] + have unitCancellation : + AlignedCell.quotientVcomp W + (Presented.wordLeftUnitorIso W (.nil X)).inv + (Presented.wordRightUnitorIso W (.nil X)).hom = + 𝟙 (Word.nil X) := by + change (λ_ (𝟙 (⟨X⟩ : Presented.Localization W))).inv ≫ + (ρ_ (𝟙 (⟨X⟩ : Presented.Localization W))).hom = _ + rw [unitors_inv_equal] + exact (Presented.wordRightUnitorIso W (.nil X)).inv_hom_id + rw [unitCancellation, AlignedCell.quotientVcomp_id_comp] + +/-- Equality transport does not change normalized quotient semantics. -/ +@[simp] +theorem normalizedCellHom_transport {X Y : B} + {first second first' second' : Word W X Y} + (sourceEquality : first = first') (targetEquality : second = second') + (cell : Cell W first second) : + normalizedCellHom W (.transport sourceEquality targetEquality cell) = + sourceEquality ▸ targetEquality ▸ normalizedCellHom W cell := by + subst first' + subst second' + unfold normalizedCellHom + have transportEquality : + Presented.mk W (Cell.transport (W := W) rfl rfl cell) = + Presented.mk W cell := + Quot.sound (Presented.Rel.transport_refl cell) + rw [transportEquality] + /-- 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) @@ -2112,6 +2494,126 @@ theorem vcomp_normalizable {X Y : B} rw [Normalizable, normalizedCellHom_vcomp] exact vcomp_mem_semanticImage W hAlpha hBeta +/-- Left whiskering preserves raw-cell normalizability. -/ +theorem whiskerLeft_normalizable {X Y Z : B} + (pre : Word W X Y) {first second : Word W Y Z} + {cell : Cell W first second} (member : Normalizable W cell) : + Normalizable W (.whiskerLeft pre cell) := by + rw [Normalizable, normalizedCellHom_whiskerLeft] + exact whiskerLeft_mem_semanticImage W (LinearWord.flatten W pre) member + +/-- Right whiskering preserves raw-cell normalizability. -/ +theorem whiskerRight_normalizable {X Y Z : B} + {first second : Word W X Y} {cell : Cell W first second} + (member : Normalizable W cell) (post : Word W Y Z) : + Normalizable W (.whiskerRight cell post) := by + rw [Normalizable, normalizedCellHom_whiskerRight] + exact whiskerRight_mem_semanticImage W (LinearWord.flatten W post) member + +/-- The source-identity comparison is hammock-normalizable. -/ +theorem sourceId_normalizable {X : B} : + Normalizable W (Cell.sourceId (W := W) (X := X)) := by + rw [Normalizable, normalizedCellHom_sourceId] + exact refinement_mem_semanticImage W (.deleteIdentity (.nil X)) + +/-- The inverse source-identity comparison is hammock-normalizable. -/ +theorem sourceIdInv_normalizable {X : B} : + Normalizable W (Cell.sourceIdInv (W := W) (X := X)) := by + rw [Normalizable, normalizedCellHom_sourceIdInv] + exact refinement_mem_semanticImage W (.insertIdentity (.nil X)) + +/-- Equality transport preserves raw-cell normalizability. -/ +theorem transport_normalizable {X Y : B} + {first second first' second' : Word W X Y} + (sourceEquality : first = first') (targetEquality : second = second') + {cell : Cell W first second} (member : Normalizable W cell) : + Normalizable W (.transport sourceEquality targetEquality cell) := by + subst first' + subst second' + rw [Normalizable, normalizedCellHom_transport] + exact member + +/-- Exact remaining generator obligations for a complete raw-cell +normalization induction. Identity, vertical composition, original cells, +source identities, both whiskerings, and equality transport are already +discharged separately. -/ +structure StructuralGeneratorNormalizable : Prop where + /-- Source-composition comparison. -/ + sourceComp : ∀ {X Y Z : B} (f : X ⟶ Y) (g : Y ⟶ Z), + Normalizable W (Cell.sourceComp (W := W) f g) + /-- Inverse source-composition comparison. -/ + sourceCompInv : ∀ {X Y Z : B} (f : X ⟶ Y) (g : Y ⟶ Z), + Normalizable W (Cell.sourceCompInv (W := W) f g) + /-- Marked unit. -/ + markedUnit : ∀ {X Y : B} (f : X ⟶ Y) (hf : W f), + Normalizable W (Cell.markedUnit (W := W) f hf) + /-- Inverse marked unit. -/ + markedUnitInv : ∀ {X Y : B} (f : X ⟶ Y) (hf : W f), + Normalizable W (Cell.markedUnitInv (W := W) f hf) + /-- Marked counit. -/ + markedCounit : ∀ {X Y : B} (f : X ⟶ Y) (hf : W f), + Normalizable W (Cell.markedCounit (W := W) f hf) + /-- Inverse marked counit. -/ + markedCounitInv : ∀ {X Y : B} (f : X ⟶ Y) (hf : W f), + Normalizable W (Cell.markedCounitInv (W := W) f hf) + /-- Binary associator. -/ + associator : ∀ {X Y Z T : B} (first : Word W X Y) + (second : Word W Y Z) (third : Word W Z T), + Normalizable W (Cell.associator (W := W) first second third) + /-- Inverse binary associator. -/ + associatorInv : ∀ {X Y Z T : B} (first : Word W X Y) + (second : Word W Y Z) (third : Word W Z T), + Normalizable W (Cell.associatorInv (W := W) first second third) + /-- Binary left unitor. -/ + leftUnitor : ∀ {X Y : B} (word : Word W X Y), + Normalizable W (Cell.leftUnitor (W := W) word) + /-- Inverse binary left unitor. -/ + leftUnitorInv : ∀ {X Y : B} (word : Word W X Y), + Normalizable W (Cell.leftUnitorInv (W := W) word) + /-- Binary right unitor. -/ + rightUnitor : ∀ {X Y : B} (word : Word W X Y), + Normalizable W (Cell.rightUnitor (W := W) word) + /-- Inverse binary right unitor. -/ + rightUnitorInv : ∀ {X Y : B} (word : Word W X Y), + Normalizable W (Cell.rightUnitorInv (W := W) word) + +/-- Complete raw-cell normalization follows by structural induction from the +remaining explicit structural-generator obligations. -/ +theorem normalizable_of_structuralGenerators + (generators : StructuralGeneratorNormalizable W) : + ∀ {X Y : B} {first second : Word W X Y} + (cell : Cell W first second), Normalizable W cell := by + intro X Y first second cell + induction cell with + | id word => exact identity_normalizable W word + | vcomp alpha beta hAlpha hBeta => + exact vcomp_normalizable W hAlpha hBeta + | original alpha => + rw [Normalizable, normalizedCellHom_original] + exact originalCell_mem_semanticImage W alpha + | sourceId => exact sourceId_normalizable W + | sourceIdInv => exact sourceIdInv_normalizable W + | sourceComp f g => exact generators.sourceComp f g + | sourceCompInv f g => exact generators.sourceCompInv f g + | markedUnit f hf => exact generators.markedUnit f hf + | markedUnitInv f hf => exact generators.markedUnitInv f hf + | markedCounit f hf => exact generators.markedCounit f hf + | markedCounitInv f hf => exact generators.markedCounitInv f hf + | whiskerLeft pre cell member => + exact whiskerLeft_normalizable W pre member + | whiskerRight cell post member => + exact whiskerRight_normalizable W member post + | associator first second third => + exact generators.associator first second third + | associatorInv first second third => + exact generators.associatorInv first second third + | leftUnitor word => exact generators.leftUnitor word + | leftUnitorInv word => exact generators.leftUnitorInv word + | rightUnitor word => exact generators.rightUnitor word + | rightUnitorInv word => exact generators.rightUnitorInv word + | transport sourceEquality targetEquality cell member => + exact transport_normalizable W sourceEquality targetEquality member + /-- Original source 2-cells are hammock-normalizable. -/ theorem original_normalizable {X Y : B} {f g : X ⟶ Y} (alpha : f ⟶ g) : diff --git a/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean b/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean index 05b4ed1..fa23c45 100644 --- a/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean +++ b/Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean @@ -64,6 +64,22 @@ def flatten {X Y : B} : Word W X Y → LinearWord W X Y | .nil X => .nil X | .comp first second => append W (flatten first) (flatten second) +/-- Flattening a one-step forward word gives the corresponding singleton +linear row. -/ +@[simp] +theorem flatten_forward {X Y : B} (f : X ⟶ Y) : + flatten W (Word.forward W f) = + .cons (.forward f) (.nil Y) := + rfl + +/-- Flattening a one-step marked reverse gives the corresponding singleton +linear row. -/ +@[simp] +theorem flatten_backward {X Y : B} (f : X ⟶ Y) (hf : W f) : + flatten W (Word.backward W f hf) = + .cons (.backward f hf) (.nil X) := + rfl + /-- Number of oriented steps in a linear word. -/ def length {X Y : B} : LinearWord W X Y → ℕ | .nil _ => 0 @@ -141,6 +157,35 @@ noncomputable def normalizationIso {X Y : B} (word : Word W X Y) : exact appendIso W ihFirst ihSecond ≪≫ (toWordAppendIso W (flatten W first) (flatten W second)).symm +/-- Normalization of one atomic word is inverse right unitor. -/ +theorem normalizationIso_atom {X Y : B} (step : Step W X Y) : + normalizationIso W (Word.atom step) = + (Presented.wordRightUnitorIso W (Word.atom step)).symm := + rfl + +/-- The empty word is already in linear normal form. -/ +theorem normalizationIso_nil (X : B) : + normalizationIso W (Word.nil X) = Iso.refl (Word.nil X) := + rfl + +/-- Flattening binary append is exactly linear append. -/ +@[simp] +theorem flatten_append {X Y Z : B} + (first : Word W X Y) (second : Word W Y Z) : + flatten W (.comp first second) = + append W (flatten W first) (flatten W second) := + rfl + +/-- The canonical normalization of a binary append is horizontal append of +the two endpoint normalizations followed by the canonical linear append +comparison. -/ +theorem normalizationIso_append {X Y Z : B} + (first : Word W X Y) (second : Word W Y Z) : + normalizationIso W (.comp first second) = + appendIso W (normalizationIso W first) (normalizationIso W second) ≪≫ + (toWordAppendIso W (flatten W first) (flatten W second)).symm := + rfl + /-- Linear words form a mapping category by pulling back the quotient 2-cell hom-sets between their binary expansions. -/ instance category (X Y : B) : Category (LinearWord W X Y) where diff --git a/Ript/Higher/CostExactZigzagMappingSpace.lean b/Ript/Higher/CostExactZigzagMappingSpace.lean index d00d6d0..0d1d1b0 100644 --- a/Ript/Higher/CostExactZigzagMappingSpace.lean +++ b/Ript/Higher/CostExactZigzagMappingSpace.lean @@ -33,7 +33,10 @@ 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. 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 +nerve formulas. A raw-cell normalization core records the completed identity, +original, source-identity/inverse, vertical, whiskering, and transport branches +and a conditional all-cell induction from twelve remaining structural +generators. 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. -/ @@ -1344,6 +1347,126 @@ theorem hammockPathWhiskeringCore maps_whiskerRight := hammockPathSemanticComparison_whiskerRightEdge maps_append := hammockPathSemanticComparison_appendEdge +/-- Machine-facing raw-cell normalization fragment for the cost-exact +marking. It records the completed structural-induction cases without claiming +normalization of every raw generator. -/ +structure HammockRawCellNormalizationCore : Prop where + /-- Every raw identity cell is normalizable. -/ + identity : ∀ (M N : ProcessModel.{u, v, w} R) + (word : CostExactZigzag.Word (R := R) M N), + Bicategory.MarkedZigzag.HammockPath.Normalizable + (costExactArrows R) (Bicategory.MarkedZigzag.Cell.id word) + /-- Normalizability is closed under raw vertical composition. -/ + vcomp : ∀ (M N : ProcessModel.{u, v, w} R) + {first middle last : CostExactZigzag.Word (R := R) M N} + {alpha : Bicategory.MarkedZigzag.Cell + (costExactArrows R) first middle} + {beta : Bicategory.MarkedZigzag.Cell + (costExactArrows R) middle last}, + Bicategory.MarkedZigzag.HammockPath.Normalizable + (costExactArrows R) alpha → + Bicategory.MarkedZigzag.HammockPath.Normalizable + (costExactArrows R) beta → + Bicategory.MarkedZigzag.HammockPath.Normalizable + (costExactArrows R) + (Bicategory.MarkedZigzag.Cell.vcomp alpha beta) + /-- Every original source 2-cell is normalizable. -/ + original : ∀ (M N : ProcessModel.{u, v, w} R) + {f g : M ⟶ N} (alpha : f ⟶ g), + Bicategory.MarkedZigzag.HammockPath.Normalizable + (costExactArrows R) + (Bicategory.MarkedZigzag.Cell.original + (W := costExactArrows R) alpha) + /-- The source-identity comparison is normalizable. -/ + sourceId : ∀ (M : ProcessModel.{u, v, w} R), + Bicategory.MarkedZigzag.HammockPath.Normalizable + (costExactArrows R) + (Bicategory.MarkedZigzag.Cell.sourceId + (W := costExactArrows R) (X := M)) + /-- The inverse source-identity comparison is normalizable. -/ + sourceIdInv : ∀ (M : ProcessModel.{u, v, w} R), + Bicategory.MarkedZigzag.HammockPath.Normalizable + (costExactArrows R) + (Bicategory.MarkedZigzag.Cell.sourceIdInv + (W := costExactArrows R) (X := M)) + /-- Raw left whiskering preserves normalizability. -/ + whiskerLeft : ∀ (M N P : ProcessModel.{u, v, w} R) + (pre : CostExactZigzag.Word (R := R) M N) + {first second : CostExactZigzag.Word (R := R) N P} + {cell : Bicategory.MarkedZigzag.Cell + (costExactArrows R) first second}, + Bicategory.MarkedZigzag.HammockPath.Normalizable + (costExactArrows R) cell → + Bicategory.MarkedZigzag.HammockPath.Normalizable + (costExactArrows R) + (Bicategory.MarkedZigzag.Cell.whiskerLeft pre cell) + /-- Raw right whiskering preserves normalizability. -/ + whiskerRight : ∀ (M N P : ProcessModel.{u, v, w} R) + {first second : CostExactZigzag.Word (R := R) M N} + {cell : Bicategory.MarkedZigzag.Cell + (costExactArrows R) first second} + (post : CostExactZigzag.Word (R := R) N P), + Bicategory.MarkedZigzag.HammockPath.Normalizable + (costExactArrows R) cell → + Bicategory.MarkedZigzag.HammockPath.Normalizable + (costExactArrows R) + (Bicategory.MarkedZigzag.Cell.whiskerRight cell post) + /-- Equality transport preserves normalizability. -/ + transport : ∀ (M N : ProcessModel.{u, v, w} R) + {first second first' second' : CostExactZigzag.Word (R := R) M N} + (sourceEquality : first = first') + (targetEquality : second = second') + {cell : Bicategory.MarkedZigzag.Cell + (costExactArrows R) first second}, + Bicategory.MarkedZigzag.HammockPath.Normalizable + (costExactArrows R) cell → + Bicategory.MarkedZigzag.HammockPath.Normalizable + (costExactArrows R) + (Bicategory.MarkedZigzag.Cell.transport + sourceEquality targetEquality cell) + /-- The remaining explicit structural-generator obligations suffice for + normalization of every cost-exact raw cell. -/ + structural_induction : ∀ (M N : ProcessModel.{u, v, w} R), + (@Bicategory.MarkedZigzag.HammockPath.StructuralGeneratorNormalizable + (ProcessModel.{u, v, w} R) _ (costExactArrows R)) → + ∀ {first second : CostExactZigzag.Word (R := R) M N} + (cell : Bicategory.MarkedZigzag.Cell + (costExactArrows R) first second), + Bicategory.MarkedZigzag.HammockPath.Normalizable + (costExactArrows R) cell + +/-- The completed raw-cell induction branches hold uniformly for the +cost-exact marking. -/ +theorem hammockRawCellNormalizationCore : + HammockRawCellNormalizationCore (R := R) where + identity := fun _ _ word => + Bicategory.MarkedZigzag.HammockPath.identity_normalizable + (costExactArrows R) word + vcomp := fun _ _ {_ _ _} {_} {_} hAlpha hBeta => + Bicategory.MarkedZigzag.HammockPath.vcomp_normalizable + (costExactArrows R) hAlpha hBeta + original := fun _ _ {_ _} alpha => + Bicategory.MarkedZigzag.HammockPath.original_normalizable + (costExactArrows R) alpha + sourceId := fun _ => + Bicategory.MarkedZigzag.HammockPath.sourceId_normalizable + (costExactArrows R) + sourceIdInv := fun _ => + Bicategory.MarkedZigzag.HammockPath.sourceIdInv_normalizable + (costExactArrows R) + whiskerLeft := fun _ _ _ pre {_ _} {_} member => + Bicategory.MarkedZigzag.HammockPath.whiskerLeft_normalizable + (costExactArrows R) pre member + whiskerRight := fun _ _ _ {_ _} {_} post member => + Bicategory.MarkedZigzag.HammockPath.whiskerRight_normalizable + (costExactArrows R) member post + transport := fun _ _ {_ _ _ _} sourceEquality targetEquality {_} member => + Bicategory.MarkedZigzag.HammockPath.transport_normalizable + (costExactArrows R) sourceEquality targetEquality member + structural_induction := fun _ _ generators {_ _} cell => + Bicategory.MarkedZigzag.HammockPath.normalizable_of_structuralGenerators + (costExactArrows R) generators cell + /-- 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 989073c..c7bbf8f 100644 --- a/docs/en/RESEARCH_STATUS.md +++ b/docs/en/RESEARCH_STATUS.md @@ -393,11 +393,14 @@ faithful, the old nerve map factors through it strictly, and every source 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. +normalizable, and vertical composition preserves normalizability. Normalization +naturality for raw left/right whiskering is now proved by explicit append-iso +exchange and cancellation; source identity/inverse and equality transport are +normalizable as well. The remaining twelve structural generator obligations +are recorded exactly and already imply all-cell normalization conditionally, +but are not assumed unconditionally. Semantic fullness, competing-move +coherence, reduced-hammock invariance, standard weak-equivalence packaging, and +the global Dwyer--Kan/Rezk theorem remain. 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 cf8fc2d..b5302a6 100644 --- a/docs/en/reference/AXIOMS.md +++ b/docs/en/reference/AXIOMS.md @@ -993,6 +993,27 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.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` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.flatten_forward` | `none` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.flatten_backward` | `none` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_atom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_nil` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_append` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.AlignedCell.quotientVcomp_assoc` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.appendIso_inv_whiskerLeft_appendIso_hom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.appendIso_inv_whiskerRight_appendIso_hom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedHom_whiskerLeft` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedHom_whiskerRight` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_whiskerLeft` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_whiskerRight` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerLeft_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerRight_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceId` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceIdInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceId_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceIdInv_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_transport` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.transport_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizable_of_structuralGenerators` | `[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` | @@ -1016,6 +1037,7 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.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.hammockRawCellNormalizationCore` | `[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 35cbf2b..d404380 100644 --- a/docs/en/reference/BLUEPRINT.md +++ b/docs/en/reference/BLUEPRINT.md @@ -390,9 +390,9 @@ Every node in this graph is an existing compiled module. | 12 (zero-truncated common-refinement mapping nerve) | Wrapped rows form a thin common-refinement groupoid; its canonical functor to the discrete row quotient is faithful, full, essentially surjective, and hence a categorical equivalence; the induced nerve map has categorical-nerve equivalence evidence, an explicit simplicial inverse and both homotopies, and exact row-vertex action | PROVED | | 12 (non-thin semantic refinement-path nerve) | Refinement syntax modulo equality of quotient-cell interpretations forms a non-thin groupoid; executable reversal supplies inverses; its semantic functor into the linear mapping category is faithful and essentially surjective on row objects, maps every path to an isomorphism, and induces a nerve map with exact row-vertex and arbitrary-refinement-edge action; the zero-truncation functor to the thin groupoid is full and essentially surjective | PROVED | | 12 (exact refinement-generated semantic image) | Actual quotient 2-cells equipped with existence of an executable refinement generator form a non-thin image subgroupoid of the linear mapping category; inclusion is faithful, the semantic refinement-path functor is full, faithful, essentially surjective and hence an equivalence onto this exact image, and the induced nerve equivalence has an explicit simplicial homotopy inverse, exact generator-edge action, and strict factorization of the original semantic nerve map | PROVED | -| 12 (aligned-cell-augmented hammock paths) | A non-groupoidal generated path syntax alternates executable refinements with arbitrary aligned raw 2-cells and vertical composition, then quotients only by equality of quotient-cell semantics; normalized left/right whiskering enters and leaves binary append through canonical linear-normal-form isomorphisms, horizontal append composes those operations, and semantic equality/image membership are closed under all three; 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 (aligned-cell-augmented hammock paths) | A non-groupoidal generated path syntax alternates executable refinements with arbitrary aligned raw 2-cells and vertical composition, then quotients only by equality of quotient-cell semantics; normalized left/right whiskering enters and leaves binary append through canonical linear-normal-form isomorphisms, horizontal append composes those operations, and semantic equality/image membership are closed under all three; explicit append-isomorphism exchange/cancellation proves normalization naturality for raw left/right whiskering; raw identity, original, source-identity/inverse, whiskering, vertical-composite, and equality-transport cells are normalizable; `StructuralGeneratorNormalizable` lists exactly the remaining source-composite, marked pair, associator, and unitor obligations and yields all-cell normalization by structural induction; the cost-exact core records these completed branches and conditional induction | PROVED | | 12 (cost-exact two-layer global comparison) | Pseudofunctor-induced functor on homotopy categories; localization-aware relative Rezk map and auxiliary ordinary outer map into the actual marked-zigzag target; explicit source/target outer completeness homotopy equivalences; marked outer arrows factoring through the target actual-equivalence space; packaging with the exact non-groupoidal local nerve comparison; exact vertex, identity, horizontal-composition, associator, and left/right-unitor gluing; arbitrary invertible local 2-cell decoding; explicit pentagon and triangle compatibility | PROVED | -| 12 (global cost-exact complete-Segal/Rezk equivalence) | 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 | +| 12 (global cost-exact complete-Segal/Rezk equivalence) | Discharge the twelve explicit `StructuralGeneratorNormalizable` fields for source composition/inverse, marked unit/counit and inverses, associator/inverse, and left/right unitors and inverses; deduce every presented quotient 2-cell has an alternating aligned/refinement path and hence semantic fullness, then prove critical-pair coherence and reduced-hammock homotopical invariance (or compare the generated path category to another accepted derived mapping-space construction), connect that comparison to a standard weak-equivalence interface, and finish the standard Dwyer--Kan/Rezk weak-equivalence and completeness theorem | OPEN_RESEARCH | ## Finite deterministic copy-discard theorem records diff --git a/docs/en/reference/CONJECTURES.md b/docs/en/reference/CONJECTURES.md index b01f2a4..f5a108e 100644 --- a/docs/en/reference/CONJECTURES.md +++ b/docs/en/reference/CONJECTURES.md @@ -472,10 +472,15 @@ 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. +Normalization naturality for both raw whiskerings is now proved by explicit +append-isomorphism exchange and cancellation; source identity and inverse plus +equality transport are normalizable too. The exact remaining induction basis +is the twelve-field `StructuralGeneratorNormalizable` record: source composite +and inverse, marked unit/counit and inverses, associator and inverse, and both +unitors and inverses. That record already implies normalization of every raw +cell by structural induction, but none of its unproved fields is assumed in an +unconditional theorem. 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. @@ -582,10 +587,11 @@ 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, 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. +vertical-composite, original-cell, both whiskering, source-identity/inverse, +and equality-transport normalization cases are proved. The remaining twelve +structural generator obligations are explicit and sufficient for the complete +induction, but remain unproved; 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 dde1ba3..618d811 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, 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 | +| Rezk classifying diagram | Outer simplicial category of composable interface strings, followed levelwise by the ordinary nerve | Every vertical level and horizontal row is a groupoid nerve and Kan; every horizontal row is strict Segal; the whole outer diagram is naturally `n ↦ Map(Δ[n], N(M.Object))`; `Map(∂Δ[n], N(M.Object))` is the genuine matching limit; every matching map is a fibration; the actual completeness map has an explicit simplicial homotopy inverse | Semantic proof layer; exact project-local `GroupoidalCompleteSegal` and `HomotopyEquivalenceWitness` evidence proved; the full cost-exact localization, common-universe local comparison, localization-aware all-dimensional relative outer Rezk map, source/target completeness witnesses, arbitrary-2-cell one-skeleton glue, vertical local 2-simplex/composite-diagonal glue, degree-one horizontal compositor squares, degree-two vertical pasting/interchange, the explicit three-tetrahedron degree-two compositor prism, all-degree local prism coherence, arbitrary outer-string vertex/restriction comparison, relative-outer gluing of every all-degree prism source vertex, strict decoded-pair naturality for every restriction, exact side-sensitive outer/local glue for every actual target prism-face vertex, a categorical-nerve equivalence from the presented relative-zigzag mapping nerve to every actual target local nerve, strict all-degree local-map factorization, outer essential surjectivity, target-independent algebraic/simplicial presentation universality, an audited `PresentedDwyerKanCore`, an independent right-associated linear hammock mapping category equivalent to the binary presentation and actual target local nerve, an audited `LinearHammockDwyerKanCore`, an exact arbitrary-height row-grid representation of every linear-hammock simplex, exact quotient/nerve interpretation of the fixed-shape aligned multi-column fragment, an executable elementary forward/marked-pair refinement calculus, an object-level common-refinement quotient sound for semantic isomorphism, a zero-truncated thin refinement-groupoid nerve equivalent to the discrete quotient nerve, a non-thin semantic refinement-path groupoid nerve with exact edge action, its categorical/nerve equivalence to the exact refinement-generated quotient-cell image subgroupoid, and a faithful aligned-cell-augmented non-groupoidal path category containing every source 2-cell in canonical one-column form are proved; normalized whiskering/append have exact three-model formulas, normalization commutes with raw whiskering, identity/original/source-identity/transport and closure cases are proved, and a twelve-field criterion implies all-cell normalization; those twelve structural generator fields, semantic fullness, competing-move coherence, reduced-hammock invariance, standard weak-equivalence packaging, and the final Dwyer--Kan comparison remain open | The concrete Boolean model proves that `bit tensor unit` and `unit tensor bit` are unequal syntax trees in Lean while tensor symmetry makes them internally @@ -671,8 +671,10 @@ 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, 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 +left/right whiskering and horizontal append. Normalization now commutes with +both raw whiskerings; raw identity/original/source-identity/inverse and +equality-transport cases plus vertical/whiskering closure are proved. Twelve +explicit source-composite, marked-pair, associator, and unitor obligations are +sufficient for the complete structural induction but remain open, together +with critical-pair coherence and reduced-hammock invariance. These layers do not add `Equiv α β → α = β` and are not a complete presheaf model. diff --git a/docs/eo/RESEARCH_STATUS.md b/docs/eo/RESEARCH_STATUS.md index 9d4a0f6..4d05360 100644 --- a/docs/eo/RESEARCH_STATUS.md +++ b/docs/eo/RESEARCH_STATUS.md @@ -364,10 +364,14 @@ unukolumnan eĝon egalan al la origina kvocienta ĉelo konjugita per dekstraj 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. +kaj vertikala kunmeto konservas normaligeblecon. Normaligo nun estas nature +kongrua kun ambaŭ krudaj whiskering-operacioj; krudaj identecaj, originalaj, +font-identecaj/inversaj kaj transportaj kazoj, kune kun vertikala/whiskering +fermo, estas pruvitaj. La ceteraj dek du source-composite, markitaj paroj, +asociatoraj kaj unuitoraj generatoraj kampoj estas eksplicitaj kaj kondiĉe +implicas normaligon de ĉiu kruda ĉelo, sed ne estas senkondiĉe pruvitaj. +Semantika pleneco, kohereco de kritikaj paroj, reduktita-hammock invariant eco +kaj norma malfort-ekvivalenta pako restas malfermitaj. 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 4eb346c..a21eefe 100644 --- a/docs/eo/reference/AXIOMS.md +++ b/docs/eo/reference/AXIOMS.md @@ -995,6 +995,27 @@ per `scripts/sync-doc-reference-tables.sh` kaj ne estu mane redaktataj. | `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` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.flatten_forward` | `none` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.flatten_backward` | `none` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_atom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_nil` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_append` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.AlignedCell.quotientVcomp_assoc` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.appendIso_inv_whiskerLeft_appendIso_hom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.appendIso_inv_whiskerRight_appendIso_hom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedHom_whiskerLeft` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedHom_whiskerRight` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_whiskerLeft` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_whiskerRight` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerLeft_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerRight_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceId` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceIdInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceId_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceIdInv_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_transport` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.transport_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizable_of_structuralGenerators` | `[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` | @@ -1018,6 +1039,7 @@ per `scripts/sync-doc-reference-tables.sh` kaj ne estu mane redaktataj. | `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.hammockRawCellNormalizationCore` | `[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 fb77141..0205a74 100644 --- a/docs/ja/RESEARCH_STATUS.md +++ b/docs/ja/RESEARCH_STATUS.md @@ -151,7 +151,7 @@ fold は一意な解釈です。生成合同は全代数で健全で、木項モ 制限付きながら真に独立した右結合 linear hammock 対象モデルもできました。typed step 列は二分 words と相互変換・平坦化され、長さを厳密に保存し、同値な mapping category、nerve の明示的ホモトピー逆、実際の対象 local nerve への直接比較を与えます。`LinearHammockDwyerKanCore` はこれを outer essential surjectivity と統合します。古典的な任意グリッド hammock または他の受理された derived 構成との比較は未解決です。 -任意高さの垂直 grid も明示化されました。`n`-grid は `n + 1` 行の linear hammocks、`n` 本の隣接商 2-cell 辺、全端点方程式を持ち、strict-Segal 再構成により linear hammock nerve の `n`-simplex と同値です。行、辺、復号、双方向 round trip は厳密に証明されています。固定形状の水平多列部分も形式化されました。同形の行は各共通列に一つの raw atomic 2-cell を持ち、幅と実行可能な水平 append は厳密で、商解釈は interchange により列ごとの恒等と垂直合成を保存し、任意高さの aligned grid は行と解釈済み辺を厳密に保つ genuine simplex を再構成します。基本的な前向き列 refinement も実行可能です。恒等列の挿入/削除、合成列の展開/縮約、任意の共通 prefix 下での move、推移合成、符号付き幅変化、商意味論での双方向 cancellation が証明されています。marked reverse 構造にも unit pair `f ; f⁻¹` と counit pair `f⁻¹ ; f` の実行可能な挿入/削除が加わり、符号付き幅 `±2`、厳密な意味同型、双方向 round trip、任意 prefix 安定性が証明されました。各 refinement は実行可能な逆と統一意味同型を持ちます。二本脚 common-refinement span は同値関係と行商を構成し、商等式は common-refinability と同値で、対象等式を仮定せず意味同型を与えます。0-切断 mapping 層も完成しました。包装された行は薄い common-refinement 群胚を構成し、離散行商圏と圏同値で、nerve 比較には明示的単体逆と両ホモトピーがあります。非薄意味 refinement-path 群胚は quotient-cell 意味で異なる paths を保持し、linear mapping nerve への nerve map は faithful、行対象上 essentially surjective、全 path を同型へ写し、厳密な頂点/辺式を持ちます。薄群胚への 0-切断も full かつ essentially surjective です。実際の商 2-cell と「実行可能な refinement が生成する」という存在証明は厳密な意味像群胚を構成します。path 群胚はこれと圏同値で、nerve 比較は明示的単体ホモトピー逆を持ち、完全な linear mapping category への像包含は faithful、元の意味 nerve map は厳密にこの像を経由します。さらに大きい非群胚生成 path 圏は refinement と任意の aligned raw 2-cell を交互に合成できます。意味関手と refinement 埋め込みはいずれも faithful で、旧 nerve map は厳密にこれを経由し、各始域 2-cell は right-unitor で共役された元の商 2-cell に等しい正準一列辺を持ちます。正規化された左右 whiskering と水平 append は意味同値と像所属を保存し、厳密な三モデル nerve 公式を持ちます。raw identity/original cell は正規化可能で、垂直合成は正規化可能性を保存します。未解決なのは、正規化同型の raw whiskering に対する自然性、残る構造生成元の正規化、critical-pair coherence、reduced-hammock 不変性、標準弱同値 packaging です。 +任意高さの垂直 grid も明示化されました。`n`-grid は `n + 1` 行の linear hammocks、`n` 本の隣接商 2-cell 辺、全端点方程式を持ち、strict-Segal 再構成により linear hammock nerve の `n`-simplex と同値です。行、辺、復号、双方向 round trip は厳密に証明されています。固定形状の水平多列部分も形式化されました。同形の行は各共通列に一つの raw atomic 2-cell を持ち、幅と実行可能な水平 append は厳密で、商解釈は interchange により列ごとの恒等と垂直合成を保存し、任意高さの aligned grid は行と解釈済み辺を厳密に保つ genuine simplex を再構成します。基本的な前向き列 refinement も実行可能です。恒等列の挿入/削除、合成列の展開/縮約、任意の共通 prefix 下での move、推移合成、符号付き幅変化、商意味論での双方向 cancellation が証明されています。marked reverse 構造にも unit pair `f ; f⁻¹` と counit pair `f⁻¹ ; f` の実行可能な挿入/削除が加わり、符号付き幅 `±2`、厳密な意味同型、双方向 round trip、任意 prefix 安定性が証明されました。各 refinement は実行可能な逆と統一意味同型を持ちます。二本脚 common-refinement span は同値関係と行商を構成し、商等式は common-refinability と同値で、対象等式を仮定せず意味同型を与えます。0-切断 mapping 層も完成しました。包装された行は薄い common-refinement 群胚を構成し、離散行商圏と圏同値で、nerve 比較には明示的単体逆と両ホモトピーがあります。非薄意味 refinement-path 群胚は quotient-cell 意味で異なる paths を保持し、linear mapping nerve への nerve map は faithful、行対象上 essentially surjective、全 path を同型へ写し、厳密な頂点/辺式を持ちます。薄群胚への 0-切断も full かつ essentially surjective です。実際の商 2-cell と「実行可能な refinement が生成する」という存在証明は厳密な意味像群胚を構成します。path 群胚はこれと圏同値で、nerve 比較は明示的単体ホモトピー逆を持ち、完全な linear mapping category への像包含は faithful、元の意味 nerve map は厳密にこの像を経由します。さらに大きい非群胚生成 path 圏は refinement と任意の aligned raw 2-cell を交互に合成できます。意味関手と refinement 埋め込みはいずれも faithful で、旧 nerve map は厳密にこれを経由し、各始域 2-cell は right-unitor で共役された元の商 2-cell に等しい正準一列辺を持ちます。正規化された左右 whiskering と水平 append は意味同値と像所属を保存し、厳密な三モデル nerve 公式を持ちます。正規化は raw 左右 whiskering と自然に可換することが証明され、raw identity、original、source identity/逆、transport、および垂直/whiskering 閉包分岐が完成しました。残る十二の source-composite、marked pair、associator、unitor 構造生成元フィールドは明示され、条件付きで全 raw Cell 正規化を導きますが、まだ無条件には証明されていません。semantic fullness、critical-pair coherence、reduced-hammock 不変性、標準弱同値 packaging は未解決です。 異なる資源代数のモデルは順序付き加法準同型で比較できます。直列、並列、構造、予算則が再添字 付けされ、異種強モデル射は資源写像とともに合成します。これらは、資源代数とモデルを対象、 diff --git a/docs/ja/reference/AXIOMS.md b/docs/ja/reference/AXIOMS.md index bb0dd32..1d898ea 100644 --- a/docs/ja/reference/AXIOMS.md +++ b/docs/ja/reference/AXIOMS.md @@ -993,6 +993,27 @@ | `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` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.flatten_forward` | `none` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.flatten_backward` | `none` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_atom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_nil` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_append` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.AlignedCell.quotientVcomp_assoc` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.appendIso_inv_whiskerLeft_appendIso_hom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.appendIso_inv_whiskerRight_appendIso_hom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedHom_whiskerLeft` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedHom_whiskerRight` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_whiskerLeft` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_whiskerRight` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerLeft_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerRight_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceId` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceIdInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceId_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceIdInv_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_transport` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.transport_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizable_of_structuralGenerators` | `[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` | @@ -1016,6 +1037,7 @@ | `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.hammockRawCellNormalizationCore` | `[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 40577ea..dc8a3d1 100644 --- a/docs/zh-CN/RESEARCH_STATUS.md +++ b/docs/zh-CN/RESEARCH_STATUS.md @@ -144,7 +144,7 @@ quarter/half-flip 树分别实现为概率、保留相干的随机酉量子仪 现已有受限但真正独立的右结合 linear hammock 对象模型：typed step 列表与二叉 words 相互转换和扁平化，精确保留长度，并给出等价 mapping category、nerve 显式同伦逆以及到实际 target local nerve 的直接比较。`LinearHammockDwyerKanCore` 将其与 outer essential surjectivity 组合。尚缺与经典任意网格 hammock 或其他认可 derived 构造的比较。 -任意高度的纵向 grid 现也已显式化：`n`-grid 包含 `n + 1` 行 linear hammocks、`n` 条相邻商 2-胞腔边和全部端点方程，strict-Segal 重构将其与 linear hammock nerve 的 `n`-simplices 等价，并精确证明行、边、解码和双向 round trip。固定形状的横向多列片段也已形式化：等形行的每个公共列含一个原始原子 2-胞腔，宽度与可执行横向拼接精确，商解释通过 interchange 保持逐列恒等和纵向合成，任意高度 aligned grid 重构为具有精确行和解释边的真实 simplex。基本前向列细化也已可执行：恒等列可插入/删除，复合列可展开/收缩，move 可在任意公共前缀下提升并传递复合；带符号宽度变化精确，两个生成器对在商语义中双向抵消。marked reverse 结构现在也包含可执行的 unit pair `f ; f⁻¹` 与 counit pair `f⁻¹ ; f` 插入/删除，其带符号宽度为 `±2`，语义同构、双向 round trip 和任意前缀稳定性均已证明。每个 refinement 现有可执行逆向和统一语义同构；双腿 common-refinement span 构成等价关系及行商，商相等精确等价于可共同细化，并只推出语义同构而非对象相等。0-截断 mapping 层也已完成：包装行构成薄 common-refinement 群胚，并与离散行商范畴等价；nerve 比较具有显式单纯逆和双向同伦。非薄语义 refinement-path 群胚现保留按 quotient-cell 语义区分的路径；其 nerve map 到 linear mapping nerve 对态射 faithful、对行对象本质满、将全部路径映为同构并具有精确顶点/边公式，且到薄群胚的 0-截断 full 且本质满。实际商 2-胞腔连同“由可执行 refinement 生成”的存在见证现构成精确语义像群胚；路径群胚与其范畴等价，nerve 比较具有显式单纯同伦逆，像包含到完整 linear mapping category 忠实，原语义 nerve map 严格经过它。更大的非群胚生成路径范畴现可交替复合 refinement 与任意 aligned raw 2-胞腔；其语义及 refinement 嵌入均 faithful，旧 nerve map 严格经过它，并且每个源 2-胞腔都有一个规范单列边，其商语义是由左右规范 right-unitor 共轭的原 2-胞腔。规范左右 whiskering 与横向 append 现保持语义等价和像成员资格，并具有精确三模型 nerve 公式；raw 恒等与 original 胞腔已可正规化，纵向复合保持可正规化性。仍缺证明正规化同构对 raw whiskering 的自然性、正规化其余结构生成元、critical-pair 协调、约化 hammock 不变性及标准弱等价封装。 +任意高度的纵向 grid 现也已显式化：`n`-grid 包含 `n + 1` 行 linear hammocks、`n` 条相邻商 2-胞腔边和全部端点方程，strict-Segal 重构将其与 linear hammock nerve 的 `n`-simplices 等价，并精确证明行、边、解码和双向 round trip。固定形状的横向多列片段也已形式化：等形行的每个公共列含一个原始原子 2-胞腔，宽度与可执行横向拼接精确，商解释通过 interchange 保持逐列恒等和纵向合成，任意高度 aligned grid 重构为具有精确行和解释边的真实 simplex。基本前向列细化也已可执行：恒等列可插入/删除，复合列可展开/收缩，move 可在任意公共前缀下提升并传递复合；带符号宽度变化精确，两个生成器对在商语义中双向抵消。marked reverse 结构现在也包含可执行的 unit pair `f ; f⁻¹` 与 counit pair `f⁻¹ ; f` 插入/删除，其带符号宽度为 `±2`，语义同构、双向 round trip 和任意前缀稳定性均已证明。每个 refinement 现有可执行逆向和统一语义同构；双腿 common-refinement span 构成等价关系及行商，商相等精确等价于可共同细化，并只推出语义同构而非对象相等。0-截断 mapping 层也已完成：包装行构成薄 common-refinement 群胚，并与离散行商范畴等价；nerve 比较具有显式单纯逆和双向同伦。非薄语义 refinement-path 群胚现保留按 quotient-cell 语义区分的路径；其 nerve map 到 linear mapping nerve 对态射 faithful、对行对象本质满、将全部路径映为同构并具有精确顶点/边公式，且到薄群胚的 0-截断 full 且本质满。实际商 2-胞腔连同“由可执行 refinement 生成”的存在见证现构成精确语义像群胚；路径群胚与其范畴等价，nerve 比较具有显式单纯同伦逆，像包含到完整 linear mapping category 忠实，原语义 nerve map 严格经过它。更大的非群胚生成路径范畴现可交替复合 refinement 与任意 aligned raw 2-胞腔；其语义及 refinement 嵌入均 faithful，旧 nerve map 严格经过它，并且每个源 2-胞腔都有一个规范单列边，其商语义是由左右规范 right-unitor 共轭的原 2-胞腔。规范左右 whiskering 与横向 append 现保持语义等价和像成员资格，并具有精确三模型 nerve 公式。正规化现已证明与 raw 左右 whiskering 自然相容；raw 恒等、original、source identity/逆、transport 及纵向/whiskering 闭包分支均已完成。剩余十二个 source-composite、marked pair、associator 和 unitor 结构生成元字段被精确登记，并在条件下推出全部 raw Cell 正规化，但尚未无条件证明；semantic fullness、critical-pair 协调、约化 hammock 不变性及标准弱等价封装仍开放。 模型比较不再要求全局使用同一资源代数。有序加法同态重索引串行、并行、结构和预算律；跨资源 代数的强辫模型态射随同态复合，并在每个固定资源映射上形成单子自然变换的局部范畴。四维计算 diff --git a/docs/zh-CN/reference/AXIOMS.md b/docs/zh-CN/reference/AXIOMS.md index c530616..557e730 100644 --- a/docs/zh-CN/reference/AXIOMS.md +++ b/docs/zh-CN/reference/AXIOMS.md @@ -993,6 +993,27 @@ | `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` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.flatten_forward` | `none` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.flatten_backward` | `none` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_atom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_nil` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.LinearWord.normalizationIso_append` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagLinearHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.AlignedCell.quotientVcomp_assoc` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.appendIso_inv_whiskerLeft_appendIso_hom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.appendIso_inv_whiskerRight_appendIso_hom` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedHom_whiskerLeft` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedHom_whiskerRight` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_whiskerLeft` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_whiskerRight` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerLeft_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.whiskerRight_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceId` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_sourceIdInv` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceId_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.sourceIdInv_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizedCellHom_transport` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.transport_normalizable` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` | +| `CategoryTheory.Bicategory.MarkedZigzag.HammockPath.normalizable_of_structuralGenerators` | `[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` | @@ -1016,6 +1037,7 @@ | `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.hammockRawCellNormalizationCore` | `[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` |