diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -243,7 +243,7 @@
   { }
   { }
 ...
-\phinoMorphingRule{root}
+\phinoMorphingRule{universe}
   { \mathbb{M}( Q, e ) }
   { \mathbb{M}( \phinoNormalize{ e }, e ) }
   { $ e \not= Q $ }
diff --git a/phino.cabal b/phino.cabal
--- a/phino.cabal
+++ b/phino.cabal
@@ -1,6 +1,6 @@
 cabal-version: 3.0
 name: phino
-version: 0.0.96
+version: 0.0.97
 license: MIT
 synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions
 description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
diff --git a/resources/dataization.yaml b/resources/dataization.yaml
--- a/resources/dataization.yaml
+++ b/resources/dataization.yaml
@@ -22,9 +22,11 @@
 # 'norm' matches the bare meta 𝑛, which unifies with any expression, so it is
 # guarded to fire only when 𝑛 is neither a formation ('not (formation 𝑛)',
 # carving out 'delta', 'box', 'fire' and 'none') nor the termination ⊥
-# ('not (𝑛 = ⊥)', carving out 'end'). Without the guard 'norm' would behave
-# correctly only by being declared last; with it the clauses no longer rely on
-# their order.
+# ('not (𝑛 = ⊥)'). 𝔻 is partial: ⊥ (the terminator T) signals an error and
+# lies outside its domain, so it deliberately matches no clause and dataization
+# stops there — there is no 'end' rule mapping ⊥ to empty bytes (see #955).
+# Without the guard 'norm' would behave correctly only by being declared last;
+# with it the clauses no longer rely on their order.
 
 - name: delta
   label: \Delta
@@ -75,11 +77,6 @@
   premises:
     - d-result: δ
       dataize: ⊥
-
-- name: end
-  match: ⊥
-  e-match: 𝑒
-  d-result: '--'
 
 - name: norm
   match: 𝑛
diff --git a/resources/morphing.yaml b/resources/morphing.yaml
--- a/resources/morphing.yaml
+++ b/resources/morphing.yaml
@@ -4,7 +4,7 @@
 # Morphing 𝕄 — applied top-to-bottom, first matching clause wins. It is ternary,
 # 𝕄(n, e, s): n is the morphed term, e is the fixed global universe and s is
 # the mutable state. The universe is threaded unchanged through every recursive
-# call and substituted for Φ by the 'root' rule (Φ, rendered Q, is just the
+# call and substituted for Φ by the 'universe' rule (Φ, rendered Q, is just the
 # locator of e); the state is threaded too and the new state returned. Only the
 # 'ml' rule changes it, by firing an atom through 𝔼. The first argument is
 # always a normal form: a non-NF expression matches no clause. 𝕄 navigates a
@@ -87,7 +87,8 @@
     - n-result: 𝑛3
       morph: 𝑛2
 
-- name: root
+- name: universe
+  label: \Phi
   match: Φ
   e-match: 𝑒
   n-result: 𝑛1
diff --git a/src/Dataize.hs b/src/Dataize.hs
--- a/src/Dataize.hs
+++ b/src/Dataize.hs
@@ -83,7 +83,7 @@
 -- 𝕄(n, e, s): besides the term 'n' it takes the universe 'e' ('univ') — a plain
 -- expression — and the mutable state 's', returning the morphed term together
 -- with the new state. The universe is matched against the rule's 'e-match'
--- pattern (usually the '𝑒' meta, which binds 'e' so the 'root' rule substitutes
+-- pattern (usually the '𝑒' meta, which binds 'e' so the 'universe' rule substitutes
 -- it, but a rule may pin it to a literal such as 'mg' matching Φ). Its rules
 -- come from 'morphing.yaml': the first matching rule's premises are evaluated and
 -- its conclusion 'nresult' is built, always forwarding the same universe. The
@@ -157,12 +157,15 @@
   ((bytes, seq), _state) <- dataize' (expr, (program, Nothing) :| []) univ emptyState ctx
   pure (bytes, reverse seq)
 
--- The Dataization function 𝔻 retrieves bytes from an expression. It is total and
--- ternary, 𝔻(n, e, s): besides the term 'n' it takes the universe 'e' ('univ'),
+-- The Dataization function 𝔻 retrieves bytes from an expression. It is partial
+-- and ternary, 𝔻(n, e, s): besides the term 'n' it takes the universe 'e' ('univ'),
 -- which it forwards to 𝕄, and the mutable state 's', returning the bytes together
 -- with the new state. Its rules come from 'dataization.yaml': 'delta' yields the
--- asset bytes, 'end' (⊥) yields empty bytes (--) and 'none' (a formation with no
--- Δ/λ/φ) delegates to 'end' by dataizing ⊥,
+-- asset bytes and 'none' (a formation with no Δ/λ/φ) has nothing to dataize, so
+-- it dataizes ⊥. The terminator ⊥ signals an error and lies outside 𝔻's domain,
+-- so it matches no clause (there is no 'end' rule mapping it to empty bytes) and
+-- dataization stops there; a data-less formation therefore fails through the
+-- same path (see #955).
 -- 'box' contextualizes the φ-body and keeps dataizing (its step is labelled by
 -- its 'contextualize' side-computation), and 'norm' reduces through morphing,
 -- splicing the morphing steps into the chain. The clauses are disjoint (see
@@ -181,8 +184,15 @@
   matched <- firstMatch rules
   case matched of
     Just (rule, subst) -> reduce rule subst
-    Nothing -> throwIO (userError "no dataization rule matched")
+    Nothing -> throwIO (userError (unmatched expr))
   where
+    -- 𝔻 is partial: the terminator ⊥ signals an error and lies outside its
+    -- domain (see #955), so it matches no clause and lands here. Name it in the
+    -- message rather than reporting the generic "no dataization rule matched",
+    -- which would otherwise hide that the computation reached a dead end.
+    unmatched :: Expression -> String
+    unmatched ExTermination = "dataization reached the terminator ⊥, which signals an error and cannot be dataized"
+    unmatched _ = "no dataization rule matched"
     firstMatch :: [Y.DataizeRule] -> IO (Maybe (Y.DataizeRule, Subst))
     firstMatch [] = pure Nothing
     firstMatch (rule : rest) = do
@@ -345,9 +355,9 @@
     pure (bts, state')
   _ -> throwIO (userError "Can't call _dataize from atoms with non-formation universe")
 
--- A number atom only operates on numeric data. Empty bytes (the result of
--- dataizing a bare formation ⟦𝐵⟧ or ⊥ now that 𝔻 is total) carry no number,
--- so the operand is rejected and the atom yields ⊥.
+-- A number atom only operates on numeric data. Empty bytes — a genuine
+-- zero-length byte array ⟦Δ ⤍ --⟧ — carry no number, so the operand is rejected
+-- and the atom yields ⊥.
 asNumber :: Bytes -> Maybe Double
 asNumber BtEmpty = Nothing
 asNumber bts = Just (either toDouble id (btsToNum bts))
diff --git a/src/Rule.hs b/src/Rule.hs
--- a/src/Rule.hs
+++ b/src/Rule.hs
@@ -363,7 +363,7 @@
 -- and morphing driver, where a rule applies to the entire configuration rather
 -- than to nested redexes. The leading '[Subst]' seeds matching with pre-bound
 -- meta-variables: the morphing driver passes the global universe bound to 'e',
--- the second argument of 𝕄(n, e), so the 'root' rule reads it directly instead
+-- the second argument of 𝕄(n, e), so the 'universe' rule reads it directly instead
 -- of through a 'global()' build-term function. Pass '[substEmpty]' for no seed.
 matchExpressionWithRule' :: [Subst] -> Expression -> Y.Rule -> RuleContext -> IO [Subst]
 matchExpressionWithRule' = matchExpressionBy matchExpression'
diff --git a/test/CLISpec.hs b/test/CLISpec.hs
--- a/test/CLISpec.hs
+++ b/test/CLISpec.hs
@@ -867,9 +867,9 @@
       withStdin "Q -> [[ D> 01- ]]" $
         testCLISucceeded ["dataize"] ["01-"]
 
-    it "dataizes empty object to empty bytes" $
+    it "fails to dataize an empty object, which dataizes the terminator ⊥" $
       withStdin "Q -> [[ ]]" $
-        testCLISucceeded ["dataize"] ["--"]
+        testCLIFailed ["dataize"] ["terminator ⊥"]
 
     it "dataizes with --sequence" $
       withStdin "{[[ @ -> [[ x -> [[ D> 01-, y -> ? ]](y -> [[ ]]) ]].x ]]}" $
@@ -1085,7 +1085,8 @@
             , "  \\phinoConclusion{ \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> e_1 ) }{ e }{ s_1 }{ n_3 }{ s_3 } }"
             , "\\end{phinoMorphingInference}"
             , "\\begin{phinoMorphingInference}"
-            , "  \\phinoName{root}"
+            , "  \\phinoName{universe}"
+            , "  \\phinoLabel{\\Phi}"
             , "  \\phinoCondition{ e \\not= Q }"
             , "  \\phinoPremise{ \\phinoNormalize{ e }{ n } }"
             , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }"
@@ -1137,10 +1138,6 @@
             , "  \\phinoCondition{ [ D \\char44{} L \\char44{} @ ] \\cap B = \\emptyset }"
             , "  \\phinoPremise{ \\phinoDataize{ T }{ e }{ s_1 }{ \\delta }{ s_2 } }"
             , "  \\phinoConclusion{ \\phinoDataize{ [[ B ]] }{ e }{ s_1 }{ \\delta }{ s_2 } }"
-            , "\\end{phinoDataizationInference}"
-            , "\\begin{phinoDataizationInference}"
-            , "  \\phinoName{end}"
-            , "  \\phinoConclusion{ \\phinoDataize{ T }{ e }{ s }{ |--| }{ s } }"
             , "\\end{phinoDataizationInference}"
             , "\\begin{phinoDataizationInference}"
             , "  \\phinoName{norm}"
diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs
--- a/test/DataizeSpec.hs
+++ b/test/DataizeSpec.hs
@@ -127,9 +127,10 @@
 
   -- 'norm' matches the bare meta 𝑛, which unifies with any expression, so it is
   -- guarded to fire only when 𝑛 is neither a formation ('not (formation 𝑛)',
-  -- left to 'delta'/'box'/'fire'/'none') nor the termination ⊥ ('not (𝑛 = ⊥)',
-  -- left to 'end'). The dataization clauses are therefore disjoint and their
-  -- order in 'dataization.yaml' cannot change behavior.
+  -- left to 'delta'/'box'/'fire'/'none') nor the termination ⊥ ('not (𝑛 = ⊥)').
+  -- 𝔻 is partial: ⊥ matches no clause and lands on the unmatched-term error
+  -- (#955). The dataization clauses are therefore disjoint and their order in
+  -- 'dataization.yaml' cannot change behavior.
   describe "dataization 'norm' is disjoint from the specific clauses" $ do
     let rctx = RuleContext (execBuildTerm ExRoot (defaultDataizeContext ExRoot))
         dataizeRule :: String -> Yaml.DataizeRule
@@ -150,8 +151,6 @@
     test
       dataize'
       [ ("[[ D> 00- ]] => 00-", ExFormation [BiDelta (BtOne "00")], ExRoot, BtOne "00")
-      , ("T => --", ExTermination, ExRoot, BtEmpty)
-      , ("[[ ]] => --", ExFormation [], ExRoot, BtEmpty)
       ,
         ( "[[ @ -> [[ D> 00-]] ]] => 00-"
         , ExFormation [BiTau AtPhi (ExFormation [BiDelta (BtOne "00"), BiVoid AtRho]), BiVoid AtRho]
@@ -186,6 +185,19 @@
         )
       ]
 
+  -- 𝔻 is partial (#955): the terminator ⊥ signals an error and lies outside its
+  -- domain, so it matches no dataization clause and 𝔻 stops there instead of
+  -- yielding empty bytes. A data-less formation ⟦⟧ ('none') dataizes ⊥, so it
+  -- fails through the very same path — it has nothing to dataize.
+  describe "fails to dataize the terminator" $ do
+    let failsOn desc input =
+          it desc $
+            let prog = Program ExRoot
+             in dataize' (input, (prog, Nothing) :| []) ExRoot emptyState (defaultDataizeContext ExRoot)
+                  `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException))
+    failsOn "throws on ⊥ instead of mapping it to empty bytes" ExTermination
+    failsOn "throws on a data-less formation, which dataizes ⊥" (ExFormation [])
+
   describe "labels every step with a defined rule or operation" $ do
     let verb op = case op of
           Yaml.OpMorph _ -> "morph"
@@ -261,12 +273,14 @@
     it "dataizes a located reference through the expected rules" $ do
       labels <- labelsOf "Q.foo.bar" "Q -> [[ foo -> [[ bar -> [[ @ -> Q.x ]] ]], x -> [[ D> 42- ]] ]]"
       labels `shouldBe` ["contextualize", "md", "dot", "copy", "mf"]
-    -- The 'none' rule no longer emits '--' itself: it delegates to 'end' by
-    -- dataizing ⊥, so the empty formation reduces through one labelled 'dataize'
-    -- step (𝔻(⟦⟧) → 𝔻(⊥)) before 'end' yields the empty bytes (#942).
-    it "dataizes an empty formation by delegating to end" $ do
-      labels <- labelsOf "Q" "Q -> [[ ]]"
-      labels `shouldBe` ["dataize"]
+    -- The 'none' rule dataizes ⊥ (𝔻(⟦⟧) → 𝔻(⊥)), which matches no clause now
+    -- that there is no 'end' rule, so an empty formation reduces through one
+    -- labelled 'dataize' step and then fails: it has nothing to dataize (#955).
+    it "fails to dataize an empty formation, which dataizes ⊥" $ do
+      prog <- parseProgramThrows "Q -> [[ ]]"
+      loc <- parseExpressionThrows "Q"
+      dataize prog (defaultDataizeContext loc)
+        `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException))
 
   testDataize
     [