diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,15 @@
 # Changelog
 
+## 1.1.0.0 - 2026-08-21
+
+- Breaking: replace the lossy import-category projection with a
+  provenance-preserving site kernel and total object lookup.
+- Breaking: replace fallible nerve-chain vertex recovery with total validated
+  chain vertices, and rename the normalized and identity-inclusive nerve
+  constructors to make their semantic and resource distinction explicit.
+- Compatibility: build the complete test and benchmark closure on GHC 9.10.3,
+  9.12.4, and 9.14.1 through `moonlight-pale:test-0.1.0.2` and `base >= 4.20`.
+
 ## 1.0.0.0 - 2026-08-20
 
 - Publish the validated GHC 9.10.3, 9.12.4, and 9.14.1 public-library surface
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -45,13 +45,13 @@
 
 ## Public modules
 
-| Module | Surface |
-| --- | --- |
-| `Moonlight.Category` | The broad categorical surface: `Category` and composition, the limit/colimit and higher-category towers, finite and thin categories, invertibility/groupoids, adhesive & PBPO witnesses, structured cospans, double categories, decorated composition, Galois connections, polynomial functors, covering families, and the site/path layer. |
-| `Moonlight.Category.Indexed` | The indexed, typed-arrow category-theory layer adapted from `data-category`: indexed categories, functors, natural transformations, adjunctions, (co)limits, Kan extensions, products/coproducts and the simplex category. |
-| `Moonlight.Category.Presentation` | The finite-category authoring surface: named objects, named nonidentity morphisms, strict-order `below` declarations, identities in equations, and compilation to `FinCat`. |
-| `Moonlight.Category.Notation` | Scoped query and composition helpers for already-compiled `FinCat` values. |
-| `Moonlight.Category.Simplicial` | The public simplicial surface: Δ, simplicial sets, nerves, Kan interfaces, homotopy queries, and pure validation. |
+| Module | Cabal component | Surface |
+| --- | --- | --- |
+| `Moonlight.Category` | `moonlight-category` | The broad categorical surface: `Category` and composition, the limit/colimit and higher-category towers, finite and thin categories, invertibility/groupoids, adhesive & PBPO witnesses, structured cospans, double categories, decorated composition, Galois connections, polynomial functors, covering families, and the site/path layer. |
+| `Moonlight.Category.Indexed` | `moonlight-category` | The indexed, typed-arrow category-theory layer adapted from `data-category`: indexed categories, functors, natural transformations, adjunctions, (co)limits, Kan extensions, products/coproducts and the simplex category. |
+| `Moonlight.Category.Presentation` | `moonlight-category` | The finite-category authoring surface: named objects, named nonidentity morphisms, strict-order `below` declarations, identities in equations, and compilation to `FinCat`. |
+| `Moonlight.Category.Notation` | `moonlight-category` | Scoped query and composition helpers for already-compiled `FinCat` values. |
+| `Moonlight.Category.Simplicial` | `moonlight-category:simplicial` | The public simplicial surface: Δ, simplicial sets, nerves, Kan interfaces, homotopy queries, and pure validation. |
 
 The `Moonlight.Category.Pure.*` leaves live in named implementation sublibraries:
 `abstract` for generic category theory, `finite` for `FinCat`/presentation runtime,
@@ -59,6 +59,44 @@
 typed-arrow layer, and `simplicial` for Δ, simplicial sets, nerves and Kan
 interfaces. Effectful law harnesses and cross-package test fixtures live in the
 `laws` sublibrary rather than the pure production components.
+
+### Main-library and simplicial consumers
+
+The simplicial facade is a separate public Cabal component. A program using both
+facades must request both components explicitly:
+
+```cabal
+build-depends:
+    moonlight-category >= 1.1.0.0 && < 1.2,
+    moonlight-category:simplicial >= 1.1.0.0 && < 1.2
+```
+
+```haskell
+import Moonlight.Category
+import Moonlight.Category.Simplicial
+```
+
+Those two facades are the ordinary consumer path. `Moonlight.Category` owns site
+compilation and provenance lookup; `Moonlight.Category.Simplicial` owns nerves and
+their simplicial queries. A consumer should not need a `Pure.*` import to compile a
+site's import category, inspect its nerve, or recover source object names.
+
+### Site provenance and nerves
+
+Use `thinSiteImportKernel` when only the import category is required, then obtain
+its `FinCat` with `thinSiteKernelCodomain`. Use `thinSiteKernel` when full cover
+validation is required. Site-derived `FinObjectId` values are kernel-relative
+representation tokens: their numerical order is not a semantic name or a stable
+persistence contract. Preserve the `ThinSiteKernel` and cross the boundary through
+`thinSiteFinObject` and `thinSiteObjectValue` instead of reconstructing an object
+map from `siteObjects`.
+
+For ordinary topological or combinatorial work, use `normalizedNerve`; it enumerates
+nonidentity chains and closes under faces. `unnormalizedNerve` materializes every
+composable chain, including identity insertions, and is deliberately for small law
+or diagnostic workloads: its truncation bound is not a memory budget. A validated
+`ComposableChain` retains its vertices, so `chainVertices` is a total projection;
+there is no fallible category lookup after construction.
 
 ## Dependency footprint
 
diff --git a/bench/finite/FinCat.hs b/bench/finite/FinCat.hs
--- a/bench/finite/FinCat.hs
+++ b/bench/finite/FinCat.hs
@@ -60,10 +60,12 @@
     mkFinObject,
   )
 import Moonlight.Category.Pure.FiniteComposable
-  ( SizedComposableChain,
+  ( ComposableChain,
+    SizedComposableChain,
     appendComposableMorphism,
     chainDimension,
     chainMorphisms,
+    chainVertices,
     enumerateComposableChains,
     sizedChainDimension,
     sizedChainValue,
@@ -92,7 +94,8 @@
       bgroup
         "prepared FinCat operations"
         (thinOrderCases & fmap preparedFinCatBenchmark),
-      bench "appendComposableMorphism identity x1024" (nf repeatedChainAppendWeight 1024)
+      bench "appendComposableMorphism identity x1024" (nf repeatedChainAppendWeight 1024),
+      chainProjectionBenchmarks
     ]
 type ThinOrderCase :: Type
 data ThinOrderCase = ThinOrderCase
@@ -282,6 +285,52 @@
                   fromIntegral (chainDimension chainValue)
                     + sum (finMorphismWeight <$> chainMorphisms chainValue)
               )
+
+chainProjectionBenchmarks :: Benchmark
+chainProjectionBenchmarks =
+  env (prepareBenchValue (repeatedChainProjectionSetup 1024)) $ \(PreparedComposableChain chainValue) ->
+    bgroup
+      "ComposableChain projections identity x1024"
+      [ bench "chainMorphisms" (nf chainMorphismProjectionWeight chainValue),
+        bench "chainVertices" (nf chainVertexProjectionWeight chainValue)
+      ]
+
+newtype PreparedComposableChain = PreparedComposableChain (ComposableChain FinCat)
+
+instance NFData PreparedComposableChain where
+  rnf (PreparedComposableChain chainValue) =
+    chainMorphismProjectionWeight chainValue `seq`
+      chainVertexProjectionWeight chainValue `seq`
+        ()
+
+repeatedChainProjectionSetup :: Int -> BenchSetup PreparedComposableChain
+repeatedChainProjectionSetup appendCount =
+  BenchSetup
+    (PreparedComposableChain <$> runBenchSetup (repeatedIdentityChain appendCount))
+
+repeatedIdentityChain :: Int -> BenchSetup (ComposableChain FinCat)
+repeatedIdentityChain appendCount =
+  BenchSetup $ do
+    startObject <- first (const "sample FinCat is missing object 0") (mkFinObject sampleFinCat (FinObjectId 0))
+    let identityMorphism = finObjectIdentityMor startObject
+    first
+      (const "the sample identity morphism did not append to its own chain")
+      ( foldM
+          (appendComposableMorphism sampleFinCat)
+          (singletonComposableChain startObject)
+          (replicate appendCount identityMorphism)
+      )
+
+chainMorphismProjectionWeight :: ComposableChain FinCat -> Int
+chainMorphismProjectionWeight chainValue =
+  sum (finMorphismWeight <$> chainMorphisms chainValue)
+
+chainVertexProjectionWeight :: ComposableChain FinCat -> Int
+chainVertexProjectionWeight chainValue =
+  chainVertices chainValue
+    & NonEmpty.toList
+    & fmap (finObjectIdWeight . finObjId)
+    & sum
 
 sourceBucketWeight :: FinCat -> Int
 sourceBucketWeight categoryValue =
diff --git a/bench/simplicial/SimplicialNerve.hs b/bench/simplicial/SimplicialNerve.hs
--- a/bench/simplicial/SimplicialNerve.hs
+++ b/bench/simplicial/SimplicialNerve.hs
@@ -24,13 +24,16 @@
     mkFinCat,
   )
 import Moonlight.Category.Simplicial
-  ( NerveSimplex,
+  ( GeneratedSSet,
+    NerveSimplex,
     TruncatedNormalizedSSet,
-    nerve,
+    generatedSimplicesAtDimension,
     nerveSimplexChain,
     nerveSimplexDimension,
+    normalizedNerve,
     simplicesAtDimension,
     truncationBound,
+    unnormalizedNerve,
   )
 import Numeric.Natural (Natural)
 import SimplicialWeight (naturalWeight)
@@ -45,7 +48,11 @@
 nerveBenchmark :: NerveCase -> Benchmark
 nerveBenchmark nerveCase =
   env (prepareNerveCategory nerveCase) $ \categoryValue ->
-    bench (nerveCaseLabel nerveCase) (nf preparedNerveWeight categoryValue)
+    bgroup
+      (nerveCaseLabel nerveCase)
+      [ bench "normalized nonidentity chains" (nf preparedNormalizedNerveWeight categoryValue),
+        bench "unnormalized identity-complete chains" (nf preparedUnnormalizedNerveWeight categoryValue)
+      ]
 
 data NerveCase = NerveCase
   { nerveCaseObjectCount :: !Int,
@@ -132,17 +139,28 @@
 thinMorphismId sourceKey targetKey =
   FinGeneratorMorphismId (FinGeneratorId (sourceKey * 1024 + targetKey))
 
-nerveWeight :: Natural -> FinCat -> Int
-nerveWeight upperBound categoryValue =
-  nerve categoryValue upperBound
+normalizedNerveWeight :: Natural -> FinCat -> Int
+normalizedNerveWeight upperBound categoryValue =
+  normalizedNerve categoryValue upperBound
     & nerveSSetWeight
 
-preparedNerveWeight :: PreparedNerveCategory -> Int
-preparedNerveWeight prepared =
-  nerveWeight
+preparedNormalizedNerveWeight :: PreparedNerveCategory -> Int
+preparedNormalizedNerveWeight prepared =
+  normalizedNerveWeight
     (preparedNerveTruncationBound prepared)
     (preparedNerveCategory prepared)
 
+unnormalizedNerveWeight :: Natural -> FinCat -> Int
+unnormalizedNerveWeight upperBound categoryValue =
+  unnormalizedNerve categoryValue upperBound
+    & generatedNerveSSetWeight upperBound
+
+preparedUnnormalizedNerveWeight :: PreparedNerveCategory -> Int
+preparedUnnormalizedNerveWeight prepared =
+  unnormalizedNerveWeight
+    (preparedNerveTruncationBound prepared)
+    (preparedNerveCategory prepared)
+
 preparedNerveCategoryWeight :: PreparedNerveCategory -> Int
 preparedNerveCategoryWeight prepared =
   length (allObjects (preparedNerveCategory prepared))
@@ -153,6 +171,12 @@
 nerveSSetWeight simplicialSet =
   [0 .. truncationBound simplicialSet]
     & fmap (nerveSimplicesWeight . simplicesAtDimension simplicialSet)
+    & sum
+
+generatedNerveSSetWeight :: Natural -> GeneratedSSet (NerveSimplex FinCat) -> Int
+generatedNerveSSetWeight upperBound generatedSet =
+  [0 .. upperBound]
+    & fmap (nerveSimplicesWeight . generatedSimplicesAtDimension generatedSet)
     & sum
 
 nerveSimplicesWeight :: [NerveSimplex FinCat] -> Int
diff --git a/bench/site/SiteCases.hs b/bench/site/SiteCases.hs
--- a/bench/site/SiteCases.hs
+++ b/bench/site/SiteCases.hs
@@ -9,13 +9,18 @@
   )
 where
 
+import Data.Bifunctor (first)
 import Data.Function ((&))
 import Data.Map.Strict (Map)
 import Data.Map.Strict qualified as Map
 import Data.Set (Set)
 import Data.Set qualified as Set
 import FinCat (objectKeys)
-import Moonlight.Category.Pure.FinCat (FinObjectId (..))
+import Moonlight.Category.Pure.FinCat (FinObjectId, finObjId)
+import Moonlight.Category.Pure.Site.Compile
+  ( ThinSiteKernel,
+    thinSiteFinObject,
+  )
 import Moonlight.Category.Pure.Site.Core (SiteManifest (..))
 import Moonlight.Category.Pure.Site.Graph (reachableClosure)
 
@@ -57,19 +62,13 @@
     LinearSite objectCount -> (0, objectCount - 1)
     LayeredSite width depth -> (layeredNode width 0 0, layeredNode width depth 0)
 
-siteEndpointObjectIds :: SiteCase -> SiteManifest Int -> Either String (FinObjectId, FinObjectId)
-siteEndpointObjectIds siteCase manifest =
-  case (Map.lookup sourceValue objectIds, Map.lookup targetValue objectIds) of
-    (Just sourceId, Just targetId) -> Right (sourceId, targetId)
-    _ -> Left ("site endpoint missing from manifest: " <> show (sourceValue, targetValue))
+siteEndpointObjectIds :: SiteCase -> ThinSiteKernel validation Int -> Either String (FinObjectId, FinObjectId)
+siteEndpointObjectIds siteCase kernel = do
+  sourceObject <- first show (thinSiteFinObject kernel sourceValue)
+  targetObject <- first show (thinSiteFinObject kernel targetValue)
+  pure (finObjId sourceObject, finObjId targetObject)
   where
     (sourceValue, targetValue) = siteEndpoints siteCase
-    objectIds =
-      siteObjects manifest
-        & Set.toAscList
-        & zip (FinObjectId <$> [0 ..])
-        & fmap (\(objectId, objectValue) -> (objectValue, objectId))
-        & Map.fromList
 
 linearSiteManifest :: Int -> SiteManifest Int
 linearSiteManifest objectCount =
diff --git a/bench/site/SiteManifest.hs b/bench/site/SiteManifest.hs
--- a/bench/site/SiteManifest.hs
+++ b/bench/site/SiteManifest.hs
@@ -40,8 +40,9 @@
   )
 import Moonlight.Category.Pure.Site.Compile
   ( ThinSitePresentation (..),
-    siteImportsAsFinCat,
+    thinSiteImportKernel,
     thinSiteKernel,
+    thinSiteKernelCodomain,
     thinSitePresentation,
   )
 import Moonlight.Category.Pure.Site.Core
@@ -78,10 +79,10 @@
           bench "reachableClosure" (nf reachableClosureWeight (siteImports manifest)),
           bench "importCycles" (nf importCyclesWeight manifest),
           bench "thinSiteKernel + explicit presentation" (nf thinSitePresentationWeight manifest),
-          bench "siteImportsAsFinCat constructor" (nf siteImportsAsFinCatConstructorWeight manifest),
+          bench "thinSiteImportKernel constructor" (nf thinSiteImportKernelConstructorWeight manifest),
           env (prepareBenchValue (preparedSiteFinCatCase siteCase manifest)) $ \prepared ->
             bgroup
-              "prepared siteImportsAsFinCat"
+              "prepared thinSiteImportKernel"
               [ bench "resident endpoint lookup" (nf preparedSiteFinCatEndpointLookupWeight prepared),
                 bench "resident source incident count" (nf preparedSiteFinCatSourceIncidentCountWeight prepared),
                 bench "resident target incident count" (nf preparedSiteFinCatTargetIncidentCountWeight prepared),
@@ -110,8 +111,9 @@
 preparedSiteFinCatCase :: SiteCase -> SiteManifest Int -> BenchSetup PreparedSiteFinCatCase
 preparedSiteFinCatCase siteCase manifest =
   BenchSetup $ do
-    categoryValue <- first show (siteImportsAsFinCat manifest)
-    (sourceId, targetId) <- siteEndpointObjectIds siteCase manifest
+    importKernel <- first show (thinSiteImportKernel manifest)
+    let categoryValue = thinSiteKernelCodomain importKernel
+    (sourceId, targetId) <- siteEndpointObjectIds siteCase importKernel
     pure
       PreparedSiteFinCatCase
         { preparedSiteFinCatCategory = categoryValue,
@@ -203,9 +205,12 @@
             + morphismMapWeight (thinPresentationMorphisms presentation)
             + compositionMapWeight (thinPresentationComposition presentation)
 
-siteImportsAsFinCatConstructorWeight :: SiteManifest Int -> Int
-siteImportsAsFinCatConstructorWeight manifest =
-  either siteFinCatErrorWeight (\categoryValue -> finCatHandle categoryValue `seq` 1) (siteImportsAsFinCat manifest)
+thinSiteImportKernelConstructorWeight :: SiteManifest Int -> Int
+thinSiteImportKernelConstructorWeight manifest =
+  either
+    siteFinCatErrorWeight
+    (\kernel -> finCatHandle (thinSiteKernelCodomain kernel) `seq` 1)
+    (thinSiteImportKernel manifest)
 
 siteViolationWeight :: SiteViolation Int -> Int
 siteViolationWeight =
diff --git a/bench/site/SitePathQuotient.hs b/bench/site/SitePathQuotient.hs
--- a/bench/site/SitePathQuotient.hs
+++ b/bench/site/SitePathQuotient.hs
@@ -16,19 +16,23 @@
     finMorphismWeight,
     finObjectIdWeight,
   )
-import Moonlight.Category.Pure.FinCat (FinObjectId)
+import Moonlight.Category.Pure.FinCat (finObjId)
 import Moonlight.Category.Pure.Site.Category
   ( SitePathCategory,
     SitePathMorphism,
     sitePathCategory,
     sitePathCategoryCodomain,
-    sitePathCategoryObjectIds,
+    sitePathCategoryKernel,
     sitePathManifest,
     sitePathMorphismCodomain,
     sitePathMorphismNodes,
     sitePathMorphismsBetween,
   )
-import Moonlight.Category.Pure.Site.Compile (thinSiteKernel)
+import Moonlight.Category.Pure.Site.Compile
+  ( thinSiteFinObject,
+    thinSiteKernel,
+    thinSiteObjectValue,
+  )
 import Moonlight.Category.Pure.Site.Core (SiteManifest (..))
 import Moonlight.Category.Pure.Site.Quotient
   ( SitePathQuotient,
@@ -36,7 +40,6 @@
     sitePathQuotient,
     sitePathQuotientCodomain,
     sitePathQuotientDomain,
-    sitePathQuotientObjectIds,
   )
 import SiteCases
   ( SiteCase,
@@ -58,7 +61,8 @@
   env (prepareBenchValue (preparedPathSiteCase siteCase)) $ \prepared ->
     bgroup
       (siteCaseLabel siteCase)
-      [ bench "sitePathMorphismsBetween" (nf preparedPathEnumerationWeight prepared),
+      [ bench "site kernel object roundtrip" (nf preparedPathObjectRoundTripWeight prepared),
+        bench "sitePathMorphismsBetween" (nf preparedPathEnumerationWeight prepared),
         bench "sitePathQuotient map morphisms" (nf preparedPathQuotientWeight prepared)
       ]
 
@@ -103,6 +107,10 @@
     & fmap sitePathMorphismWeight
     & sum
 
+preparedPathObjectRoundTripWeight :: PreparedPathSiteCase -> Int
+preparedPathObjectRoundTripWeight prepared =
+  sitePathObjectRoundTripWeight (preparedPathCategory prepared)
+
 preparedPathQuotientWeight :: PreparedPathSiteCase -> Int
 preparedPathQuotientWeight prepared =
   sitePathMorphismsBetween
@@ -130,14 +138,31 @@
 sitePathCategoryDeepWeight categoryValue =
   siteManifestWeight (sitePathManifest categoryValue)
     + finCatWeight (sitePathCategoryCodomain categoryValue)
-    + objectIdMapWeight (sitePathCategoryObjectIds categoryValue)
+    + sitePathObjectRoundTripWeight categoryValue
 
 sitePathQuotientDeepWeight :: SitePathQuotient Int -> Int
 sitePathQuotientDeepWeight quotientValue =
   sitePathCategoryDeepWeight (sitePathQuotientDomain quotientValue)
     + finCatWeight (sitePathQuotientCodomain quotientValue)
-    + objectIdMapWeight (sitePathQuotientObjectIds quotientValue)
 
+sitePathObjectRoundTripWeight :: SitePathCategory Int -> Int
+sitePathObjectRoundTripWeight categoryValue =
+  siteObjects (sitePathManifest categoryValue)
+    & Set.toAscList
+    & fmap (sitePathObjectRoundTripWeightFor categoryValue)
+    & sum
+
+sitePathObjectRoundTripWeightFor :: SitePathCategory Int -> Int -> Int
+sitePathObjectRoundTripWeightFor categoryValue objectValue =
+  case thinSiteFinObject (sitePathCategoryKernel categoryValue) objectValue of
+    Left _ -> 0
+    Right finObject ->
+      finObjectIdWeight (finObjId finObject)
+        + either
+          (const 0)
+          id
+          (thinSiteObjectValue (sitePathCategoryKernel categoryValue) finObject)
+
 siteManifestWeight :: SiteManifest Int -> Int
 siteManifestWeight manifest =
   intSetWeight (siteObjects manifest)
@@ -153,14 +178,6 @@
   Map.foldlWithKey'
     ( \accumulated objectValue coveredValues ->
         accumulated + objectValue + intSetWeight coveredValues
-    )
-    0
-
-objectIdMapWeight :: Map Int FinObjectId -> Int
-objectIdMapWeight =
-  Map.foldlWithKey'
-    ( \accumulated objectValue objectId ->
-        accumulated + objectValue + finObjectIdWeight objectId
     )
     0
 
diff --git a/moonlight-category.cabal b/moonlight-category.cabal
--- a/moonlight-category.cabal
+++ b/moonlight-category.cabal
@@ -1,6 +1,6 @@
 cabal-version:       3.4
 name:                moonlight-category
-version:             1.0.0.0
+version:             1.1.0.0
 homepage:            https://github.com/PaleRoses/moonlight
 bug-reports:         https://github.com/PaleRoses/moonlight/issues
 synopsis:            Categorical layer for Pale Meridian.
@@ -38,7 +38,7 @@
 source-repository this
   type:     git
   location: https://github.com/PaleRoses/moonlight.git
-  tag:      moonlight-category-1.0.0.0
+  tag:      moonlight-category-1.1.0.0
   subdir:   moonlight-category
 
 common shared-properties
@@ -228,7 +228,7 @@
 common category-test-properties
   import: shared-properties
   build-depends:
-    base >= 4.22 && < 5
+    base >= 4.20 && < 5
     , tasty >= 1.4 && < 1.6
 
 common category-abstract-fixture-slice
@@ -253,7 +253,7 @@
     , moonlight-category:abstract
     , moonlight-category:finite
     , moonlight-category:laws
-    , moonlight-pale:test >= 0.1 && < 0.2
+    , moonlight-pale:test >= 0.1.0.2 && < 0.2
     , tasty-hunit >= 0.10 && < 0.11
 
 common category-finite-test-slice
@@ -269,7 +269,7 @@
     , moonlight-category:abstract
     , moonlight-category:finite
     , moonlight-category:laws
-    , moonlight-pale:test >= 0.1 && < 0.2
+    , moonlight-pale:test >= 0.1.0.2 && < 0.2
     , tasty-hunit >= 0.10 && < 0.11
     , tasty-quickcheck >= 0.10 && < 0.12
     , QuickCheck >= 2.14 && < 2.19
@@ -330,10 +330,13 @@
 common category-facade-test-slice
   other-modules:
     FacadeTests
+    FacadeSiteNerveSpec
     NotationSpec
   build-depends:
-    moonlight-category
-    , moonlight-pale:test >= 0.1 && < 0.2
+    containers >= 0.6 && < 0.9
+    , moonlight-category
+    , moonlight-pale:test >= 0.1.0.2 && < 0.2
+    , moonlight-category:simplicial
     , tasty-hunit >= 0.10 && < 0.11
 
 common category-laws-test-slice
@@ -408,7 +411,7 @@
   import: shared-properties
   ghc-options: -O2 -rtsopts
   build-depends:
-    base >= 4.22 && < 5
+    base >= 4.20 && < 5
     , tasty-bench >= 0.3 && < 0.6
 
 common category-benchmark-support-slice
diff --git a/src-abstract/Moonlight/Category/Pure/FiniteComposable.hs b/src-abstract/Moonlight/Category/Pure/FiniteComposable.hs
--- a/src-abstract/Moonlight/Category/Pure/FiniteComposable.hs
+++ b/src-abstract/Moonlight/Category/Pure/FiniteComposable.hs
@@ -7,6 +7,7 @@
 module Moonlight.Category.Pure.FiniteComposable
   ( ComposableChain,
     chainStartObject,
+    chainVertices,
     chainMorphisms,
     ComposableChainError (..),
     SizedComposableChain,
@@ -25,24 +26,25 @@
 
 import Data.Bifunctor (first)
 import Control.Monad (foldM)
-import Data.Foldable (toList)
 import Data.Function ((&))
 import Data.Kind (Constraint, Type)
 import Data.List (genericTake)
+import Data.List.NonEmpty (NonEmpty (..))
 import Data.Maybe (fromMaybe, mapMaybe)
-import Data.Sequence (Seq, (|>))
-import qualified Data.Sequence as Seq
 import Numeric.Natural (Natural)
 import Moonlight.Category.Pure.Category (Category (..))
 
 type ComposableChain :: Type -> Type
--- | A path whose adjacent morphism endpoints have been validated.
+-- | A path whose adjacent morphism endpoints have been validated.  Every stored
+-- step carries the target established while appending it, so vertex projection
+-- is total and never has to query the category again.  The terminal object is
+-- an O(1) view of the newest step; the strict finite step count is an opaque
+-- cache with the same representable domain as the previous sequence-length
+-- view.
 data ComposableChain c = ComposableChain
-  { -- | The path's source object.
-    chainStartObject :: Ob c,
-    -- | The path's current target object.
-    chainTerminalObject :: Ob c,
-    chainMorphismSequence :: Seq (Mor c)
+  { chainStartObjectInternal :: Ob c,
+    chainStepCountInternal :: !Int,
+    chainValidatedStepsNewestFirst :: [(Mor c, Ob c)]
   }
 
 type SizedComposableChain :: Type -> Type
@@ -63,16 +65,44 @@
 
 -- | Count the morphisms in a validated path.
 chainDimension :: ComposableChain c -> Natural
-chainDimension = fromIntegral . Seq.length . chainMorphismSequence
+chainDimension = fromIntegral . chainStepCountInternal
+{-# INLINE chainDimension #-}
 
+-- | The first vertex of a validated path.
+chainStartObject :: ComposableChain c -> Ob c
+chainStartObject = chainStartObjectInternal
+{-# INLINE chainStartObject #-}
+
+-- | The terminal vertex of a validated path.
+chainTerminalObject :: ComposableChain c -> Ob c
+chainTerminalObject chainValue =
+  case chainValidatedStepsNewestFirst chainValue of
+    [] -> chainStartObjectInternal chainValue
+    (_, terminalObject) : _ -> terminalObject
+{-# INLINE chainTerminalObject #-}
+
+-- | The nonempty vertex sequence established by chain construction, in path
+-- order.  Its final vertex is 'chainTerminalObject'.
+chainVertices :: ComposableChain c -> NonEmpty (Ob c)
+chainVertices chainValue =
+  chainStartObjectInternal chainValue
+    :| foldl'
+      (\targets (_, targetObject) -> targetObject : targets)
+      []
+      (chainValidatedStepsNewestFirst chainValue)
+
 -- | Project the morphisms in composition order.
 chainMorphisms :: ComposableChain c -> [Mor c]
-chainMorphisms = toList . chainMorphismSequence
+chainMorphisms chainValue =
+  foldl'
+    (\morphisms (morphism, _) -> morphism : morphisms)
+    []
+    (chainValidatedStepsNewestFirst chainValue)
 
 -- | The dimension-zero path at an object.
 singletonComposableChain :: Ob c -> ComposableChain c
 singletonComposableChain objectValue =
-  ComposableChain objectValue objectValue Seq.empty
+  ComposableChain objectValue 0 []
 
 -- | Validate a morphism sequence from a declared start object.
 mkComposableChain :: (Category c, Eq (Ob c)) => c -> Ob c -> [Mor c] -> Either (ComposableChainError c) (ComposableChain c)
@@ -92,15 +122,16 @@
 appendComposableMorphism categoryValue chainValue morphism = do
   morphismSource <- first ComposableChainCategoryError (source categoryValue morphism)
   morphismTarget <- first ComposableChainCategoryError (target categoryValue morphism)
-  if morphismSource == chainTerminalObject chainValue
+  let terminalObject = chainTerminalObject chainValue
+  if morphismSource == terminalObject
     then
       Right
         ComposableChain
-          { chainStartObject = chainStartObject chainValue,
-            chainTerminalObject = morphismTarget,
-            chainMorphismSequence = chainMorphismSequence chainValue |> morphism
+          { chainStartObjectInternal = chainStartObjectInternal chainValue,
+            chainStepCountInternal = chainStepCountInternal chainValue + 1,
+            chainValidatedStepsNewestFirst = (morphism, morphismTarget) : chainValidatedStepsNewestFirst chainValue
           }
-    else Left (ComposableChainEndpointMismatch (chainTerminalObject chainValue) morphismSource)
+    else Left (ComposableChainEndpointMismatch terminalObject morphismSource)
 
 -- | Enumerate all composable paths at one exact dimension.
 chainsOfDimension :: FiniteComposableCategory c => c -> Natural -> [ComposableChain c]
diff --git a/src-laws/Moonlight/Category/Effect/Harness/Site.hs b/src-laws/Moonlight/Category/Effect/Harness/Site.hs
--- a/src-laws/Moonlight/Category/Effect/Harness/Site.hs
+++ b/src-laws/Moonlight/Category/Effect/Harness/Site.hs
@@ -14,10 +14,13 @@
 import Moonlight.Category.Pure.Site
   ( SiteManifest,
     SiteViolation (..),
-    siteImportsAsFinCat,
     siteImportEdges,
     validateSiteManifest,
   )
+import Moonlight.Category.Pure.Site.Compile
+  ( thinSiteImportKernel,
+    thinSiteKernelCodomain,
+  )
 import Prelude hiding (Functor)
 
 mkSiteLaws :: forall obj layer. Ord obj => SiteLaws obj layer
@@ -43,20 +46,22 @@
 
 siteCategoryIdentityLaw :: forall obj. Ord obj => SiteManifest obj -> Bool
 siteCategoryIdentityLaw manifest =
-  case siteImportsAsFinCat manifest of
+  case thinSiteImportKernel manifest of
     Left _ -> False
-    Right finCategory ->
-      let morphisms = allMorphisms finCategory
+    Right importKernel ->
+      let finCategory = thinSiteKernelCodomain importKernel
+          morphisms = allMorphisms finCategory
           laws = mkCategoryLaws @FinCat finCategory
        in all (categoryLeftIdentity laws) morphisms
             && all (categoryRightIdentity laws) morphisms
 
 siteCategoryAssociativityLaw :: forall obj. Ord obj => SiteManifest obj -> Bool
 siteCategoryAssociativityLaw manifest =
-  case siteImportsAsFinCat manifest of
+  case thinSiteImportKernel manifest of
     Left _ -> False
-    Right finCategory ->
-      let morphisms = allMorphisms finCategory
+    Right importKernel ->
+      let finCategory = thinSiteKernelCodomain importKernel
+          morphisms = allMorphisms finCategory
           laws = mkCategoryLaws @FinCat finCategory
        in [ (firstValue, secondValue, thirdValue)
             | firstValue <- morphisms,
diff --git a/src-laws/Moonlight/Category/Effect/Laws/Site.hs b/src-laws/Moonlight/Category/Effect/Laws/Site.hs
--- a/src-laws/Moonlight/Category/Effect/Laws/Site.hs
+++ b/src-laws/Moonlight/Category/Effect/Laws/Site.hs
@@ -30,7 +30,6 @@
     pathThinCodomainObject,
     quotientPathThinMorphism,
     quotientPathThinObject,
-    siteImportsAsFinCat,
     sitePathCategory,
     sitePathManifest,
     sitePathMorphismsBetween,
@@ -38,6 +37,10 @@
     thinSiteKernel,
     thinSitePresentation,
   )
+import Moonlight.Category.Pure.Site.Compile
+  ( thinSiteImportKernel,
+    thinSiteKernelCodomain,
+  )
 import Moonlight.Pale.Test.Laws.Suite (LawSuite, lawGroup, namedQuickCheckLaw)
 
 sampleSiteManifest :: SiteManifest Int
@@ -98,15 +101,16 @@
 
 thinSiteFinCatGenericAgreementLaw :: Bool
 thinSiteFinCatGenericAgreementLaw =
-  case (siteImportsAsFinCat diamondManifest, thinSiteKernel diamondManifest) of
-    (Right thinDerived, Right kernel) ->
+  case (thinSiteImportKernel diamondManifest, thinSiteKernel diamondManifest) of
+    (Right importKernel, Right kernel) ->
       case thinPresentationToFinCat (thinSitePresentation kernel) of
         Left _ -> False
         Right genericallyChecked ->
-          thinDerived == genericallyChecked
-            && finCatObjects thinDerived == finCatObjects genericallyChecked
-            && finCatExplicitMorphismMapView thinDerived == finCatExplicitMorphismMapView genericallyChecked
-            && finCatExplicitCompositionMapView thinDerived == finCatExplicitCompositionMapView genericallyChecked
+          let thinDerived = thinSiteKernelCodomain importKernel
+           in thinDerived == genericallyChecked
+                && finCatObjects thinDerived == finCatObjects genericallyChecked
+                && finCatExplicitMorphismMapView thinDerived == finCatExplicitMorphismMapView genericallyChecked
+                && finCatExplicitCompositionMapView thinDerived == finCatExplicitCompositionMapView genericallyChecked
     _ -> False
 
 siteQuotientIdentityLaw :: SitePathCategory Int -> Bool
@@ -136,10 +140,11 @@
 
 pathThinCodomainIdentityLaw :: SitePathCategory Int -> Bool
 pathThinCodomainIdentityLaw category =
-  case siteImportsAsFinCat (sitePathManifest category) of
+  case thinSiteImportKernel (sitePathManifest category) of
     Left _ -> False
-    Right finCategory ->
-      let thinCategory = pathThinCat category
+    Right importKernel ->
+      let finCategory = thinSiteKernelCodomain importKernel
+          thinCategory = pathThinCat category
        in all
             ( \sitePathObject ->
                 let objectValue = quotientPathThinObject sitePathObject
@@ -151,10 +156,11 @@
 
 pathThinCodomainCompositionLaw :: SitePathCategory Int -> Bool
 pathThinCodomainCompositionLaw category =
-  case siteImportsAsFinCat (sitePathManifest category) of
+  case thinSiteImportKernel (sitePathManifest category) of
     Left _ -> False
-    Right finCategory ->
-      let thinCategory = pathThinCat category
+    Right importKernel ->
+      let finCategory = thinSiteKernelCodomain importKernel
+          thinCategory = pathThinCat category
        in all
             ( \(leftValue, rightValue) ->
                 case compose thinCategory leftValue rightValue of
diff --git a/src-public/Moonlight/Category.hs b/src-public/Moonlight/Category.hs
--- a/src-public/Moonlight/Category.hs
+++ b/src-public/Moonlight/Category.hs
@@ -19,6 +19,25 @@
 already-compiled finite category, import "Moonlight.Category.Notation".
 
 The indexed, typed-arrow layer is exposed separately as "Moonlight.Category.Indexed".
+
+== Ordinary consumer path
+
+This facade owns ordinary site compilation and finite-category provenance.
+'thinSiteImportKernel' validates and compiles just the import category, while
+'thinSiteKernel' additionally establishes the cover axioms required by the full
+site/path layer. Keep the resulting 'ThinSiteKernel' with its codomain: a
+site-derived 'FinObjectId' is a kernel-relative representation token, /not/ a
+semantic name or a stable numeric ordering. Recover source objects through
+'thinSiteFinObject' and 'thinSiteObjectValue', never by rebuilding an identifier
+map from the manifest's object set.
+
+'ComposableChain' is opaque and validated at construction. Its 'chainVertices'
+projection is therefore total: the established endpoint evidence is retained rather
+than queried again. For a nerve, add the separate
+"Moonlight.Category.Simplicial" component and import its facade. Its
+@normalizedNerve@ is the ordinary nonidentity-chain construction;
+@unnormalizedNerve@ intentionally materializes identity insertions as well and can
+grow combinatorially even for a modest truncation bound.
 -}
 module Moonlight.Category
   ( UnitCat (..),
@@ -45,7 +64,7 @@
 import Moonlight.Category.Pure.PolynomialFunctor as X
 import Moonlight.Category.Pure.Limits as X
 import Moonlight.Category.Pure.StructuredCospan as X
-import Moonlight.Category.Pure.Site as X
+import Moonlight.Category.Pure.Site as X hiding (ThinSitePresentation (..), thinPresentationToFinCat, thinSitePresentation)
 import Moonlight.Category.Pure.Unit
   ( UnitCat (..),
     UnitMor (..),
diff --git a/src-simplicial/Moonlight/Category/Pure/Simplicial/Nerve.hs b/src-simplicial/Moonlight/Category/Pure/Simplicial/Nerve.hs
--- a/src-simplicial/Moonlight/Category/Pure/Simplicial/Nerve.hs
+++ b/src-simplicial/Moonlight/Category/Pure/Simplicial/Nerve.hs
@@ -3,7 +3,10 @@
 {-# LANGUAGE UndecidableInstances #-}
 
 -- | The nerve of a finite composable category: simplices are composable chains,
--- with face and degeneracy structure.
+-- with face and degeneracy structure.  'normalizedNerve' is the ordinary
+-- nonidentity-chain construction.  'unnormalizedNerve' materializes every
+-- composable chain, including identity insertions, and therefore has a
+-- substantially larger cost surface.
 module Moonlight.Category.Pure.Simplicial.Nerve
   ( NerveSimplex,
     nerveSimplexDimension,
@@ -13,12 +16,11 @@
     Nerve,
     nerveCategory,
     unNerve,
-    nerveGenerated,
+    unnormalizedNerve,
     isNerveSimplexDegenerate,
     nerveSimplexFace,
     nerveSimplexDegeneracy,
-    nerveChainVertices,
-    nerve,
+    normalizedNerve,
     nerveInnerKan,
     fillNerveInnerHorn,
     fillNerveInnerHornIndexed,
@@ -30,6 +32,7 @@
 import Data.Function ((&))
 import Data.Kind (Type)
 import Data.List (genericLength, genericSplitAt, unsnoc)
+import Data.List.NonEmpty qualified as NonEmpty
 import Data.Maybe (mapMaybe)
 import Data.Map.Strict qualified as Map
 import GHC.TypeNats (KnownNat, type (+))
@@ -41,6 +44,7 @@
     chainDimension,
     chainMorphisms,
     chainStartObject,
+    chainVertices,
     mkComposableChain,
     sizedChainDimension,
     sizedChainValue,
@@ -102,12 +106,16 @@
   chainMorphisms (nerveSimplexChain simplexValue)
     & any (morphismIsIdentity categoryValue)
 
-nerveGenerated ::
+-- | Materialize the unnormalized nerve through the supplied dimension.  This
+-- includes every identity insertion, so it is intended only for small
+-- diagnostic or law workloads.  The dimension bound is /not/ a resource bound:
+-- the number of composable chains can grow combinatorially before that bound.
+unnormalizedNerve ::
   (FiniteComposableCategory c, Ord (Ob c), Ord (Mor c)) =>
   c ->
   Natural ->
   GeneratedSSet (NerveSimplex c)
-nerveGenerated categoryValue upperBound =
+unnormalizedNerve categoryValue upperBound =
   let levelMap = Map.fromAscListWith (<>) (nerveLevels categoryValue upperBound)
    in trustedGeneratedSSetWithWitness
         upperBound
@@ -116,12 +124,17 @@
         (nerveDegeneracy categoryValue)
         (isNerveSimplexDegenerate categoryValue)
 
-nerve ::
+-- | Construct the normalized nerve through the supplied dimension by
+-- enumerating nonidentity chains and closing them under faces.  This is the
+-- default construction for topological and combinatorial queries.  Its
+-- dimension bound selects simplices; it does not promise a fixed time or memory
+-- budget for an arbitrary finite category.
+normalizedNerve ::
   (FiniteComposableCategory c, Ord (Ob c), Ord (Mor c)) =>
   c ->
   Natural ->
   TruncatedNormalizedSSet (NerveSimplex c)
-nerve categoryValue upperBound =
+normalizedNerve categoryValue upperBound =
   normalizeGeneratedSSet
     ( trustedGeneratedSSetWithWitness
         upperBound
@@ -147,7 +160,7 @@
   c ->
   Natural ->
   Nerve c
-nerveInnerKan categoryValue upperBound = Nerve categoryValue (nerve categoryValue upperBound)
+nerveInnerKan categoryValue upperBound = Nerve categoryValue (normalizedNerve categoryValue upperBound)
 
 nerveLevels :: (FiniteComposableCategory c, Ord (Ob c), Ord (Mor c)) => c -> Natural -> [(Natural, [NerveSimplex c])]
 nerveLevels categoryValue upperBound =
@@ -300,10 +313,6 @@
   degeneracyChainValue <- degeneracyChain categoryValue degeneracyIndex (nerveSimplexChain simplexValue)
   pure (NerveSimplex (currentDimension + 1) degeneracyChainValue)
 
-nerveChainVertices :: Category c => c -> ComposableChain c -> Either (CategoryError c) [Ob c]
-nerveChainVertices categoryValue chainValue =
-  fmap (chainStartObject chainValue :) (traverse (target categoryValue) (chainMorphisms chainValue))
-
 splitAtNatural :: Natural -> [a] -> Maybe ([a], [a])
 splitAtNatural splitIndex values =
   let (prefix, suffix) = genericSplitAt splitIndex values
@@ -321,9 +330,9 @@
   | faceIndex > dimensionValue' = Nothing
   | otherwise = case morphisms of
       [] -> Nothing
-      firstMorphism : restMorphisms
+      _ : restMorphisms
         | faceIndex == 0 -> do
-            startObject <- either (const Nothing) Just (target categoryValue firstMorphism)
+            startObject <- safeIndexNatural 1 (NonEmpty.toList (chainVertices chainValue))
             either (const Nothing) Just (mkComposableChain categoryValue startObject restMorphisms)
         | faceIndex == dimensionValue' -> do
             (prefixMorphisms, _) <- unsnoc morphisms
@@ -353,8 +362,7 @@
    in if degeneracyIndex > dimensionValue'
         then Nothing
         else do
-          vertices <- either (const Nothing) Just (nerveChainVertices categoryValue chainValue)
-          duplicatedObject <- safeIndexNatural degeneracyIndex vertices
+          duplicatedObject <- safeIndexNatural degeneracyIndex (NonEmpty.toList (chainVertices chainValue))
           identityMorphism <- either (const Nothing) Just (identity categoryValue duplicatedObject)
           insertedMorphisms <- insertAt degeneracyIndex identityMorphism (chainMorphisms chainValue)
           either (const Nothing) Just (mkComposableChain categoryValue (chainStartObject chainValue) insertedMorphisms)
diff --git a/src-simplicial/Moonlight/Category/Simplicial.hs b/src-simplicial/Moonlight/Category/Simplicial.hs
--- a/src-simplicial/Moonlight/Category/Simplicial.hs
+++ b/src-simplicial/Moonlight/Category/Simplicial.hs
@@ -4,6 +4,20 @@
 @simplicial@ sublibrary without making downstream consumers name its
 @Pure.Simplicial@ implementation paths.  The effectful property harness remains
 in @moonlight-category:laws@.
+
+== Cabal boundary and nerve cost
+
+This module is provided by the public @moonlight-category:simplicial@ component;
+programs using site compilation and simplicial constructions should depend on that
+component alongside @moonlight-category@ and import this facade alongside
+"Moonlight.Category".  That pair is the complete ordinary consumer path.
+
+'normalizedNerve' is the default: it enumerates nonidentity chains and closes them
+under faces. 'unnormalizedNerve' instead materializes every composable chain,
+including identity insertions, and is intended only for small diagnostic or law
+workloads. Its dimension bound is not a resource bound. Validated chain vertices
+are available totally as 'chainVertices' from "Moonlight.Category"; use the site
+kernel's inverse lookup there to recover domain object names.
 -}
 module Moonlight.Category.Simplicial
   ( module CategoricalSimplex,
diff --git a/src-site/Moonlight/Category/Pure/Site.hs b/src-site/Moonlight/Category/Pure/Site.hs
--- a/src-site/Moonlight/Category/Pure/Site.hs
+++ b/src-site/Moonlight/Category/Pure/Site.hs
@@ -5,7 +5,10 @@
   ( SiteManifest (..),
     SiteViolation (..),
     SiteFinCatError (..),
+    ThinSiteValidation (..),
     ThinSiteKernel,
+    ThinSiteLookupError (..),
+    ThinSiteObjectValueError (..),
     ThinSitePresentation (..),
     SitePathCategory,
     SitePathObject,
@@ -17,7 +20,14 @@
     SitePathQuotientError (..),
     mkSiteManifest,
     validateSiteManifest,
+    thinSiteImportKernel,
     thinSiteKernel,
+    thinSiteKernelManifest,
+    thinSiteKernelCodomain,
+    thinSiteFinObject,
+    thinSiteObjectValue,
+    thinSiteFinMorphism,
+    thinSiteFinMorphismByEndpoints,
     thinSitePresentation,
     thinPresentationToFinCat,
     sitePathCategory,
@@ -35,7 +45,6 @@
     sitePathQuotient,
     quotientMapObject,
     quotientMapMorphism,
-    siteImportsAsFinCat,
     siteImportEdges,
     siteReachable,
   )
@@ -43,11 +52,20 @@
 
 import Moonlight.Category.Pure.Site.Category as X
 import Moonlight.Category.Pure.Site.Compile as X
-  ( ThinSiteKernel,
+  ( ThinSiteValidation (..),
+    ThinSiteKernel,
+    ThinSiteLookupError (..),
+    ThinSiteObjectValueError (..),
     ThinSitePresentation (..),
-    siteImportsAsFinCat,
     thinPresentationToFinCat,
+    thinSiteFinMorphism,
+    thinSiteFinMorphismByEndpoints,
+    thinSiteFinObject,
+    thinSiteImportKernel,
     thinSiteKernel,
+    thinSiteKernelCodomain,
+    thinSiteKernelManifest,
+    thinSiteObjectValue,
     thinSitePresentation,
   )
 import Moonlight.Category.Pure.Site.Core as X
diff --git a/src-site/Moonlight/Category/Pure/Site/Category.hs b/src-site/Moonlight/Category/Pure/Site/Category.hs
--- a/src-site/Moonlight/Category/Pure/Site/Category.hs
+++ b/src-site/Moonlight/Category/Pure/Site/Category.hs
@@ -1,5 +1,7 @@
--- | The path category of a site: objects, morphisms-as-paths, and enumeration of the
--- morphisms between two objects.
+{-# LANGUAGE DataKinds #-}
+
+-- | The path category of a fully validated site: objects, morphisms-as-paths,
+-- and enumeration of the morphisms between two objects.
 module Moonlight.Category.Pure.Site.Category
   ( SitePathCategory,
     SitePathObject,
@@ -7,7 +9,6 @@
     sitePathCategory,
     sitePathCategoryKernel,
     sitePathCategoryCodomain,
-    sitePathCategoryObjectIds,
     sitePathManifest,
     sitePathObjectCategory,
     sitePathObjectValue,
@@ -26,7 +27,6 @@
 import Data.Function ((&))
 import Data.List.NonEmpty (NonEmpty (..))
 import qualified Data.List.NonEmpty as NonEmpty
-import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import Data.Maybe (mapMaybe)
 import qualified Data.Set as Set
@@ -36,24 +36,23 @@
   ( FinCat,
     FinCatError,
     FinMor,
-    FinObjectId,
     FinObj,
   )
 import Moonlight.Core qualified as Aggregate
 import Moonlight.Category.Pure.Site.Compile
   ( ThinSiteKernel,
+    ThinSiteValidation (SiteValidated),
     thinSiteFinMorphism,
     thinSiteFinObject,
     thinSiteKernelCodomain,
     thinSiteKernelManifest,
-    thinSiteKernelObjectIds,
   )
 import Moonlight.Category.Pure.Site.Core (SiteManifest (..))
 import Moonlight.Category.Pure.Site.Graph (siteImportEdges)
 
 type SitePathCategory :: Type -> Type
 newtype SitePathCategory obj = SitePathCategory
-  { sitePathCategoryKernel :: ThinSiteKernel obj
+  { sitePathCategoryKernel :: ThinSiteKernel 'SiteValidated obj
   }
   deriving stock (Eq, Show)
 
@@ -90,14 +89,11 @@
   | SitePathCodomainError FinCatError
   deriving stock (Eq, Show)
 
-sitePathCategory :: ThinSiteKernel obj -> SitePathCategory obj
+sitePathCategory :: ThinSiteKernel 'SiteValidated obj -> SitePathCategory obj
 sitePathCategory = SitePathCategory
 
 sitePathCategoryCodomain :: SitePathCategory obj -> FinCat
 sitePathCategoryCodomain = thinSiteKernelCodomain . sitePathCategoryKernel
-
-sitePathCategoryObjectIds :: SitePathCategory obj -> Map obj FinObjectId
-sitePathCategoryObjectIds = thinSiteKernelObjectIds . sitePathCategoryKernel
 
 sitePathManifest :: SitePathCategory obj -> SiteManifest obj
 sitePathManifest = thinSiteKernelManifest . sitePathCategoryKernel
diff --git a/src-site/Moonlight/Category/Pure/Site/Compile.hs b/src-site/Moonlight/Category/Pure/Site/Compile.hs
--- a/src-site/Moonlight/Category/Pure/Site/Compile.hs
+++ b/src-site/Moonlight/Category/Pure/Site/Compile.hs
@@ -1,19 +1,24 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RoleAnnotations #-}
+
 -- | Compilation of a thin site presentation to a runtime-validated finite category,
--- with object and morphism lookup.
+-- with kernel-relative object and morphism lookup.
 module Moonlight.Category.Pure.Site.Compile
-  ( ThinSitePresentation (..),
+  ( ThinSiteValidation (..),
     ThinSiteKernel,
     thinSiteKernelManifest,
     thinSiteKernelCodomain,
-    thinSiteKernelObjectIds,
     ThinSiteLookupError (..),
+    ThinSiteObjectValueError (..),
+    ThinSitePresentation (..),
     thinSitePresentation,
     thinPresentationToFinCat,
+    thinSiteImportKernel,
     thinSiteKernel,
     thinSiteFinObject,
+    thinSiteObjectValue,
     thinSiteFinMorphism,
     thinSiteFinMorphismByEndpoints,
-    siteImportsAsFinCat,
   )
 where
 
@@ -30,6 +35,7 @@
 import Moonlight.Category.Pure.Category (Category (identity))
 import Moonlight.Category.Pure.FinCat
   ( FinCat,
+    FinCatHandle,
     FinCatError,
     FinCatValidationError,
     FinMor,
@@ -41,12 +47,16 @@
     mkFinObject,
     denseThinEndpointMorphismsFromCategory,
     finCatExplicitCompositionMapView,
+    finCatHandle,
     finCatMorphismIdByEndpoints,
+    finObjCategoryHandle,
+    finObjId,
     trustedDenseThinFinCatFromReachabilityRows,
   )
-import Moonlight.Category.Pure.Site.Core (SiteFinCatError (..), SiteManifest)
+import Moonlight.Category.Pure.Site.Core (SiteFinCatError (..), SiteManifest, SiteViolation)
 import Moonlight.Category.Pure.Site.Manifest
-  ( validateSiteImportManifest,
+  ( ValidatedSiteManifest,
+    validateSiteImportManifest,
     validateSiteManifestDetailed,
     validatedSiteObjectVector,
     validatedSiteReachabilityRows,
@@ -61,11 +71,33 @@
     thinPresentationComposition :: Map (FinMorphismId, FinMorphismId) FinMorphismId
   }
 
-type ThinSiteKernel :: Type -> Type
-data ThinSiteKernel obj = ThinSiteKernel
+-- | The validation obligation discharged before compiling a 'ThinSiteKernel'.
+--
+-- An import kernel validates only the import graph. A site kernel additionally
+-- proves the cover axioms required by path and quotient construction.
+type ThinSiteValidation :: Type
+data ThinSiteValidation
+  = ImportsValidated
+  | SiteValidated
+  deriving stock (Eq, Show)
+
+-- | A finite import category together with the exact manifest-local
+-- correspondence between semantic objects and its opaque finite objects.
+--
+-- 'FinObjectId' values produced here are representation tokens relative to this
+-- kernel, not semantic object names or a stable ordering contract. Use
+-- 'thinSiteFinObject' and 'thinSiteObjectValue' rather than reconstructing the
+-- ascending-set enumeration.
+--
+-- The validation index is nominal: an import-only kernel cannot be coerced into
+-- the full-site evidence required by path and quotient construction.
+type ThinSiteKernel :: ThinSiteValidation -> Type -> Type
+type role ThinSiteKernel nominal nominal
+data ThinSiteKernel validation obj = ThinSiteKernel
   { thinSiteKernelManifest :: SiteManifest obj,
     thinSiteKernelCodomain :: FinCat,
-    thinSiteKernelObjectIds :: Map obj FinObjectId
+    thinSiteKernelObjectIds :: Map obj FinObjectId,
+    thinSiteKernelObjectValues :: Vector.Vector obj
   }
   deriving stock (Eq, Show)
 
@@ -78,15 +110,26 @@
   | ThinSiteCodomainMorphismInvalid FinCatError
   deriving stock (Eq, Show)
 
+-- | Obstructions specific to inverting a finite object through a site kernel.
+--
+-- These are intentionally distinct from 'ThinSiteLookupError': callers that
+-- only construct finite objects or morphisms do not acquire impossible inverse
+-- lookup cases in their error algebra.
+type ThinSiteObjectValueError :: Type
+data ThinSiteObjectValueError
+  = ThinSiteForeignCodomainObject FinCatHandle FinCatHandle FinObjectId
+  | ThinSiteUnmappedCodomainObject FinObjectId
+  deriving stock (Eq, Show)
+
 -- | Builds the explicit presentation, including the materialized composition
 -- table via 'finCatExplicitCompositionMapView' — an output-bound @Θ(n³)@ witness
 -- for a linear site on @n@ objects, dominating the @Θ(n²/w)@ dense validation
 -- that precedes it. The record fields are lazy, so the cubic table is only paid
 -- when 'thinPresentationComposition' is forced. Callers that need composition
--- queries rather than the explicit witness should use 'thinSiteKernel', which
+-- queries rather than the explicit witness should use a 'ThinSiteKernel', which
 -- stays on the dense handle and answers composition in
 -- @O(1)@ without materializing.
-thinSitePresentation :: ThinSiteKernel obj -> ThinSitePresentation obj
+thinSitePresentation :: ThinSiteKernel validation obj -> ThinSitePresentation obj
 thinSitePresentation kernel =
   let objectIds = thinSiteKernelObjectIds kernel
       codomain = thinSiteKernelCodomain kernel
@@ -141,25 +184,49 @@
     (thinPresentationMorphisms presentation)
     (thinPresentationComposition presentation)
 
-thinSiteKernel :: Ord obj => SiteManifest obj -> Either (SiteFinCatError obj) (ThinSiteKernel obj)
-thinSiteKernel manifest =
-  case validateSiteManifestDetailed manifest of
+-- | Compile the import category while deliberately leaving cover validation
+-- outside the obligation. The resulting kernel cannot construct a
+-- 'SitePathCategory' or a 'SitePathQuotient'.
+thinSiteImportKernel :: Ord obj => SiteManifest obj -> Either (SiteFinCatError obj) (ThinSiteKernel 'ImportsValidated obj)
+thinSiteImportKernel =
+  compileThinSiteKernel validateSiteImportManifest
+
+-- | Compile a full site kernel after validating both imports and cover axioms.
+thinSiteKernel :: Ord obj => SiteManifest obj -> Either (SiteFinCatError obj) (ThinSiteKernel 'SiteValidated obj)
+thinSiteKernel =
+  compileThinSiteKernel validateSiteManifestDetailed
+
+compileThinSiteKernel ::
+  Ord obj =>
+  (SiteManifest obj -> Either (NonEmpty (SiteViolation obj)) (ValidatedSiteManifest obj)) ->
+  SiteManifest obj ->
+  Either (SiteFinCatError obj) (ThinSiteKernel validation obj)
+compileThinSiteKernel validateManifest manifest =
+  case validateManifest manifest of
+    Left errors -> Left (SiteManifestInvalid errors)
     Right validatedManifest ->
-      let objectIds = thinSiteObjectIds (Vector.toList (validatedSiteObjectVector validatedManifest))
-          codomain =
-            trustedDenseThinFinCatFromReachabilityRows
-              (thinSiteFinObjectSet objectIds)
-              (validatedSiteReachabilityRows validatedManifest)
-       in Right
-            ThinSiteKernel
-              { thinSiteKernelManifest = manifest,
-                thinSiteKernelCodomain = codomain,
-                thinSiteKernelObjectIds = objectIds
-              }
-    Left errors ->
-      Left (SiteManifestInvalid errors)
+      Right (thinSiteKernelFromValidatedManifest manifest validatedManifest)
 
-thinSiteFinObject :: Ord obj => ThinSiteKernel obj -> obj -> Either (ThinSiteLookupError obj) FinObj
+thinSiteKernelFromValidatedManifest ::
+  Ord obj =>
+  SiteManifest obj ->
+  ValidatedSiteManifest obj ->
+  ThinSiteKernel validation obj
+thinSiteKernelFromValidatedManifest manifest validatedManifest =
+  let objectValues = validatedSiteObjectVector validatedManifest
+      objectIds = thinSiteObjectIds (Vector.toList objectValues)
+      codomain =
+        trustedDenseThinFinCatFromReachabilityRows
+          (thinSiteFinObjectSet objectIds)
+          (validatedSiteReachabilityRows validatedManifest)
+   in ThinSiteKernel
+        { thinSiteKernelManifest = manifest,
+          thinSiteKernelCodomain = codomain,
+          thinSiteKernelObjectIds = objectIds,
+          thinSiteKernelObjectValues = objectValues
+        }
+
+thinSiteFinObject :: Ord obj => ThinSiteKernel validation obj -> obj -> Either (ThinSiteLookupError obj) FinObj
 thinSiteFinObject kernel objectValue =
   case Map.lookup objectValue (thinSiteKernelObjectIds kernel) of
     Nothing ->
@@ -171,7 +238,30 @@
         Right finObject ->
           Right finObject
 
-thinSiteFinMorphism :: Ord obj => ThinSiteKernel obj -> NonEmpty obj -> Either (ThinSiteLookupError obj) FinMor
+-- | Recover the semantic manifest object for an object from this kernel's
+-- codomain. The category-handle check rejects objects from a different finite
+-- category; a correctly handled object without an entry is reported as an
+-- explicit unmapped-codomain obstruction rather than silently reusing its
+-- numeric identifier.
+thinSiteObjectValue :: ThinSiteKernel validation obj -> FinObj -> Either ThinSiteObjectValueError obj
+thinSiteObjectValue kernel finObject
+  | finObjCategoryHandle finObject /= expectedHandle =
+      Left
+        ( ThinSiteForeignCodomainObject
+            expectedHandle
+            (finObjCategoryHandle finObject)
+            (finObjId finObject)
+        )
+  | otherwise =
+      case finObjId finObject of
+        objectId@(FinObjectId objectIndex) ->
+          case thinSiteKernelObjectValues kernel Vector.!? objectIndex of
+            Nothing -> Left (ThinSiteUnmappedCodomainObject objectId)
+            Just objectValue -> Right objectValue
+  where
+    expectedHandle = finCatHandle (thinSiteKernelCodomain kernel)
+
+thinSiteFinMorphism :: Ord obj => ThinSiteKernel validation obj -> NonEmpty obj -> Either (ThinSiteLookupError obj) FinMor
 thinSiteFinMorphism kernel nodes =
   thinSiteFinMorphismByEndpoints
     kernel
@@ -180,7 +270,7 @@
 
 thinSiteFinMorphismByEndpoints ::
   Ord obj =>
-  ThinSiteKernel obj ->
+  ThinSiteKernel validation obj ->
   obj ->
   obj ->
   Either (ThinSiteLookupError obj) FinMor
@@ -200,23 +290,8 @@
             Right finMorphism ->
               Right finMorphism
 
-thinSiteMorphismIdByEndpoints :: Ord obj => ThinSiteKernel obj -> obj -> obj -> Maybe FinMorphismId
+thinSiteMorphismIdByEndpoints :: Ord obj => ThinSiteKernel validation obj -> obj -> obj -> Maybe FinMorphismId
 thinSiteMorphismIdByEndpoints kernel sourceValue targetValue = do
   sourceId <- Map.lookup sourceValue (thinSiteKernelObjectIds kernel)
   targetId <- Map.lookup targetValue (thinSiteKernelObjectIds kernel)
   finCatMorphismIdByEndpoints (thinSiteKernelCodomain kernel) sourceId targetId
-
--- | Compile only the import category. Cover axioms are deliberately outside this
--- boundary; use 'thinSiteKernel' when a validated site is required.
-siteImportsAsFinCat :: Ord obj => SiteManifest obj -> Either (SiteFinCatError obj) FinCat
-siteImportsAsFinCat manifest =
-  case validateSiteImportManifest manifest of
-    Right validatedManifest ->
-      let objectIds = thinSiteObjectIds (Vector.toList (validatedSiteObjectVector validatedManifest))
-       in Right
-            ( trustedDenseThinFinCatFromReachabilityRows
-                (thinSiteFinObjectSet objectIds)
-                (validatedSiteReachabilityRows validatedManifest)
-            )
-    Left errors ->
-      Left (SiteManifestInvalid errors)
diff --git a/src-site/Moonlight/Category/Pure/Site/Quotient.hs b/src-site/Moonlight/Category/Pure/Site/Quotient.hs
--- a/src-site/Moonlight/Category/Pure/Site/Quotient.hs
+++ b/src-site/Moonlight/Category/Pure/Site/Quotient.hs
@@ -1,5 +1,7 @@
--- | The path-thin quotient of a site path category: quotient objects and morphisms,
--- and the quotient maps from the path category.
+{-# LANGUAGE DataKinds #-}
+
+-- | The path-thin quotient of a fully validated site path category: quotient
+-- objects and morphisms, and the quotient maps from the path category.
 module Moonlight.Category.Pure.Site.Quotient
   ( PathThinCat (..),
     PathThinObject (..),
@@ -7,7 +9,6 @@
     SitePathQuotient,
     sitePathQuotientDomain,
     sitePathQuotientCodomain,
-    sitePathQuotientObjectIds,
     SitePathQuotientError (..),
     pathThinCat,
     mkPathThinObject,
@@ -25,7 +26,6 @@
 import Data.Kind (Type)
 import Data.Bifunctor (first)
 import qualified Data.List.NonEmpty as NonEmpty
-import Data.Map.Strict (Map)
 import Moonlight.Category.Pure.Category (Category (..))
 import Moonlight.Category.Pure.FinCat
   ( FinCat,
@@ -41,7 +41,6 @@
     mkSitePathObject,
     sitePathCategoryCodomain,
     sitePathCategoryKernel,
-    sitePathCategoryObjectIds,
     sitePathManifest,
     sitePathMorphismCategory,
     sitePathMorphismCodomain,
@@ -52,6 +51,7 @@
   )
 import Moonlight.Category.Pure.Site.Compile
   ( ThinSiteKernel,
+    ThinSiteValidation (SiteValidated),
     ThinSiteLookupError (..),
     thinSiteFinMorphismByEndpoints,
     thinSiteFinObject,
@@ -116,9 +116,6 @@
 sitePathQuotientCodomain :: SitePathQuotient obj -> FinCat
 sitePathQuotientCodomain = sitePathCategoryCodomain . sitePathQuotientDomain
 
-sitePathQuotientObjectIds :: SitePathQuotient obj -> Map obj FinObjectId
-sitePathQuotientObjectIds = sitePathCategoryObjectIds . sitePathQuotientDomain
-
 type SitePathQuotientError :: Type -> Type
 data SitePathQuotientError obj
   = QuotientUnknownObject obj
@@ -298,7 +295,7 @@
               pathThinObjectCodomain = codomainObject
             }
 
-sitePathQuotientKernel :: SitePathQuotient obj -> ThinSiteKernel obj
+sitePathQuotientKernel :: SitePathQuotient obj -> ThinSiteKernel 'SiteValidated obj
 sitePathQuotientKernel = sitePathCategoryKernel . sitePathQuotientDomain
 
 fromThinSiteLookupError :: ThinSiteLookupError obj -> SitePathQuotientError obj
diff --git a/test/abstract/FiniteComposableSpec.hs b/test/abstract/FiniteComposableSpec.hs
--- a/test/abstract/FiniteComposableSpec.hs
+++ b/test/abstract/FiniteComposableSpec.hs
@@ -3,6 +3,7 @@
   )
 where
 
+import Data.List.NonEmpty qualified as NonEmpty
 import Moonlight.Category.Pure.Category (Category (..))
 import Moonlight.Category.Effect.Fixture.FinCat (sampleFinCat)
 import Moonlight.Category.Pure.FinCat
@@ -16,7 +17,9 @@
     chainDimension,
     chainMorphisms,
     chainTerminalObject,
+    chainVertices,
     mkComposableChain,
+    singletonComposableChain,
   )
 import Moonlight.Pale.Test.Assertions (expectRightWithLabel, expectSome)
 import Test.Tasty (TestTree, testGroup)
@@ -26,7 +29,7 @@
 tests =
   testGroup
     "FiniteComposable"
-    [ testCase "checked chains cache their terminal without changing their morphisms" testCheckedChain,
+    [ testCase "checked chains retain a total vertex sequence" testCheckedChain,
       testCase "Natural dimension bounds do not overflow through Int" testNaturalDimensionBound,
       testCase "identity construction requires a validated object" testCheckedIdentity
     ]
@@ -34,6 +37,7 @@
 testCheckedChain :: Assertion
 testCheckedChain = do
   object0 <- expectRightWithLabel "object 0" (mkFinObject sampleFinCat (FinObjectId 0))
+  object1 <- expectRightWithLabel "object 1" (mkFinObject sampleFinCat (FinObjectId 1))
   object2 <- expectRightWithLabel "object 2" (mkFinObject sampleFinCat (FinObjectId 2))
   morphism01 <- expectSome "morphism 0 -> 1" (finCatHomMorphism sampleFinCat (FinObjectId 0) (FinObjectId 1))
   morphism12 <- expectSome "morphism 1 -> 2" (finCatHomMorphism sampleFinCat (FinObjectId 1) (FinObjectId 2))
@@ -43,6 +47,10 @@
       chainDimension chainValue @?= 2
       chainTerminalObject chainValue @?= object2
       chainMorphisms chainValue @?= [morphism01, morphism12]
+      chainVertices chainValue @?= object0 NonEmpty.:| [object1, object2]
+      NonEmpty.last (chainVertices chainValue) @?= chainTerminalObject chainValue
+      NonEmpty.length (chainVertices chainValue) @?= 3
+      chainVertices (singletonComposableChain object0) @?= object0 NonEmpty.:| []
 
 testNaturalDimensionBound :: Assertion
 testNaturalDimensionBound =
diff --git a/test/facade/FacadeSiteNerveSpec.hs b/test/facade/FacadeSiteNerveSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/facade/FacadeSiteNerveSpec.hs
@@ -0,0 +1,70 @@
+module FacadeSiteNerveSpec
+  ( tests,
+  )
+where
+
+import Data.List.NonEmpty (NonEmpty (..))
+import qualified Data.Map.Strict as Map
+import qualified Data.Set as Set
+import Moonlight.Category
+  ( SiteManifest (..),
+    chainVertices,
+    thinSiteImportKernel,
+    thinSiteKernelCodomain,
+    thinSiteObjectValue,
+  )
+import Moonlight.Category.Simplicial
+  ( nerveSimplexChain,
+    normalizedNerve,
+    simplicesAtDimension,
+  )
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.HUnit (Assertion, assertFailure, testCase, (@?=))
+
+tests :: TestTree
+tests =
+  testGroup
+    "main and simplicial facades"
+    [ testCase
+        "site imports compile, normalize, and recover names without Pure imports"
+        testFacadeOnlySiteNerve
+    ]
+
+testFacadeOnlySiteNerve :: Assertion
+testFacadeOnlySiteNerve =
+  case thinSiteImportKernel threeModuleManifest of
+    Left siteError ->
+      assertFailure ("import kernel rejected a valid module manifest: " <> show siteError)
+    Right kernel -> do
+      let normalized = normalizedNerve (thinSiteKernelCodomain kernel) 2
+          fVector = length . simplicesAtDimension normalized <$> [0, 1, 2]
+      fVector @?= [3, 3, 1]
+      case simplicesAtDimension normalized 2 of
+        [topSimplex] ->
+          traverse
+            (thinSiteObjectValue kernel)
+            (chainVertices (nerveSimplexChain topSimplex))
+            @?= Right ("app" :| ["api", "core"])
+        topSimplices ->
+          assertFailure
+            ( "expected exactly one normalized 2-simplex, found "
+                <> show (length topSimplices)
+            )
+
+threeModuleManifest :: SiteManifest String
+threeModuleManifest =
+  SiteManifest
+    { siteObjects = Set.fromList ["app", "api", "core"],
+      siteImports =
+        Map.fromList
+          [ ("app", Set.singleton "api"),
+            ("api", Set.singleton "core"),
+            ("core", Set.empty)
+          ],
+      siteCovers =
+        Map.fromList
+          [ ("app", Set.fromList ["api", "core"]),
+            ("api", Set.singleton "core"),
+            ("core", Set.empty)
+          ]
+    }
diff --git a/test/facade/FacadeTests.hs b/test/facade/FacadeTests.hs
--- a/test/facade/FacadeTests.hs
+++ b/test/facade/FacadeTests.hs
@@ -4,10 +4,13 @@
 where
 
 import qualified NotationSpec
+import qualified FacadeSiteNerveSpec
 import Test.Tasty (TestTree, testGroup)
 
 tests :: TestTree
 tests =
   testGroup
     "facade"
-    [NotationSpec.tests]
+    [ NotationSpec.tests,
+      FacadeSiteNerveSpec.tests
+    ]
diff --git a/test/simplicial/NerveSpec.hs b/test/simplicial/NerveSpec.hs
--- a/test/simplicial/NerveSpec.hs
+++ b/test/simplicial/NerveSpec.hs
@@ -33,12 +33,13 @@
     generatedSimplicesAtDimension,
     mkHorn,
     mkInnerHorn,
-    nerve,
-    nerveGenerated,
     nerveSimplexChain,
     nerveSimplexDimension,
     nerveSimplexFromChain,
+    normalizeGeneratedSSet,
+    normalizedNerve,
     simplicesAtDimension,
+    unnormalizedNerve,
   )
 import Laws.Suite (LawSuiteConfig (..), mkLawfulCarrierSpec)
 import Moonlight.Pale.Test.Laws.Suite (LawSuite)
@@ -154,7 +155,7 @@
 
 innerHornFillMatchesSimplex :: GeneratedFiniteCategory -> Bool
 innerHornFillMatchesSimplex generatedValue =
-  let simplicialSet = nerve (generatedCategory generatedValue) (generatedTruncation generatedValue)
+  let simplicialSet = normalizedNerve (generatedCategory generatedValue) (generatedTruncation generatedValue)
    in and
         [ case mkHorn nerveSimplexDimension (applyFaceAtDimension simplicialSet) simplexDimension missingFace faceEntries of
             Left _ -> False
@@ -180,11 +181,11 @@
 lawfulCarrierSpec :: LawSuite
 lawfulCarrierSpec =
   mkLawfulCarrierSpec
-    "nerve"
+    "normalized nerve"
     LawSuiteConfig
-      { lawSuiteName = "nerve simplicial laws",
+      { lawSuiteName = "normalized nerve simplicial laws",
         lawSuiteMaxSuccess = 300,
-        lawSuiteCarrierToSSet = \generatedValue -> nerve (generatedCategory generatedValue) (generatedTruncation generatedValue),
+        lawSuiteCarrierToSSet = \generatedValue -> normalizedNerve (generatedCategory generatedValue) (generatedTruncation generatedValue),
         lawSuiteEquality = sameSimplex,
         lawSuiteRenderSimplex = show . simplexFingerprint
       }
@@ -193,20 +194,31 @@
 carrierTests =
   testGroup
     "Nerve"
-    [ testCase "generated and normalized carriers separate degenerate simplices" $ do
-        let generatedSet = nerveGenerated sampleFinCat 1
-            simplicialSet = nerve sampleFinCat 1
-        assertEqual "generated 0-simplices" 3 (length (generatedSimplicesAtDimension generatedSet 0))
-        assertEqual "generated 1-simplices" 6 (length (generatedSimplicesAtDimension generatedSet 1))
+    [ testCase "unnormalized and normalized carriers separate degenerate simplices" $ do
+        let generatedSet = unnormalizedNerve sampleFinCat 1
+            simplicialSet = normalizedNerve sampleFinCat 1
+        assertEqual "unnormalized 0-simplices" 3 (length (generatedSimplicesAtDimension generatedSet 0))
+        assertEqual "unnormalized 1-simplices" 6 (length (generatedSimplicesAtDimension generatedSet 1))
         assertEqual "normalized 0-simplices" 3 (length (simplicesAtDimension simplicialSet 0))
         assertEqual "normalized 1-simplices" 3 (length (simplicesAtDimension simplicialSet 1)),
+      testCase "normalizing the unnormalized nerve agrees with the normalized nerve" $ do
+        let normalizedSet = normalizedNerve sampleFinCat 2
+            normalizedFromUnnormalized = normalizeGeneratedSSet (unnormalizedNerve sampleFinCat 2)
+            fingerprintRows simplicialSet =
+              fmap
+                (Set.fromList . fmap simplexFingerprint . simplicesAtDimension simplicialSet)
+                [0 .. 2]
+        assertEqual
+          "normalized simplex rows"
+          (fingerprintRows normalizedSet)
+          (fingerprintRows normalizedFromUnnormalized),
       testCase "inner horn filler reconstructs a composable 2-simplex" $ do
         let oneChains = chainsOfDimension sampleFinCat 1
             maybeFirst = lookupSingleMorphismChain (generatorMorphismId 10) oneChains
             maybeSecond = lookupSingleMorphismChain (generatorMorphismId 11) oneChains
         case (maybeFirst, maybeSecond) of
           (Just firstChain, Just secondChain) ->
-            let simplicialSet = nerve sampleFinCat 2
+            let simplicialSet = normalizedNerve sampleFinCat 2
                 hornEntries = [(2, nerveSimplexFromChain firstChain), (0, nerveSimplexFromChain secondChain)]
              in case mkHorn nerveSimplexDimension (applyFaceAtDimension simplicialSet) 2 1 hornEntries of
                   Left _ -> assertBool "expected a compatible inner horn" False
@@ -220,6 +232,6 @@
                             assertEqual "filled simplex dimension" 2 (nerveSimplexDimension simplexValue)
                             assertEqual "filled simplex chain length" 2 (length (chainMorphisms (nerveSimplexChain simplexValue)))
           _ -> assertBool "expected generator chains in dimension 1" False,
-      QC.testProperty "inner horns reconstruct original simplex in generated nerves" $
+      QC.testProperty "inner horns reconstruct original simplex in normalized nerves" $
         QC.withNumTests 200 innerHornFillMatchesSimplex
     ]
diff --git a/test/site/SiteSpec.hs b/test/site/SiteSpec.hs
--- a/test/site/SiteSpec.hs
+++ b/test/site/SiteSpec.hs
@@ -9,7 +9,15 @@
 import qualified Data.Map.Strict as Map
 import Data.Set (Set)
 import qualified Data.Set as Set
-import Moonlight.Category.Pure.Site.Compile (thinSiteKernel)
+import Moonlight.Category (allObjects)
+import Moonlight.Category.Pure.Site.Compile
+  ( ThinSiteObjectValueError (..),
+    thinSiteFinObject,
+    thinSiteImportKernel,
+    thinSiteKernel,
+    thinSiteKernelCodomain,
+    thinSiteObjectValue,
+  )
 import Moonlight.Category.Pure.Site.Core (SiteFinCatError (..), SiteManifest (..), SiteViolation (..))
 import Moonlight.Category.Pure.Site.Graph (importCycles, reachableClosure)
 import Moonlight.Category.Pure.Site.Manifest (validateSiteManifest)
@@ -39,6 +47,18 @@
         "manifest validation and kernel compilation share diagnostics"
         testManifestValidationAndKernelDiagnosticsAgree,
       testCase
+        "site kernel round-trips every semantic and codomain object"
+        testThinSiteKernelObjectRoundTrips,
+      testCase
+        "site kernel rejects a finite object from a foreign codomain"
+        testThinSiteKernelRejectsForeignCodomainObject,
+      testCase
+        "import kernel accepts import-valid cover-invalid manifests while the full kernel rejects them"
+        testThinSiteImportKernelSeparatesCoverValidation,
+      testCase
+        "import and full kernels agree for a valid manifest"
+        testThinSiteKernelsAgreeOnValidManifest,
+      testCase
         "validateSiteManifest reports cover sets that are not closed under covered covers"
         testValidateSiteManifestReportsCoverClosureViolation
     ]
@@ -111,6 +131,71 @@
       NonEmpty.toList violations @?= validateSiteManifest invalidCoverManifest
     Right _ -> assertFailure "invalid cover produced a validated site kernel"
 
+testThinSiteKernelObjectRoundTrips :: Assertion
+testThinSiteKernelObjectRoundTrips =
+  case thinSiteKernel roundTripManifest of
+    Left siteError ->
+      assertFailure ("round-trip manifest failed to compile: " <> show siteError)
+    Right kernel -> do
+      let manifestObjects = Set.toAscList (siteObjects roundTripManifest)
+          codomainObjects = allObjects (thinSiteKernelCodomain kernel)
+      case traverse (thinSiteFinObject kernel) manifestObjects of
+        Left lookupError ->
+          assertFailure ("semantic object failed to compile: " <> show lookupError)
+        Right finObjects ->
+          case traverse (thinSiteObjectValue kernel) finObjects of
+            Left objectValueError ->
+              assertFailure ("compiled object failed to recover: " <> show objectValueError)
+            Right recoveredObjects ->
+              recoveredObjects @?= manifestObjects
+      case traverse (thinSiteObjectValue kernel) codomainObjects of
+        Left lookupError ->
+          assertFailure ("codomain object failed to recover: " <> show lookupError)
+        Right recoveredObjects ->
+          Set.fromList recoveredObjects @?= siteObjects roundTripManifest
+
+testThinSiteKernelRejectsForeignCodomainObject :: Assertion
+testThinSiteKernelRejectsForeignCodomainObject =
+  case (thinSiteKernel roundTripManifest, thinSiteKernel foreignCodomainManifest) of
+    (Right kernel, Right foreignKernel) ->
+      case thinSiteFinObject foreignKernel 0 of
+        Left lookupError ->
+          assertFailure ("foreign kernel did not produce its declared object: " <> show lookupError)
+        Right foreignObject ->
+          case thinSiteObjectValue kernel foreignObject of
+            Left (ThinSiteForeignCodomainObject _ _ _) -> pure ()
+            otherResult ->
+              assertFailure ("foreign codomain object was not rejected: " <> show otherResult)
+    (leftResult, rightResult) ->
+      assertFailure
+        ( "foreign-codomain fixtures failed to compile: "
+            <> show (leftResult, rightResult)
+        )
+
+testThinSiteImportKernelSeparatesCoverValidation :: Assertion
+testThinSiteImportKernelSeparatesCoverValidation =
+  case (thinSiteImportKernel invalidCoverManifest, thinSiteKernel invalidCoverManifest) of
+    (Right _, Left (SiteManifestInvalid _)) -> pure ()
+    outcomes ->
+      assertFailure ("import and full kernels did not separate cover validation: " <> show outcomes)
+
+testThinSiteKernelsAgreeOnValidManifest :: Assertion
+testThinSiteKernelsAgreeOnValidManifest =
+  case (thinSiteImportKernel roundTripManifest, thinSiteKernel roundTripManifest) of
+    (Right importKernel, Right fullKernel) -> do
+      thinSiteKernelCodomain importKernel @?= thinSiteKernelCodomain fullKernel
+      let manifestObjects = Set.toAscList (siteObjects roundTripManifest)
+      case
+          ( traverse (thinSiteFinObject importKernel) manifestObjects,
+            traverse (thinSiteFinObject fullKernel) manifestObjects
+          ) of
+        (Right importObjects, Right fullObjects) ->
+          importObjects @?= fullObjects
+        outcomes ->
+          assertFailure ("valid kernels disagreed about a manifest object: " <> show outcomes)
+    outcomes ->
+      assertFailure ("valid manifest failed to compile under one kernel scope: " <> show outcomes)
+
 declaredCycleManifest :: SiteManifest String
 declaredCycleManifest =
   let objects = set ["domain", "service"]
@@ -130,6 +215,42 @@
     { siteObjects = Set.singleton 0,
       siteImports = Map.singleton 0 Set.empty,
       siteCovers = Map.singleton 0 (Set.singleton 1)
+    }
+
+roundTripManifest :: SiteManifest Int
+roundTripManifest =
+  SiteManifest
+    { siteObjects = set [0, 1, 2],
+      siteImports =
+        Map.fromList
+          [ (0, set [1]),
+            (1, set [2]),
+            (2, Set.empty)
+          ],
+      siteCovers =
+        Map.fromList
+          [ (0, set [1, 2]),
+            (1, set [2]),
+            (2, Set.empty)
+          ]
+    }
+
+foreignCodomainManifest :: SiteManifest Int
+foreignCodomainManifest =
+  SiteManifest
+    { siteObjects = set [0, 1, 2],
+      siteImports =
+        Map.fromList
+          [ (0, set [1]),
+            (1, Set.empty),
+            (2, Set.empty)
+          ],
+      siteCovers =
+        Map.fromList
+          [ (0, set [1]),
+            (1, Set.empty),
+            (2, Set.empty)
+          ]
     }
 
 testValidateSiteManifestReportsCoverClosureViolation :: Assertion