feat(higher): characterize refinement semantic image

AXIOMS.md

@@ -963,6 +963,13 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.lean`.
 | `CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.semanticFunctor_map_isIso` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
 | `CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.toThinFunctor_full` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
 | `CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.toThinFunctor_essSurj` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.isGroupoid` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.inclusion_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_full` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_faithful` | `[Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_essSurj` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
+| `CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.semanticFunctor_factorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/MarkedZigzagAlignedHammock.lean` |
 | `Ript.Higher.CostExactZigzagMappingSpace.AlignedHammockGrid.linearHammockGridEquiv_simplex` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` |
 | `Ript.Higher.CostExactZigzagMappingSpace.alignedHammockCore` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` |
 | `Ript.Higher.CostExactZigzagMappingSpace.columnRefinementCore` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` |
@@ -973,6 +980,11 @@ the actual output of `lake env lean Ript/Audit/AxiomChecks.lean`.
 | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_vertex` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` |
 | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_edge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` |
 | `Ript.Higher.CostExactZigzagMappingSpace.refinementPathNerveCore` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` |
+| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageNerveEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` |
+| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageHomotopyEquivalence` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` |
+| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_factorization` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` |
+| `Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageComparison_edge` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` |
+| `Ript.Higher.CostExactZigzagMappingSpace.refinementImageNerveCore` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` |
 | `Ript.Higher.CostExactZigzagMappingSpace.core` | `[propext, Classical.choice, Quot.sound]` | `Ript/Higher/CostExactZigzagMappingSpace.lean` |
 | `CategoryTheory.Pseudofunctor.homotopyFunctor` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/PseudofunctorHomotopy.lean` |
 | `CategoryTheory.Pseudofunctor.homotopyFunctor_map_homMk` | `[propext, Classical.choice, Quot.sound]` | `Ript/ForMathlib/CategoryTheory/Bicategory/PseudofunctorHomotopy.lean` |

BLUEPRINT.md

@@ -389,8 +389,9 @@ Every node in this graph is an existing compiled module.
 | 12 (common-refinement row quotient) | Every executable refinement has an executable reverse with negated signed width and one unified semantic isomorphism whose forward map is the quotient-cell interpretation; explicit two-leg common-refinement spans are reflexive, symmetric, and transitive; their setoid quotient identifies every refinement endpoint, quotient equality is exactly common-refinability, and every quotient equality yields a semantic isomorphism without assuming object equality | PROVED |
 | 12 (zero-truncated common-refinement mapping nerve) | Wrapped rows form a thin common-refinement groupoid; its canonical functor to the discrete row quotient is faithful, full, essentially surjective, and hence a categorical equivalence; the induced nerve map has categorical-nerve equivalence evidence, an explicit simplicial inverse and both homotopies, and exact row-vertex action | PROVED |
 | 12 (non-thin semantic refinement-path nerve) | Refinement syntax modulo equality of quotient-cell interpretations forms a non-thin groupoid; executable reversal supplies inverses; its semantic functor into the linear mapping category is faithful and essentially surjective on row objects, maps every path to an isomorphism, and induces a nerve map with exact row-vertex and arbitrary-refinement-edge action; the zero-truncation functor to the thin groupoid is full and essentially surjective | PROVED |
+| 12 (exact refinement-generated semantic image) | Actual quotient 2-cells equipped with existence of an executable refinement generator form a non-thin image subgroupoid of the linear mapping category; inclusion is faithful, the semantic refinement-path functor is full, faithful, essentially surjective and hence an equivalence onto this exact image, and the induced nerve equivalence has an explicit simplicial homotopy inverse, exact generator-edge action, and strict factorization of the original semantic nerve map | PROVED |
 | 12 (cost-exact two-layer global comparison) | Pseudofunctor-induced functor on homotopy categories; localization-aware relative Rezk map and auxiliary ordinary outer map into the actual marked-zigzag target; explicit source/target outer completeness homotopy equivalences; marked outer arrows factoring through the target actual-equivalence space; packaging with the exact non-groupoidal local nerve comparison; exact vertex, identity, horizontal-composition, associator, and left/right-unitor gluing; arbitrary invertible local 2-cell decoding; explicit pentagon and triangle compatibility | PROVED |
-| 12 (global cost-exact complete-Segal/Rezk equivalence) | Characterize or enlarge the faithful non-thin refinement-path image inside the full linear mapping category, prove critical-pair coherence and reduced-hammock homotopical invariance (or compare it to another accepted derived mapping-space construction), connect that comparison to a standard weak-equivalence interface, and finish the standard Dwyer--Kan/Rezk weak-equivalence and completeness theorem | OPEN_RESEARCH |
+| 12 (global cost-exact complete-Segal/Rezk equivalence) | Prove that the exact refinement-generated semantic image covers the required derived/hammock mapping core (or characterize and add the missing linear quotient 2-cells), prove critical-pair coherence and reduced-hammock homotopical invariance (or compare it to another accepted derived mapping-space construction), connect that comparison to a standard weak-equivalence interface, and finish the standard Dwyer--Kan/Rezk weak-equivalence and completeness theorem | OPEN_RESEARCH |
 
 ## Finite deterministic copy-discard theorem records
 

CONJECTURES.md

@@ -459,10 +459,15 @@ isomorphism, not Lean object equality. A non-thin semantic refinement-path
 groupoid is now compiled as well: paths are quotiented only by equality of
 their quotient-cell interpretations, executable reversal gives inverses, and
 the semantic functor into the linear mapping category is faithful and
-essentially surjective on row objects with exact nerve edge action. The
-remaining classical gap is fullness or an exact image characterization,
-coherence for competing forward/marked moves, reduced-hammock moves, and their
-homotopical invariance.
+essentially surjective on row objects with exact nerve edge action. Its exact
+semantic image has now been internalized as the subgroupoid of actual quotient
+2-cells carrying an executable-refinement witness: paths are equivalent to
+this image, the image inclusion is faithful, the nerve equivalence has an
+explicit simplicial homotopy inverse, and semantic interpretation factors
+through it strictly. The remaining classical gap is proving that this exact
+image covers the required derived/hammock core (or adding the missing linear
+quotient 2-cells), together with coherence for competing forward/marked moves,
+reduced-hammock moves, and their homotopical invariance.
 The 0-truncated layer is now compiled separately: wrapped rows form a thin
 common-refinement groupoid categorically equivalent to the discrete row
 quotient, and its nerve comparison has an explicit simplicial homotopy inverse.
@@ -562,9 +567,12 @@ and semantic inverse laws. Their object-level common-refinement quotient and
 semantic-isomorphism soundness are now proved. A quotient mapping nerve,
 in the precise 0-truncated sense, is also proved via the thin refinement
 groupoid/discrete-quotient nerve equivalence. A non-thin refinement-path nerve,
-with faithful exact semantic action, is now proved too. Fullness/image
-characterization, critical-pair coherence, and reduced-hammock invariance
-remain open.
+with faithful exact semantic action, is now proved too. It is categorically
+and simplicially equivalent to the exact subgroupoid of refinement-generated
+quotient 2-cells, which includes faithfully in the full linear mapping
+category and strictly factors the semantic nerve map. Coverage of the required
+derived/hammock mapping core by this exact image, critical-pair coherence, and
+reduced-hammock invariance remain open.
 
 The first complete construction against that predicate is now kernel checked.
 Identity precomposition is an adjoint equivalence of pseudofunctors and an

MODEL_MATRIX.md

@@ -564,7 +564,7 @@ or the executable cores.
 | Presheaf universe | Type-valued presheaves on the internal groupoid | Yoneda is fully faithful; representable transformations/isomorphisms correspond to internal identity/equivalence | Semantic proof layer; Mathlib Yoneda audits with classical choice |
 | Yoneda envelope | Essential image of representables in the presheaf universe | Groupoid equivalent to the internal groupoid; inclusion factors Yoneda; the restricted Yoneda functor is a Mathlib localization at all internal identities | Noncomputable essential-image witnesses; exact ordinary localization of an already-groupoidal source, not a Rezk completion |
 | Simplicial interface nerve | Ordinary categorical nerve of the internal groupoid | Complete Kan horn filling, strict Segal, quasicategory, 2-coskeletal; vertices/edges/2-simplices encode interfaces, identities, and composition; homotopy category recovers the groupoid | Semantic proof layer; chosen fillers audit with classical choice; no complete-Segal or Rezk claim |
-| Rezk classifying diagram | Outer simplicial category of composable interface strings, followed levelwise by the ordinary nerve | Every vertical level and horizontal row is a groupoid nerve and Kan; every horizontal row is strict Segal; the whole outer diagram is naturally `n ↦ Map(Δ[n], N(M.Object))`; `Map(∂Δ[n], N(M.Object))` is the genuine matching limit; every matching map is a fibration; the actual completeness map has an explicit simplicial homotopy inverse | Semantic proof layer; exact project-local `GroupoidalCompleteSegal` and `HomotopyEquivalenceWitness` evidence proved; the full cost-exact localization, common-universe local comparison, localization-aware all-dimensional relative outer Rezk map, source/target completeness witnesses, arbitrary-2-cell one-skeleton glue, vertical local 2-simplex/composite-diagonal glue, degree-one horizontal compositor squares, degree-two vertical pasting/interchange, the explicit three-tetrahedron degree-two compositor prism, all-degree local prism coherence, arbitrary outer-string vertex/restriction comparison, relative-outer gluing of every all-degree prism source vertex, strict decoded-pair naturality for every restriction, exact side-sensitive outer/local glue for every actual target prism-face vertex, a categorical-nerve equivalence from the presented relative-zigzag mapping nerve to every actual target local nerve, strict all-degree local-map factorization, outer essential surjectivity, target-independent algebraic/simplicial presentation universality, an audited `PresentedDwyerKanCore`, an independent right-associated linear hammock mapping category equivalent to the binary presentation and actual target local nerve, an audited `LinearHammockDwyerKanCore`, an exact arbitrary-height row-grid representation of every linear-hammock simplex, exact quotient/nerve interpretation of the fixed-shape aligned multi-column fragment, an executable elementary forward/marked-pair refinement calculus, an object-level common-refinement quotient sound for semantic isomorphism, a zero-truncated thin refinement-groupoid nerve equivalent to the discrete quotient nerve, and a non-thin semantic refinement-path groupoid nerve faithfully and object-essentially-surjectively mapped into the linear mapping nerve with exact edge action are proved; fullness/image characterization, competing-move coherence, reduced-hammock invariance, standard weak-equivalence packaging, and the final Dwyer--Kan comparison remain open |
+| Rezk classifying diagram | Outer simplicial category of composable interface strings, followed levelwise by the ordinary nerve | Every vertical level and horizontal row is a groupoid nerve and Kan; every horizontal row is strict Segal; the whole outer diagram is naturally `n ↦ Map(Δ[n], N(M.Object))`; `Map(∂Δ[n], N(M.Object))` is the genuine matching limit; every matching map is a fibration; the actual completeness map has an explicit simplicial homotopy inverse | Semantic proof layer; exact project-local `GroupoidalCompleteSegal` and `HomotopyEquivalenceWitness` evidence proved; the full cost-exact localization, common-universe local comparison, localization-aware all-dimensional relative outer Rezk map, source/target completeness witnesses, arbitrary-2-cell one-skeleton glue, vertical local 2-simplex/composite-diagonal glue, degree-one horizontal compositor squares, degree-two vertical pasting/interchange, the explicit three-tetrahedron degree-two compositor prism, all-degree local prism coherence, arbitrary outer-string vertex/restriction comparison, relative-outer gluing of every all-degree prism source vertex, strict decoded-pair naturality for every restriction, exact side-sensitive outer/local glue for every actual target prism-face vertex, a categorical-nerve equivalence from the presented relative-zigzag mapping nerve to every actual target local nerve, strict all-degree local-map factorization, outer essential surjectivity, target-independent algebraic/simplicial presentation universality, an audited `PresentedDwyerKanCore`, an independent right-associated linear hammock mapping category equivalent to the binary presentation and actual target local nerve, an audited `LinearHammockDwyerKanCore`, an exact arbitrary-height row-grid representation of every linear-hammock simplex, exact quotient/nerve interpretation of the fixed-shape aligned multi-column fragment, an executable elementary forward/marked-pair refinement calculus, an object-level common-refinement quotient sound for semantic isomorphism, a zero-truncated thin refinement-groupoid nerve equivalent to the discrete quotient nerve, a non-thin semantic refinement-path groupoid nerve with exact edge action, and its categorical/nerve equivalence to the exact refinement-generated quotient-cell image subgroupoid with faithful linear inclusion and strict semantic factorization are proved; coverage of the required derived/hammock core by that exact image, competing-move coherence, reduced-hammock invariance, standard weak-equivalence packaging, and the final Dwyer--Kan comparison remain open |
 
 The concrete Boolean model proves that `bit tensor unit` and `unit tensor bit`
 are unequal syntax trees in Lean while tensor symmetry makes them internally
@@ -665,6 +665,9 @@ to the discrete row quotient, and the nerve map has an explicit simplicial
 homotopy inverse. The non-thin semantic path groupoid
 and its faithful, object-essentially-surjective nerve map now compile, with
 exact refinement-edge interpretation and full zero-truncation onto the thin
-groupoid. What remains is fullness or an exact image characterization,
-critical-pair coherence, and reduced-hammock invariance. These
+groupoid. Its exact refinement-generated quotient-cell image is now a
+subgroupoid equivalent to the path groupoid, with a faithful inclusion into
+the full linear mapping category and a strictly factored semantic nerve map.
+What remains is coverage of the required derived/hammock core by that exact
+image, critical-pair coherence, and reduced-hammock invariance. These
 layers do not add `Equiv α β → α = β` and are not a complete presheaf model.

Ript/Audit/AxiomChecks.lean

@@ -1044,6 +1044,13 @@ set_option autoImplicit false
 #print axioms CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.semanticFunctor_map_isIso
 #print axioms CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.toThinFunctor_full
 #print axioms CategoryTheory.Bicategory.MarkedZigzag.RefinementPath.toThinFunctor_essSurj
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.isGroupoid
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.inclusion_faithful
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_full
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_faithful
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathFunctor_essSurj
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.pathEquivalence
+#print axioms CategoryTheory.Bicategory.MarkedZigzag.RefinementImage.semanticFunctor_factorization
 #print axioms Ript.Higher.CostExactZigzagMappingSpace.AlignedHammockGrid.linearHammockGridEquiv_simplex
 #print axioms Ript.Higher.CostExactZigzagMappingSpace.alignedHammockCore
 #print axioms Ript.Higher.CostExactZigzagMappingSpace.columnRefinementCore
@@ -1054,6 +1061,11 @@ set_option autoImplicit false
 #print axioms Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_vertex
 #print axioms Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_edge
 #print axioms Ript.Higher.CostExactZigzagMappingSpace.refinementPathNerveCore
+#print axioms Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageNerveEquivalence
+#print axioms Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageHomotopyEquivalence
+#print axioms Ript.Higher.CostExactZigzagMappingSpace.refinementPathSemanticComparison_factorization
+#print axioms Ript.Higher.CostExactZigzagMappingSpace.refinementPathImageComparison_edge
+#print axioms Ript.Higher.CostExactZigzagMappingSpace.refinementImageNerveCore
 #print axioms Ript.Higher.CostExactZigzagMappingSpace.core
 #print axioms CategoryTheory.Pseudofunctor.homotopyFunctor
 #print axioms CategoryTheory.Pseudofunctor.homotopyFunctor_map_homMk