diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,5 +1,34 @@
 # Changelog for ExchangeAlgebra
 
+## 0.5.3.0 - 2026-09-26
+
+### Added
+
+- `NFData` instances for base components, including account titles, units,
+  Hat labels, account metadata, and `HatBase` values, support forcing ledger keys.
+  The benchmark now uses these library instances in place of its local orphans.
+- `ExchangeAlgebra.Posting` provides `Posted`, `PostedError`,
+  `postedUpperBound`, `posted`, and `unPosted` for checked posting values;
+  `PostSide(HatSide, NotSide)` and `sideHat` for concrete sides; and `Posting`,
+  `entry`, and `postingAlg` for constructing and reading posting sequences.
+- `ExchangeAlgebra.Algebra.Transfer.Rule` provides `SignedNet`, `SettleRule`,
+  `retainedEarningsRule`, `SettlementBatch`, `SettleError`, `settleEntries`,
+  and `settlementSteps` for ordered settlement pairs. These names are also
+  available from the root `ExchangeAlgebra` umbrella. `settleEntries` returns
+  `Either` for non-finite nets, including those at excluded keys. Finite
+  settlement magnitudes can exceed the checked posting bound.
+- `ExchangeAlgebra.Journal.Transfer.Rule` provides `carryEntries` to generate
+  reversals under the selected source notes and one rounded exact net per
+  complete base under a supplied carry note. Add the result to the journal to
+  retain its audit entries. The same module provides `carryBefore` to replace
+  selected entries with those carried nets. Other entries, including existing
+  entries under the carry note, retain their notes and values. Both operations
+  return `Either` when exact aggregation fails.
+- `collapseEntries` and `collapseNetEntries` move selected algebra entries to
+  rewritten base coordinates, including wildcard axes. The former preserves
+  every posting; the latter nets the rewritten entries after axes coincide.
+  Add either result to the original ledger to retain its audit entries.
+
 ## 0.5.2.0 - 2026-09-23
 
 ### Added
diff --git a/exchangealgebra.cabal b/exchangealgebra.cabal
--- a/exchangealgebra.cabal
+++ b/exchangealgebra.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           exchangealgebra
-version:        0.5.2.0
+version:        0.5.3.0
 synopsis:       Exchange Algebra for bookkeeping and economic simulation
 description:    Please see the README on GitHub at <https://github.com/yakagika/ExchangeAlgebra#readme>
 category:       Accounting, Finance, Math
@@ -104,6 +104,7 @@
       ExchangeAlgebra.Optimize
       ExchangeAlgebra.Optimize.Annealing
       ExchangeAlgebra.Optimize.GA
+      ExchangeAlgebra.Posting
       ExchangeAlgebra.Render.Bookkeeping
       ExchangeAlgebra.Render.Csv
       ExchangeAlgebra.Render.Simulation
@@ -123,7 +124,7 @@
       ExchangeAlgebra.Value
       ExchangeAlgebra.Write
   other-modules:
-      Paths_exchangealgebra
+      ExchangeAlgebra.Algebra.Transfer.Closing
   hs-source-dirs:
       src
   ghc-options: -feager-blackholing
@@ -238,6 +239,10 @@
       Algebra.ExactSumSpec
       Algebra.ProjWildcardSpec
       Golden.WriteRows
+      Journal.CarrySpec
+      Posting.NoNumPosted
+      Posting.PostingSpec
+      Posting.SettleSpec
       Transfer.RuleSpec
   hs-source-dirs:
       test
diff --git a/src/ExchangeAlgebra/Algebra/Base.hs b/src/ExchangeAlgebra/Algebra/Base.hs
--- a/src/ExchangeAlgebra/Algebra/Base.hs
+++ b/src/ExchangeAlgebra/Algebra/Base.hs
@@ -39,6 +39,7 @@
 import              Data.Time           (Day, TimeOfDay)
 import GHC.Stack (HasCallStack, callStack, prettyCallStack)
 import qualified Data.Binary as Binary
+import Control.DeepSeq (NFData(..))
 
 customError :: HasCallStack => String -> a
 customError msg = error (msg ++ "\nCallStack:\n" ++ prettyCallStack callStack)
@@ -121,6 +122,8 @@
             | HatNot
             deriving (Enum, Eq, Ord, Show, Generic)
 
+instance NFData Hat
+
 instance Hashable Hat where
 instance Binary.Binary Hat
 
@@ -139,6 +142,8 @@
 data BaseForSingleHat = BaseForSingleHat
     deriving (Eq,Ord,Generic)
 
+instance NFData BaseForSingleHat
+
 instance Show BaseForSingleHat where
     show _ = ""
 
@@ -189,6 +194,9 @@
 data HatBase a where
      (:<)  :: (BaseClass a) => {_hat :: Hat,  _base :: a } -> HatBase a
 
+instance (BaseClass a, NFData a) => NFData (HatBase a) where
+    rnf (hatValue :< baseValue) = rnf hatValue `seq` rnf baseValue
+
 instance (BaseClass a, Binary.Binary a) => Binary.Binary (HatBase a) where
     put (h :< b) = Binary.put h >> Binary.put b
     get = (:<) <$> Binary.get <*> Binary.get
@@ -430,6 +438,9 @@
             | MS  -- ^ minus stock (stock decrease; Liability\/Equity and contra assets)
             | OUT -- ^ output (flow out; Cost)
             deriving (Ord, Show, Eq)
+
+instance NFData PIMO where
+    rnf value = value `seq` ()
 
 -- | The division-to-PIMO map of the standard interpretation (the @g@ of
 -- Proposition 5.3.8 restricted to non-contra accounts): Assets are plus
diff --git a/src/ExchangeAlgebra/Algebra/Base/Account/Types.hs b/src/ExchangeAlgebra/Algebra/Base/Account/Types.hs
--- a/src/ExchangeAlgebra/Algebra/Base/Account/Types.hs
+++ b/src/ExchangeAlgebra/Algebra/Base/Account/Types.hs
@@ -14,10 +14,12 @@
     , ReportingEligibility(..)
     ) where
 
+import Control.DeepSeq (NFData(..))
+
 -- | Account division (financial-statement classification). The
 -- 'ExchangeAlgebra.Algebra.Base.AccountBase'
 -- correspondence instance lives in "ExchangeAlgebra.Algebra.Base" (the class's
--- home module), so this declaration stays instance-free.
+-- home module).
 data AccountDivision = Assets       -- ^ Assets
                      | Equity       -- ^ Equity
                      | Liability    -- ^ Liability
@@ -25,12 +27,18 @@
                      | Revenue      -- ^ Revenue
                      deriving (Ord, Show, Eq)
 
+instance NFData AccountDivision where
+    rnf value = value `seq` ()
+
 -- | Credit/debit distinction. v'Side' is the wildcard used by legacy APIs.
 data Side = Credit -- ^ Credit side.
           | Debit  -- ^ Debit side.
           | Side   -- ^ Wildcard.
           deriving (Ord, Show, Eq)
 
+instance NFData Side where
+    rnf value = value `seq` ()
+
 -- | Registry-level policy for automatic closing entries.
 --
 -- 'CloseByDivision' derives the transfer side from 'AccountDivision'.
@@ -40,12 +48,18 @@
                  | NoClose         -- ^ Do not generate an automatic closing entry.
                  deriving (Show, Eq)
 
+instance NFData ClosingRule where
+    rnf value = value `seq` ()
+
 -- | Fixed/Current distinction. Used for classifying account titles as fixed or current.
 data FixedCurrent = Fixed   -- ^ Fixed
                   | Current -- ^ Current
                   | Other   -- ^ Other (expenses, revenues, etc.)
                   deriving (Show, Eq)
 
+instance NFData FixedCurrent where
+    rnf value = value `seq` ()
+
 -- | Accounting role of an account-basis coordinate. Roles are not assumed to
 -- be mutually exclusive; see
 -- 'ExchangeAlgebra.Algebra.Base.Account.Registry.AccountSemantics' in the
@@ -61,6 +75,9 @@
     | ReportingSubtotal
     deriving (Show, Eq)
 
+instance NFData AccountRole where
+    rnf value = value `seq` ()
+
 -- | Context in which an account title may be used as a posting coordinate.
 -- Enforcement is introduced by the checked-conversion API in a later land;
 -- this type is the canonical metadata used by that gate.
@@ -72,6 +89,9 @@
     | NotPostable
     deriving (Show, Eq)
 
+instance NFData PostingCapability where
+    rnf value = value `seq` ()
+
 -- | Meaning of the legacy five-way 'AccountDivision' value.
 --
 -- This separates a genuine statement classification from a bookkeeping
@@ -84,6 +104,13 @@
     | NoStatementDivision
     deriving (Show, Eq)
 
+instance NFData DivisionSemantics where
+    rnf value = case value of
+        StatementDivision division        -> rnf division
+        BookkeepingControlClass division  -> rnf division
+        DirectionEncoding division        -> rnf division
+        NoStatementDivision               -> ()
+
 -- | Semantic status of an account's normal posting side.
 data HomeSideSemantics
     = FixedHomeSide Side
@@ -92,6 +119,13 @@
     | NoPostingSide
     deriving (Show, Eq)
 
+instance NFData HomeSideSemantics where
+    rnf value = case value of
+        FixedHomeSide side       -> rnf side
+        ContextDependentHomeSide -> ()
+        NoFixedHomeSide          -> ()
+        NoPostingSide            -> ()
+
 -- | Coarse reporting eligibility. Actual presentation remains a function of
 -- reporting context and policy and is implemented in a later land.
 data ReportingEligibility
@@ -100,3 +134,6 @@
     | DerivedPresentation
     | NotPresented
     deriving (Show, Eq)
+
+instance NFData ReportingEligibility where
+    rnf value = value `seq` ()
diff --git a/src/ExchangeAlgebra/Algebra/Base/Element.hs b/src/ExchangeAlgebra/Algebra/Base/Element.hs
--- a/src/ExchangeAlgebra/Algebra/Base/Element.hs
+++ b/src/ExchangeAlgebra/Algebra/Base/Element.hs
@@ -18,11 +18,12 @@
 
     To use your own type as a basis component, declare an 'Element' instance.
     A single distinguished value must serve as the wildcard used by the
-    transfer engine and by projection operations:
+    transfer engine and by projection operations. Derive 'NFData' when keys
+    containing this component must be fully evaluated:
 
     @
     data Company = CompanyA | CompanyB | CompanyWildcard
-      deriving (Eq, Ord, Show, Generic, Hashable, Typeable)
+      deriving (Eq, Ord, Show, Generic, Hashable, NFData, Typeable)
 
     instance Element Company where
       wildcard = CompanyWildcard
@@ -63,6 +64,7 @@
 import GHC.Generics (Generic)
 import Data.Hashable
 import Data.Typeable (Typeable, cast, typeOf)
+import Control.DeepSeq (NFData(..))
 import qualified Data.Binary as Binary
 import qualified Data.Binary.Get as BinaryGet
 import qualified Data.Binary.Put as BinaryPut
@@ -203,6 +205,11 @@
 -- Used to decompose multi-dimensional bases (tuples) into per-axis keys for indexing.
 data AxisKey = forall a. Element a => AxisKey !a
 
+-- | Force the stored axis to weak head normal form without requiring 'NFData'
+-- from every user-defined 'Element'.
+instance NFData AxisKey where
+    rnf (AxisKey axis) = axis `seq` ()
+
 instance Eq AxisKey where
     AxisKey x == AxisKey y = case cast y of
         Nothing -> False
@@ -502,6 +509,8 @@
 -- (2026-06-11 調査)。Enum/Binary 序数の安定のため削除はせず, 新名称への移行を促す。
 {-# DEPRECATED Commutation "通信費 (communication expenses) — use 'CommunicationExpenses' instead" #-}
 
+instance NFData AccountTitles
+
 instance Hashable AccountTitles where
     {-# INLINE hashWithSalt #-}
     hashWithSalt salt x = hashWithSalt salt (fromEnum x)
@@ -541,6 +550,8 @@
                 | Amount
                 | CountUnit
                 deriving (Show, Ord, Eq, Enum,Generic)
+
+instance NFData CountUnit
 
 instance Hashable CountUnit where
     {-# INLINE hashWithSalt #-}
diff --git a/src/ExchangeAlgebra/Algebra/Transfer.hs b/src/ExchangeAlgebra/Algebra/Transfer.hs
--- a/src/ExchangeAlgebra/Algebra/Transfer.hs
+++ b/src/ExchangeAlgebra/Algebra/Transfer.hs
@@ -15,8 +15,12 @@
     Mixed wildcard positions can make the legacy tree lookup miss matching
     entries even for disjoint rules. Overlap priority is unspecified, and
     matching is symmetric (ledger wildcards also match concrete patterns).
-    These known limitations are preserved for compatibility.
-    Use "ExchangeAlgebra.Algebra.Transfer.Rule" for one-way source matching.
+    P3 is required only for equivalence with the legacy @transfer@ and
+    @finalStockTransfer@ APIs, which match symmetrically. The new
+    "ExchangeAlgebra.Algebra.Transfer.Rule" API uses one-way matching in
+    @transferEntries@ and groups @closingEntries@ by actual base; both treat
+    a wildcard stored in the ledger as a value. These known legacy
+    limitations are preserved for compatibility.
 
     Package for Exchange Algebra defined by Hiroshi Deguchi.
 
diff --git a/src/ExchangeAlgebra/Algebra/Transfer/Closing.hs b/src/ExchangeAlgebra/Algebra/Transfer/Closing.hs
new file mode 100644
--- /dev/null
+++ b/src/ExchangeAlgebra/Algebra/Transfer/Closing.hs
@@ -0,0 +1,39 @@
+{-|
+Module      : ExchangeAlgebra.Algebra.Transfer.Closing
+Description : Shared closing posting construction.
+
+This internal Foundation module constructs a source reversal and destination
+posting using the algebra. The transfer rules and Accounting settlement select
+the destination side before calling 'closingPairBy'. Read 'closingPairBy' after
+the source-side rules in the calling module.
+
+The pair implements the posting construction used in Definition 9.
+-}
+module ExchangeAlgebra.Algebra.Transfer.Closing
+    ( closingPairBy
+    ) where
+
+import ExchangeAlgebra.Algebra
+    ( Alg
+    , HatVal
+    , HatBaseClass(..)
+    , ExBaseClass(..)
+    , AccountTitles
+    , Redundant((.+))
+    , (.@)
+    )
+
+-- | Reverse a closing balance and post it to the given destination account.
+-- The first argument transforms the source to the target side: @id@ retains
+-- Hat/Not, and 'revHat' reverses it. The caller must classify the source,
+-- and the value must satisfy the non-negative,
+-- finite posting contract of '.@'.
+closingPairBy :: (HatVal v, ExBaseClass b)
+              => (b -> b)
+              -> AccountTitles
+              -> v
+              -> b
+              -> Alg v b
+closingPairBy targetSide targetAccount value source
+    =  (value .@ revHat source)
+    .+ (value .@ setAccountTitle (targetSide source) targetAccount)
diff --git a/src/ExchangeAlgebra/Algebra/Transfer/Rule.hs b/src/ExchangeAlgebra/Algebra/Transfer/Rule.hs
--- a/src/ExchangeAlgebra/Algebra/Transfer/Rule.hs
+++ b/src/ExchangeAlgebra/Algebra/Transfer/Rule.hs
@@ -1,4 +1,9 @@
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 {- |
 Module      : ExchangeAlgebra.Algebra.Transfer.Rule
@@ -7,8 +12,10 @@
 Definition 9 describes a transfer by adding source cancellations and target
 postings to the original algebra. For @Right entries = transferEntries rules a@,
 @a .+ entries@ is precisely that expression. This module returns only the
-additional entries, preserving the original audit trail. It never applies
-@bar@. 'closingEntries' explicitly nets each closing account first.
+additional entries, preserving the original audit trail. Only
+'collapseNetEntries' applies @bar@ to rewritten entries. 'closingEntries'
+uses sequential side totals from the source entries, while 'settleEntries'
+accepts signed nets already computed by its caller.
 
 == Laws
 
@@ -24,7 +31,10 @@
   P2, patterns are disjoint; P3, ledger bases contain no wildcards; P4, axes
   are not nested tuples; P5, transformed values are nonzero. The legacy table
   translates 'Relabel', 'MulBy' and 'DivBy' to @id@, @(* p)@ and @(/ p)@,
-  respectively, and applying the new rules returns @Right entries@.
+  respectively, and applying the new rules returns @Right entries@. P3 is
+  needed only for equivalence with legacy @transfer@, whose matching is
+  symmetric. 'transferEntries' matches one way and treats ledger wildcards
+  as values.
 * Relation: @obs (a .+ entries) ~= obs (transfer a table)@.
 * Observation: @obs@ as defined above, including every target base.
 * Tolerance: relative @1e-9@; tested values are integers in @1..1000000@,
@@ -36,7 +46,10 @@
 * Subject: 'closingEntries' and legacy @finalStockTransfer@.
 * Preconditions: concrete ledger bases, valid Hat\/Not postings and values
   in the L1 range; the ledger includes only entries up to the closing date.
-  Closing returns @Right entries@.
+  Closing returns @Right entries@. Concrete bases are needed only for
+  equivalence with legacy @finalStockTransfer@ and its symmetric matching;
+  'closingEntries' groups by each actual base, including ledger wildcards
+  as values.
 * Relation: @obs (a .+ entries) ~= obs (finalStockTransfer a)@.
 * Observation: @obs@, including 'RetainedEarnings' and all retained axes.
 * Tolerance: relative @1e-9@ within the stated range. Large historical
@@ -77,6 +90,18 @@
 * Tolerance: none.
 * Instances: all lawful 'HatVal' and 'HatBaseClass' instances (closing also
   requires 'ExBaseClass'). Hat reversal is never numeric negation.
+
+=== L6: coordinate collapse
+
+* Subject: 'collapseEntries' and 'collapseNetEntries'.
+* Preconditions: non-negative valid postings and an exact additive value type.
+* Relation: @bar (x .+ collapseEntries p f x) ==
+  bar (x .+ collapseNetEntries p f x)@. The raw form has twice as many
+  postings as @proj p x@ and twice its norm; the net form calls 'bar' after
+  rewriting the base parts.
+* Observation: net ledger and raw posting count and norm.
+* Tolerance: exact.
+* Instances: @MoneyDecimal@ with 'HatBaseClass' bases.
 -}
 module ExchangeAlgebra.Algebra.Transfer.Rule
     ( TransferScale(..)
@@ -89,24 +114,41 @@
     , relabel
     , scaleBy
     , divideBy
+      -- * Additional entries
     , transferEntries
+    , collapseEntries
+    , collapseNetEntries
+      -- * Closing entries
     , ClosingSide(..)
     , closingSide
     , closingEntries
+    , SettleRule
+    , retainedEarningsRule
+    , SettlementBatch
+    , SignedNet
+    , SettleError(..)
+    , settleEntries
+    , settlementSteps
     ) where
 
 import           Data.Binary (Binary(..))
 import           Data.Hashable (Hashable)
 import           Data.List (find, sortOn, tails)
+import           Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
+import           Data.Maybe (mapMaybe)
 import           GHC.Generics (Generic)
 import           ExchangeAlgebra.Algebra
                      ( Alg(..), HatVal(..), HatBaseClass(..), ExBaseClass(..)
-                     , Hat(..), AccountTitles(..), Redundant((.+))
-                     , ignoreWildcard, foldEntries
+                     , Hat(..), HatBase(..), CountUnit(..), Element(..)
+                     , AccountTitles(..), Redundant((.+), (.^), bar, norm)
+                     , (.@)
+                     , ignoreWildcard, foldEntries, mapBasePart, proj
+                     , postFromNetBy, vals
                      , accountSpec, asClosing, ClosingRule(..)
                      , classifyAccountDivision, classifyAccountContra
                      , pimoFromDivision, pimoFlip, PIMO(..) )
+import ExchangeAlgebra.Algebra.Transfer.Closing (closingPairBy)
 
 -- | How a rule changes the value it moves.
 data TransferScale v
@@ -204,6 +246,8 @@
 matches :: HatBaseClass b => b -> b -> Bool
 matches patternBase entry = ignoreWildcard entry patternBase == entry
 
+-- * Additional entries
+
 -- | Generate cancellation and destination entries, without the input ledger.
 -- Input values must satisfy the ordinary non-negative, finite posting contract.
 -- 'Relabel'-only rules cannot fail. Scaled overflow returns 'NonFiniteResult',
@@ -239,6 +283,62 @@
             DivBy coefficient -> value / coefficient
         cancellation = value :@ revHat source
 
+-- | Move selected entries to new base coordinates while retaining every posting.
+-- Query patterns use one-way matching: only a pattern wildcard matches any
+-- coordinate. The function rewrites each selected 'BasePart' with the supplied
+-- function, so callers can replace an axis with its wildcard. A transfer
+-- rule's target wildcard instead keeps the source coordinate; it cannot turn
+-- a concrete coordinate into a wildcard.
+--
+-- The result contains only the added entries: a Hat-reversed copy of each
+-- selected posting and its rewritten copy. Add it to the ledger with @(.+)@.
+-- Values remain non-negative, and this function does not call 'bar', so it
+-- retains redundant audit detail. 'collapseNetEntries' nets the rewritten
+-- entries instead. 'postFromNetBy' generates new postings for each netted
+-- classification; both collapse functions move the coordinates of the same
+-- entries.
+-- On an axis-preserving ledger, @norm . bar@ cannot cancel across axes.
+--
+-- >>> type T = Alg Double (HatBase CountUnit)
+-- >>> x = 10 .@ Not :< Yen .+ 4 .@ Hat :< Dollar :: T
+-- >>> let moved = collapseEntries [HatNot :< wildcard] (const wildcard) x
+-- >>> norm moved
+-- 28.0
+-- >>> length (vals moved)
+-- 4
+collapseEntries :: (HatVal v, HatBaseClass b)
+                => [b] -> (BasePart b -> BasePart b) -> Alg v b -> Alg v b
+collapseEntries pats f x = (.^) selected .+ mapBasePart f selected
+  where
+    selected = proj pats x
+
+-- | Move selected entries to new base coordinates and net the rewritten side.
+-- The result contains only added entries: a Hat-reversed copy of the selected
+-- postings plus @bar (mapBasePart f selected)@. This function calls 'bar'
+-- internally after rewriting, so opposite sides from distinct original axes
+-- can cancel when the new base parts coincide. Add the result to the original
+-- ledger with @(.+)@. It leaves the original audit entries in place.
+--
+-- Query wildcards match one way. A wildcard in a transfer rule's target
+-- preserves the source coordinate; use this function to replace a concrete
+-- coordinate with a wildcard. 'collapseEntries' retains all rewritten
+-- postings. 'postFromNetBy' generates new postings for each netted
+-- classification, while this function moves the coordinates of the same
+-- entries. On an axis-preserving ledger, @norm . bar@ does not cancel across
+-- axes.
+--
+-- >>> type T = Alg Double (HatBase CountUnit)
+-- >>> x = 10 .@ Not :< Yen .+ 4 .@ Hat :< Dollar :: T
+-- >>> norm (bar (x .+ collapseNetEntries [HatNot :< wildcard] (const wildcard) x))
+-- 6.0
+collapseNetEntries :: (HatVal v, HatBaseClass b)
+                   => [b] -> (BasePart b -> BasePart b) -> Alg v b -> Alg v b
+collapseNetEntries pats f x = (.^) selected .+ bar (mapBasePart f selected)
+  where
+    selected = proj pats x
+
+-- * Closing entries
+
 -- | The retained-earnings side selected by a closing account's PIMO direction.
 data ClosingSide
     = ClosingKeep -- ^ IN: retain Hat/Not (revenue or contra cost).
@@ -266,7 +366,7 @@
         | otherwise = ordinaryDirection
     ordinaryDirection = pimoFromDivision (classifyAccountDivision title)
 
--- | Generate closing entries from each eligible base's exact net balance.
+-- | Generate closing entries from each eligible base's sequential side totals.
 -- Supply only postings through the closing date. Hat and Not totals are
 -- compared without a tolerance; their non-negative difference is closed.
 -- This deliberately folds the source sequences (audit detail) per base,
@@ -302,12 +402,92 @@
         | otherwise = checkedPair source (notTotal - hatTotal) source
     checkedPair source value balanceBase
         | isErrorValue value = Left (NonFiniteBalance source)
-        | otherwise = Right (closingPair value balanceBase)
-    closingPair value source = case closingSide (getAccountTitle source) of
-        Nothing -> Zero
-        Just side ->
-            let targetSource = case side of
-                    ClosingKeep -> source
-                    ClosingFlip -> revHat source
-            in (value :@ revHat source)
-                .+ (value :@ setAccountTitle targetSource RetainedEarnings)
+        | otherwise = case closingSide (getAccountTitle balanceBase) of
+            Nothing   -> Right Zero
+            Just side -> Right
+                (closingPairBy (targetSide side) RetainedEarnings value balanceBase)
+    targetSide side = case side of
+        ClosingKeep -> id
+        ClosingFlip -> revHat
+
+-- | A closing rule containing only its destination account title.
+-- The private constructor restricts destinations to accounts compatible with
+-- the closing directions.
+newtype SettleRule = SettleRule AccountTitles
+
+-- | Close eligible accounts into 'RetainedEarnings', preserving all other axes.
+retainedEarningsRule :: SettleRule
+retainedEarningsRule = SettleRule RetainedEarnings
+
+-- | Settlement pairs in strictly ascending source-base order.
+-- A model returns only @Posting@ built with @entry@ and 'Monoid'. Settlement
+-- magnitudes can exceed the @Posted@ bound, so this type has no conversion to
+-- @Posting@ and no 'Semigroup' or 'Monoid' instance.
+--
+-- Record each pair separately in source-base order. Combining all pairs first
+-- can change the order of additions to a shared destination. For example,
+-- sequential increments @T, 1, -T@ with @T = 2^53@ give 0 in 'Double', whereas
+-- adding @T, -T, 1@ gives 1.
+newtype SettlementBatch b = SettlementBatch [(BasePart b, Alg Double b)]
+
+-- | A signed Not-minus-Hat net. This is not a non-negative posting magnitude.
+-- As a type synonym, it does not enforce finiteness or any numeric range.
+type SignedNet = Double
+
+-- | The first non-finite input net, identified by its complete base coordinates.
+data SettleError b = NonFiniteNet (BasePart b)
+
+deriving instance Eq (BasePart b) => Eq (SettleError b)
+deriving instance Show (BasePart b) => Show (SettleError b)
+
+-- | Construct one reversal and destination pair per eligible source base.
+-- Input values are signed Not-minus-Hat nets. Zero nets, accounts without a
+-- closing side, and destination bases produce no pair. Every pair has two
+-- finite, non-negative magnitudes equal to the absolute input net; the source
+-- reversal cancels that net exactly. Other base axes are preserved.
+--
+-- A non-finite input, including at an excluded key, returns 'Left' with the
+-- first key in ascending order. Finite magnitudes above
+-- 'ExchangeAlgebra.Posting.postedUpperBound' are accepted, without passing
+-- through 'ExchangeAlgebra.Posting.posted'. No implicit @bar@ or @compress@ is
+-- applied. Complexity: O(b) for b input bases.
+-- Law: subject: each generated settlement pair; preconditions: all nets finite.
+-- Relation: each reversal cancels its source net. For each destination base,
+-- its increment is the sum of @direction * net@ over the source bases, where
+-- @direction@ is +1 for 'ClosingKeep' and -1 for 'ClosingFlip'.
+-- Observation: sums of @decL@ and @decR@ lifted to Rational for each pair.
+-- Tolerance: exact. Instances: 'ExBaseClass' bases with Double posting values.
+settleEntries :: forall b. ExBaseClass b
+              => SettleRule
+              -> Map (BasePart b) SignedNet
+              -> Either (SettleError b) (SettlementBatch b)
+settleEntries (SettleRule destination) amounts
+    = case mapMaybe nonFinite (Map.toAscList amounts) of
+        first : _ -> Left (NonFiniteNet first)
+        []        -> Right (SettlementBatch (mapMaybe close (Map.toAscList amounts)))
+  where
+    finite amount = not (isNaN amount || isInfinite amount)
+    nonFinite (coordinates, amount)
+        | finite amount = Nothing
+        | otherwise     = Just coordinates
+    close (coordinates, amount)
+        | amount == 0 = Nothing
+        | coordinates == base (setAccountTitle source destination) = Nothing
+        | otherwise = case closingSide (getAccountTitle source) of
+            Nothing   -> Nothing
+            Just side -> Just
+                (coordinates, closingPairBy (targetSide side) destination (abs amount) source)
+      where
+        source = merge (sourceSide amount) coordinates :: b
+    sourceSide amount
+        | amount < 0 = Hat
+        | otherwise  = Not
+    targetSide side = case side of
+        ClosingKeep -> id
+        ClosingFlip -> revHat
+
+-- | Read the pairs in strictly ascending source-base order, without constraints
+-- on the base type. Record each pair before proceeding to the next source.
+-- Complexity: O(1) to expose the list; O(b) to consume b pairs.
+settlementSteps :: SettlementBatch b -> [(BasePart b, Alg Double b)]
+settlementSteps (SettlementBatch steps) = steps
diff --git a/src/ExchangeAlgebra/Journal/Transfer/Rule.hs b/src/ExchangeAlgebra/Journal/Transfer/Rule.hs
--- a/src/ExchangeAlgebra/Journal/Transfer/Rule.hs
+++ b/src/ExchangeAlgebra/Journal/Transfer/Rule.hs
@@ -1,27 +1,39 @@
 {- |
 Module      : ExchangeAlgebra.Journal.Transfer.Rule
-Description : Note-preserving transfer entries and closing across notes.
+Description : Note-preserving transfer and carry entries across notes.
 
 Use a qualified import to distinguish these functions from the Algebra API:
 
 > import qualified ExchangeAlgebra.Journal.Transfer.Rule as Transfer
 
-Definition 9 and laws L1-L5 are documented in
-"ExchangeAlgebra.Algebra.Transfer.Rule". Transfer lifts that operation over
-notes; closing reads the combined ledger and returns an unannotated algebra
-through 'Either'.
+The additional-entry operations return entries to add to the input journal.
+'carryBefore' instead returns the complete journal after replacing selected
+notes. Transfer lifts Definition 9 over notes; closing reads the combined
+ledger and returns an unannotated algebra through 'Either'. Read the
+additional-entry section before the complete-result section.
 -}
 module ExchangeAlgebra.Journal.Transfer.Rule
-    ( transferEntries
+    ( -- * Additional entries
+      transferEntries
     , closingEntries
+    , carryEntries
+      -- * Complete results
+    , carryBefore
     ) where
 
 import qualified Data.HashMap.Strict as Map
-import           ExchangeAlgebra.Algebra (Alg, HatVal, HatBaseClass, ExBaseClass)
+import qualified Data.Map.Strict as OrderedMap
+import           ExchangeAlgebra.Algebra (Alg, HatVal, ExBaseClass, (.@), Redundant((.^)))
 import           ExchangeAlgebra.Algebra.Transfer.Rule (TransferRules, TransferApplyError)
 import qualified ExchangeAlgebra.Algebra.Transfer.Rule as Rule
-import           ExchangeAlgebra.Journal (Journal, Note, toMap, fromMap, toAlg)
+import           ExchangeAlgebra.Algebra.Base (Hat(..), HatBaseClass(..))
+import           ExchangeAlgebra.Journal (Journal, Note, (.|), toMap, fromMap, toAlg)
+import qualified ExchangeAlgebra.Journal as Journal
+import           ExchangeAlgebra.Journal.Exact (ExactSumError)
+import qualified ExchangeAlgebra.Journal.Exact as Exact
 
+-- * Additional entries
+
 -- | Generate additional entries under the same notes as their sources.
 -- Each note is processed in the traversal order of 'toMap'. The first failure
 -- aborts the whole operation; no partial Journal is returned. This order is
@@ -51,3 +63,96 @@
 closingEntries :: (Note n, HatVal v, ExBaseClass b)
                => Journal n v b -> Either (TransferApplyError v b) (Alg v b)
 closingEntries = Rule.closingEntries . toAlg
+
+-- | Round selected complete-base nets once and attach the carry note.
+carryNetEntries :: (Note n, HatBaseClass b)
+                => n
+                -> Journal n Double b
+                -> Either ExactSumError (Journal n Double b)
+carryNetEntries carryNote selected = do
+    balances <- Exact.balanceMapByExact Just selected
+    pure (OrderedMap.foldlWithKey' append mempty balances)
+  where
+    append result coordinates (direction, value) = case direction of
+        EQ -> result
+        GT -> result <> ((value .@ merge Not coordinates) .| carryNote)
+        LT -> result <> ((value .@ merge Hat coordinates) .| carryNote)
+
+-- | Generate carry entries while retaining every original posting.
+-- Select source notes with the predicate, reverse the Hat or Not side of each
+-- selected scalar under its original note, and append one rounded exact net
+-- per complete base under the carry note. An exact zero net adds no entry.
+-- The net uses 'Exact.balanceMapByExact' on the selected original scalars;
+-- no @bar@ or intermediate rounding is applied. An aggregation failure
+-- returns 'Left' with 'ExactSumError'.
+--
+-- Inputs require concrete Hat or Not sides and finite, non-negative values.
+-- Selected nonzero HatNot entries lie outside this contract. Applying the
+-- returned entries cancels selected notes mathematically, but reading the
+-- resulting journal with Exact can fail: reversing Not and Hat entries of
+-- @2^1023@ at one base makes each side total @2^1024@.
+--
+-- Law: subject: 'carryEntries'. Preconditions: selected exact aggregation
+-- succeeds and the input meets the side and value contract above.
+-- Relation: for each base @b@, the Rational Not-minus-Hat balance obeys
+-- @exact_b(j <> e) - exact_b(j) = RN(s_b) - s_b@, where @e@ is the generated
+-- journal, @s_b@ is the selected exact net, and @RN@ rounds once to Double.
+-- Observation: Rational balances of original scalar entries, including zero
+-- bases. Tolerance: exact Rational equality. Instances: 'Note' and
+-- 'HatBaseClass' with Double values.
+carryEntries :: (Note n, HatBaseClass b)
+             => (n -> Bool)
+             -> n
+             -> Journal n Double b
+             -> Either ExactSumError (Journal n Double b)
+carryEntries selectedNote carryNote journal = do
+    carried <- carryNetEntries carryNote selected
+    pure (Journal.map (.^) selected <> carried)
+  where
+    selected = Journal.filterWithNote (\note _ -> selectedNote note) journal
+
+-- * Complete results
+
+-- | Replace selected notes with one rounded exact net per complete base.
+-- Other entries retain their notes, bases, sides, and values. Entries already
+-- under the carry note remain when that note is not selected. This returns
+-- the entire resulting journal: selected audit entries are discarded, rather
+-- than retained with cancellation entries. Positive nets become Not entries,
+-- negative nets become Hat entries, and exact zero nets add nothing.
+--
+-- For selected entries @S@, unselected entries @U@, and rounded carried
+-- entries @Q@, this function constructs @U <> Q@ directly. Its result has
+-- the same nonzero scalar-entry multiset as adding 'carryEntries' to the
+-- original journal and then forgetting notes selected by the predicate.
+-- This decomposition requires @not (selectedNote carryNote)@, concrete Hat
+-- or Not sides, finite non-negative values, and successful exact aggregation.
+-- It does not claim equality for zero entries, empty notes, or sequence order.
+-- Existing entries under the carry note remain and are not netted again.
+-- When @selectedNote carryNote@ is true, this function still carries as
+-- described, but the decomposition does not hold because forgetting the
+-- selected notes would also remove @Q@. Selected nonzero HatNot entries lie
+-- outside the contract.
+--
+-- The selected net is computed by 'Exact.balanceMapByExact' and rounded once
+-- per complete base. An aggregation failure returns 'Left' with
+-- 'ExactSumError'. Structurally, 'carryEntries' resembles
+-- 'ExchangeAlgebra.Algebra.Transfer.Rule.collapseNetEntries': both generate
+-- reversals and moved nets. The latter uses @bar@ after rewriting and has a
+-- different numeric contract. Complexity: O(e log(k + 1)) for e selected
+-- scalars and k distinct selected complete bases, plus filtering and merge.
+-- Law: subject: 'carryBefore'. Preconditions: the decomposition conditions
+-- above. Relation: the nonzero scalar-entry multiset equals that obtained
+-- from @forgetNotes p (j <> e)@ for @Right e = carryEntries p n j@.
+-- Observation: nonzero scalar-entry multiset. Tolerance: exact.
+-- Instances: 'Note' and 'HatBaseClass' with Double values.
+carryBefore :: (Note n, HatBaseClass b)
+            => (n -> Bool)
+            -> n
+            -> Journal n Double b
+            -> Either ExactSumError (Journal n Double b)
+carryBefore selectedNote carryNote journal = do
+    carried <- carryNetEntries carryNote selected
+    pure (retained <> carried)
+  where
+    selected = Journal.filterWithNote (\note _ -> selectedNote note) journal
+    retained = Journal.filterWithNote (\note _ -> not (selectedNote note)) journal
diff --git a/src/ExchangeAlgebra/Posting.hs b/src/ExchangeAlgebra/Posting.hs
new file mode 100644
--- /dev/null
+++ b/src/ExchangeAlgebra/Posting.hs
@@ -0,0 +1,199 @@
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DerivingStrategies #-}
+
+-- | Build checked postings in the Accounting layer.
+-- The module uses the foundation algebra to construct @Posting@ values without
+-- implicit cancellation. Models and simulators consume these postings. Read
+-- checked values, sides, and then entries.
+--
+-- Posting construction follows Definitions 3-5.
+module ExchangeAlgebra.Posting
+    ( -- * Posting values
+      Posted
+    , PostedError(..)
+    , postedUpperBound
+    , posted
+    , unPosted
+      -- * Posting sides
+    , PostSide(..)
+    , sideHat
+      -- * Postings
+    , Posting
+    , entry
+    , postingAlg
+    ) where
+
+import Control.DeepSeq (NFData(..))
+import Data.Binary (Binary(..))
+import Data.Hashable (Hashable(..))
+import GHC.Generics (Generic)
+
+import ExchangeAlgebra.Algebra (Alg(Zero), HatVal(isErrorValue), (.+), (.@))
+import ExchangeAlgebra.Algebra.Base
+    ( Hat(..)
+    , HatBaseClass(BasePart, merge, base)
+    )
+
+-- * Posting values
+
+-- | A checked posting value with no 'Num', 'Fractional', or 'Real' instance.
+--
+-- Invariant: the stored 'Double' is finite and lies in @[0, 2^900]@;
+-- zero is stored as positive zero. Construct values through 'posted'.
+newtype Posted = Posted Double
+    deriving stock (Eq, Ord, Show)
+
+instance NFData Posted where
+    rnf (Posted value) = rnf value
+
+instance Hashable Posted where
+    hashWithSalt salt (Posted value) = hashWithSalt salt value
+
+-- | Decoding checks the same invariant as 'posted' and fails on invalid input.
+instance Binary Posted where
+    put = put . unPosted
+    get = do
+        value <- get
+        case posted value of
+            Left failure    -> fail (show failure)
+            Right validated -> pure validated
+
+-- | The first failed check, in the order used by 'posted'.
+data PostedError
+    = NonFinite  -- ^ NaN or either infinity.
+    | Negative   -- ^ A finite value below zero.
+    | AboveBound -- ^ A finite value above 'postedUpperBound'.
+    deriving stock (Eq, Show, Generic)
+
+instance NFData PostedError
+
+-- | Inclusive bound @2^900@. A sum of nearly @2^123@ such values remains below
+-- the largest finite Double (less than @2^1024@), leaving aggregation headroom.
+-- Complexity: O(1).
+postedUpperBound :: Double
+postedUpperBound = 2 ^ (900 :: Int)
+
+-- | Validate a value, normalizing negative zero to positive zero.
+-- Checks non-finiteness, negativity, and the upper bound in that order,
+-- returning the corresponding 'PostedError' on failure.
+--
+-- For every finite @x@ in @[0, postedUpperBound]@, with @normalizeZero x@
+-- equal to positive zero when @x == 0@ and to @x@ otherwise:
+--
+-- > fmap unPosted (posted x) == Right (normalizeZero x)
+--
+-- The law uses exact 'Double' equality, with the sign of zero also normalized.
+-- Finite, nonnegative values use the same 'isErrorValue' check as '.@'.
+-- 'postedUpperBound' is checked only at the posting entry point.
+-- Complexity: O(1).
+posted :: Double -> Either PostedError Posted
+posted value
+    | isErrorValue value       = Left (invalidValueError value)
+    | value > postedUpperBound = Left AboveBound
+    | value == 0               = Right (Posted 0)
+    | otherwise                = Right (Posted value)
+  where
+    invalidValueError invalid
+        | isNaN invalid || isInfinite invalid = NonFinite
+        | otherwise                           = Negative
+
+-- | Read a checked value. For every @p@, @posted (unPosted p) == Right p@.
+-- Complexity: O(1).
+unPosted :: Posted -> Double
+unPosted (Posted value) = value
+
+-- * Posting sides
+
+-- | The two posting sides; query wildcard 'HatNot' is excluded.
+data PostSide
+    = HatSide -- ^ The @Hat@ side.
+    | NotSide -- ^ The 'Not' side.
+    deriving stock (Eq, Ord, Show, Enum, Bounded, Generic)
+
+instance Binary PostSide
+
+instance Hashable PostSide
+
+instance NFData PostSide
+
+-- | Embed a posting side into a query-capable hat.
+-- @sideHat HatSide == Hat@ and @sideHat NotSide == Not@; 'HatNot' is never returned.
+-- Complexity: O(1).
+sideHat :: PostSide -> Hat
+sideHat HatSide = Hat
+sideHat NotSide = Not
+
+-- * Postings
+
+-- | Postings built through 'entry' and 'Monoid', without implicit cancellation
+-- or compression. Equality and display delegate to the underlying 'Alg'.
+-- Equality is structural and depends on construction order. To compare
+-- multisets of postings instead, compare the results of @toASCList . postingAlg@.
+newtype Posting b = Posting (Alg Double b)
+
+instance HatBaseClass b => Eq (Posting b) where
+    Posting left == Posting right = left == right
+
+instance HatBaseClass b => Show (Posting b) where
+    showsPrec precedence (Posting algebra) = showsPrec precedence algebra
+
+instance NFData (Posting b) where
+    rnf (Posting algebra) = rnf algebra
+
+-- | Preserve algebra addition:
+--
+-- > postingAlg (a <> b) == (postingAlg a .+ postingAlg b)
+--
+-- This law uses 'Alg' equality without a tolerance for every 'HatBaseClass'
+-- instance, so it also preserves the multiset of postings. Associativity
+-- holds as equality of posting multisets, using
+-- @sameMultiset x y = toASCList x == toASCList y@:
+--
+-- > sameMultiset (postingAlg ((a <> b) <> c)) (postingAlg (a <> (b <> c)))
+--
+-- Complexity: the same as '(.+)' on the underlying algebras.
+instance HatBaseClass b => Semigroup (Posting b) where
+    Posting left <> Posting right = Posting (left .+ right)
+
+-- | The empty posting obeys @postingAlg mempty == Zero@ using exact 'Alg' equality.
+-- The identity laws hold as equality of posting multisets for every
+-- 'HatBaseClass' instance, without a numeric tolerance:
+--
+-- > sameMultiset (postingAlg (mempty <> a)) (postingAlg a)
+-- > sameMultiset (postingAlg (a <> mempty)) (postingAlg a)
+--
+-- Here @sameMultiset x y = toASCList x == toASCList y@.
+-- Complexity: O(1) for 'mempty'; combination uses the 'Semigroup' instance.
+instance HatBaseClass b => Monoid (Posting b) where
+    mempty = Posting Zero
+
+-- | Read the underlying algebra. For every side, checked value, and base part:
+--
+-- > postingAlg (entry side value part) == unPosted value .@ merge (sideHat side) part
+--
+-- This is a one-way conversion with exact 'Alg' equality. For a list @xs@
+-- of @(side, value, part)@ triples, let @mk (s, v, p) = entry s v p@ and
+-- @sameMultiset x y = toASCList x == toASCList y@. Conversion and projection
+-- preserve the multiset of postings for every query list @qs@, including
+-- 'HatNot' and coordinate wildcards:
+--
+-- > sameMultiset (postingAlg (foldMap mk xs))
+-- >              (foldr (.+) Zero (map (postingAlg . mk) xs))
+-- > sameMultiset (proj qs (postingAlg (foldMap mk xs)))
+-- >              (foldr (.+) Zero [proj qs (postingAlg (mk x)) | x <- xs])
+--
+-- These laws use exact multiset equality without a numeric tolerance for
+-- every 'HatBaseClass' instance. Complexity of 'postingAlg': O(1).
+postingAlg :: Posting b -> Alg Double b
+postingAlg (Posting algebra) = algebra
+
+-- | Build one posting from a side, checked value, and base coordinates.
+-- A zero value produces 'Zero' through '(.@)'. The side is embedded by
+-- 'sideHat' and the coordinates are combined with 'merge'.
+--
+-- > postingAlg (entry side value part) == unPosted value .@ merge (sideHat side) part
+--
+-- The law holds with exact 'Alg' equality for every 'HatBaseClass' instance.
+-- Complexity: O(1).
+entry :: HatBaseClass b => PostSide -> Posted -> BasePart b -> Posting b
+entry side value part = Posting (unPosted value .@ merge (sideHat side) part)
diff --git a/test/Journal/CarrySpec.hs b/test/Journal/CarrySpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Journal/CarrySpec.hs
@@ -0,0 +1,277 @@
+-- | Acceptance properties for explicit journal carryover.
+module Journal.CarrySpec (runTests) where
+
+import Control.Monad (unless)
+import qualified Data.HashMap.Strict as HashMap
+import qualified Data.Map.Strict as Map
+import System.Exit (exitFailure)
+import Test.QuickCheck
+
+import ExchangeAlgebra.Algebra ((.@), foldEntries)
+import ExchangeAlgebra.Algebra.Base
+    ( AccountTitles(..)
+    , CountUnit(..)
+    , Hat(..)
+    , HatBase(..)
+    )
+import ExchangeAlgebra.Journal (Journal, (.|))
+import qualified ExchangeAlgebra.Journal as Journal
+import ExchangeAlgebra.Journal.Transfer.Rule (carryBefore, carryEntries)
+import ExchangeAlgebra.Journal.Exact (ExactSumError(..))
+
+-- | Test postings use two base axes and integer note labels.
+type Part = (CountUnit, AccountTitles)
+
+-- | One scalar posting with its complete base coordinates.
+type Row = (Int, Part, Hat, Double)
+
+-- | The generated journal's concrete base has unit and account coordinates.
+type TestJournal = Journal Int Double (HatBase Part)
+
+-- | Include decimal values and the binary64 rounding boundary.
+valueGen :: Gen Double
+valueGen = elements [0.1, 0.2, 0.3, 1, 2, 2 ^ (53 :: Int), 2 ^ (53 :: Int) + 2]
+
+-- | Vary selected notes, retained notes, sides, and complete bases.
+rowsGen :: Gen [Row]
+rowsGen = do
+    count <- chooseInt (0, 18)
+    vectorOf count $ do
+        note <- elements [0, 1, 2, 3, 4, 9]
+        unit <- elements [Yen, Dollar]
+        account <- elements [Cash, Deposits, Products]
+        side <- elements [Not, Hat]
+        value <- valueGen
+        pure (note, (unit, account), side, value)
+
+-- | Retain the redundancy of each original scalar posting.
+build :: [Row] -> TestJournal
+build = foldMap (\(note, coordinates, side, value) ->
+    (value .@ (side :< coordinates)) .| note)
+
+-- | Extract individual scalar entries, including their original note.
+rows :: TestJournal -> [Row]
+rows journal = concatMap entries (HashMap.toList (Journal.toMap journal))
+  where
+    entries (note, algebra) = foldEntries
+        (\previous value (side :< coordinates) ->
+            (note, coordinates, side, value) : previous)
+        []
+        algebra
+
+-- | Count repeated entries without relying on their storage order.
+multiset :: Ord a => [a] -> Map.Map a Int
+multiset = Map.fromListWith (+) . fmap (\entry -> (entry, 1))
+
+-- | Compute exact signed balances directly from the scalar entries.
+balances :: [Row] -> Map.Map Part Rational
+balances = Map.fromListWith (+) . fmap contribution
+  where
+    contribution (_, coordinates, side, value) =
+        (coordinates, case side of
+            Not    -> toRational value
+            Hat    -> negate (toRational value)
+            HatNot -> error "CarrySpec: concrete-side invariant violated")
+
+-- | Carry preserves retained scalars and rounds only each selected net.
+propCarry :: Property
+propCarry = forAll rowsGen $ \original ->
+    case carryBefore (< 3) 9 (build original) of
+      Left failure -> counterexample (show failure) False
+      Right after  -> checkCarry original (rows after)
+
+-- | Forgetting selected notes after adding carry entries matches replacement.
+-- The carry note 9 is outside the selected notes 0, 1, and 2.
+propCarryEntriesDecomposition :: Property
+propCarryEntriesDecomposition = forAll rowsGen $ \original ->
+    let journal = build original
+        observed = do
+            additions <- carryEntries (< 3) 9 journal
+            pure (Journal.filterWithNote (\note _ -> note >= 3) (journal <> additions))
+    in fmap (multiset . filter nonzero . rows) observed
+        === fmap (multiset . filter nonzero . rows) (carryBefore (< 3) 9 journal)
+  where
+    nonzero (_, _, _, value) = value /= 0
+
+-- | Each base's exact balance changes by the rounding of its selected net.
+propCarryEntriesBalance :: Property
+propCarryEntriesBalance = forAll rowsGen $ \original ->
+    let journal = build original
+        selectedBalances = balances
+            (filter (\(note, _, _, _) -> note < 3) original)
+        originalBalances = balances original
+        observed = do
+            additions <- carryEntries (< 3) 9 journal
+            pure (balances (rows (journal <> additions)))
+        check result = all (matches result) allCoordinates
+        allCoordinates = Map.keys (Map.union originalBalances selectedBalances)
+        matches result coordinates =
+            let before = Map.findWithDefault 0 coordinates originalBalances
+                after = Map.findWithDefault 0 coordinates result
+                selected = Map.findWithDefault 0 coordinates selectedBalances
+                rounded = toRational (fromRational selected :: Double)
+            in after - before == rounded - selected
+    in fmap check observed === Right True
+
+-- | Compare exact balances and entry multisets after a successful carry.
+checkCarry :: [Row] -> [Row] -> Property
+checkCarry original observed =
+    let retained = filter (\(note, _, _, _) -> note >= 3) original
+        retainedCounts = multiset retained
+        observedCounts = multiset observed
+        originalBalances = balances original
+        observedBalances = balances observed
+        selectedBalances = balances
+            (filter (\(note, _, _, _) -> note < 3) original)
+        expectedCarried =
+            [ (9, coordinates, netSide amount, fromRational (abs amount))
+            | (coordinates, amount) <- Map.toAscList selectedBalances
+            , amount /= 0
+            ]
+        allCoordinates = Map.keys (Map.unions
+            [originalBalances, observedBalances, selectedBalances])
+        retainedPresent = all (\(entry, count) ->
+            Map.findWithDefault 0 entry observedCounts >= count)
+            (Map.toList retainedCounts)
+        otherRetained = filter (\(note, _, _, _) -> note /= 9) retained
+        otherObserved = filter (\(note, _, _, _) -> note /= 9) observed
+        roundedExactlyOnce coordinates =
+            let beforeBalance = Map.findWithDefault 0 coordinates originalBalances
+                afterBalance = Map.findWithDefault 0 coordinates observedBalances
+                selectedBalance = Map.findWithDefault 0 coordinates selectedBalances
+                roundedSelected = toRational (fromRational selectedBalance :: Double)
+            in afterBalance - beforeBalance == roundedSelected - selectedBalance
+        valid (_, _, side, value) =
+            side /= HatNot && value > 0 && not (isNaN value) && not (isInfinite value)
+    in conjoin
+        [ multiset observed === multiset (retained ++ expectedCarried)
+        , counterexample "retained scalar multiset" (property retainedPresent)
+        , multiset otherObserved === multiset otherRetained
+        , counterexample "carry difference is not the selected net's one rounding"
+            (property (all roundedExactlyOnce allCoordinates))
+        , counterexample "carry generated an invalid magnitude or side"
+            (property (all valid observed))
+        ]
+  where
+    netSide amount
+        | amount > 0 = Not
+        | otherwise  = Hat
+
+-- | An exact cancellation adds nothing, even with an existing carry note.
+propZeroAndExistingNote :: Property
+propZeroAndExistingNote =
+    let original =
+            [ (0, (Yen, Cash), Not, 0.1)
+            , (1, (Yen, Cash), Hat, 0.1)
+            , (9, (Yen, Deposits), Not, 3)
+            ]
+        after = fmap rows (carryBefore (< 3) 9 (build original))
+    in fmap multiset after === Right (multiset [(9, (Yen, Deposits), Not, 3)])
+
+-- | An existing entry on the carry note and complete base is appended to.
+propCarryNoteCollision :: Property
+propCarryNoteCollision =
+    let original =
+            [ (0, (Yen, Cash), Not, 2)
+            , (9, (Yen, Cash), Not, 2)
+            , (0, (Dollar, Cash), Hat, 3)
+            ]
+        expected =
+            [ (9, (Yen, Cash), Not, 2)
+            , (9, (Yen, Cash), Not, 2)
+            , (9, (Dollar, Cash), Hat, 3)
+            ]
+    in fmap (multiset . rows) (carryBefore (< 3) 9 (build original))
+        === Right (multiset expected)
+
+-- | Carry entries keep the existing carry-note entry and add a separate net.
+propCarryEntriesCollision :: Property
+propCarryEntriesCollision =
+    let original =
+            [ (0, (Yen, Cash), Not, 2)
+            , (9, (Yen, Cash), Not, 2)
+            ]
+        expected =
+            [ (0, (Yen, Cash), Hat, 2)
+            , (9, (Yen, Cash), Not, 2)
+            ]
+    in fmap (multiset . rows) (carryEntries (< 3) 9 (build original))
+        === Right (multiset expected)
+
+-- | Both carry operations report the same checked aggregation failure.
+propCarryEntriesFailureParity :: Property
+propCarryEntriesFailureParity =
+    let maximumFinite = encodeFloat (2 ^ (53 :: Int) - 1) 971 :: Double
+        original = build
+            [ (0, (Yen, Cash), Not, maximumFinite)
+            , (1, (Yen, Cash), Not, maximumFinite)
+            ]
+        before = fmap (const ()) (carryBefore (< 3) 9 original)
+        entries = fmap (const ()) (carryEntries (< 3) 9 original)
+    in conjoin
+        [ before === Left SumOutOfRange
+        , entries === before
+        ]
+
+-- | Selection of every or no note follows the same exact balance contract.
+propSelectionExtremes :: Property
+propSelectionExtremes =
+    let original =
+            [ (0, (Yen, Cash), Not, 0.1)
+            , (1, (Yen, Cash), Not, 0.2)
+            , (9, (Dollar, Cash), Hat, 4)
+            ]
+        none = fmap (multiset . rows) (carryBefore (const False) 12 (build original))
+        allEntries = fmap (multiset . rows) (carryBefore (const True) 12 (build original))
+        expectedAll =
+            [ (12, (Yen, Cash), Not, fromRational
+                (toRational (0.1 :: Double) + toRational (0.2 :: Double)))
+            , (12, (Dollar, Cash), Hat, 4)
+            ]
+    in conjoin
+        [ none === Right (multiset original)
+        , allEntries === Right (multiset expectedAll)
+        ]
+
+-- | A selected complete base whose exact side sum exceeds Double fails.
+testOverflow :: IO ()
+testOverflow = do
+    let maximumFinite = encodeFloat (2 ^ (53 :: Int) - 1) 971 :: Double
+        original =
+            [ (0, (Yen, Cash), Not, maximumFinite)
+            , (1, (Yen, Cash), Not, maximumFinite)
+            ]
+        carried = carryBefore (< 3) 9 (build original)
+        additions = carryEntries (< 3) 9 (build original)
+    unless (fmap (const ()) carried == fmap (const ()) additions) $
+        failTest "carryEntries and carryBefore disagree on overflow"
+    case carried of
+        Left SumOutOfRange -> pure ()
+        Left failure     -> failTest ("unexpected overflow error: " ++ show failure)
+        Right _          -> failTest "overflowing selected side sum succeeded"
+
+-- | Report a deterministic acceptance failure and stop the suite.
+failTest :: String -> IO ()
+failTest message = do
+    putStrLn ("[FAIL] journal carry: " ++ message)
+    exitFailure
+
+-- | Run journal carry properties as part of the package test suite.
+runTests :: IO ()
+runTests = do
+    quickProperty 500 "carry" propCarry
+    quickProperty 500 "carry decomposition" propCarryEntriesDecomposition
+    quickProperty 500 "carry balance" propCarryEntriesBalance
+    quickProperty 1 "carry zero" propZeroAndExistingNote
+    quickProperty 1 "carry collision" propCarryNoteCollision
+    quickProperty 1 "carry entries collision" propCarryEntriesCollision
+    quickProperty 1 "carry error parity" propCarryEntriesFailureParity
+    quickProperty 1 "carry selection" propSelectionExtremes
+    testOverflow
+    putStrLn "[PASS] journal carry (retention, rounding, zero, and carry note)"
+
+-- | Run one named QuickCheck property and fail on a counterexample.
+quickProperty :: Testable property => Int -> String -> property -> IO ()
+quickProperty count label proposition = do
+    result <- quickCheckWithResult stdArgs { maxSuccess = count, chatty = False } proposition
+    unless (isSuccess result) $ failTest (label ++ ": " ++ output result)
diff --git a/test/Posting/NoNumPosted.hs b/test/Posting/NoNumPosted.hs
new file mode 100644
--- /dev/null
+++ b/test/Posting/NoNumPosted.hs
@@ -0,0 +1,28 @@
+{-# OPTIONS_GHC -fdefer-type-errors -Wno-deferred-type-errors #-}
+
+-- | Expressions that must fail when 'Posted' has no 'Num' instance.
+module Posting.NoNumPosted
+    ( literalPosted
+    , addPosted
+    , addPosting
+    , genericPosted
+    ) where
+
+import ExchangeAlgebra.Posting (Posted, Posting)
+import GHC.Generics (from)
+
+-- | Demand an integer literal at the protected posting type.
+literalPosted :: Posted
+literalPosted = 1
+
+-- | Demand arithmetic at the protected posting type.
+addPosted :: Posted -> Posted
+addPosted value = value + 1
+
+-- | Demand arithmetic at the protected posting container type.
+addPosting :: Posting b -> Posting b
+addPosting value = value + 1
+
+-- | Demand a Generic representation of the protected posting value.
+genericPosted :: Posted -> ()
+genericPosted value = from value `seq` ()
diff --git a/test/Posting/PostingSpec.hs b/test/Posting/PostingSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Posting/PostingSpec.hs
@@ -0,0 +1,338 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+
+-- | Validation, serialization, and algebraic laws for checked ledger postings.
+module Posting.PostingSpec (runTests) where
+
+import Control.DeepSeq (force, rnf)
+import Control.Exception (TypeError, evaluate, try)
+import Control.Monad (unless)
+import qualified Data.Binary as Binary
+import Data.Hashable (hash)
+import System.Exit (exitFailure)
+import Test.QuickCheck hiding (label)
+import ExchangeAlgebra.Algebra hiding (map, filter)
+import qualified ExchangeAlgebra.Posting as Posting
+import ExchangeAlgebra.Posting
+    ( Posted
+    , PostSide(..)
+    , Posting
+    , entry
+    , posted
+    , postedUpperBound
+    , postingAlg
+    , sideHat
+    , unPosted
+    )
+import qualified Posting.NoNumPosted as NoNum
+
+-- | Account and unit coordinates used for every algebraic property.
+type TestBase = HatBase (AccountTitles, CountUnit)
+
+-- | Values stay exact after all generated postings are added.
+type TestEntry = (PostSide, Posted, BasePart TestBase)
+
+-- | Generate accepted magnitudes across normal and subnormal exponents.
+genAccepted :: Gen Double
+genAccepted = frequency
+    [ (1, pure 0)
+    , (2, do
+          significand <- chooseInteger (1, 2 ^ (52 :: Int) - 1)
+          pure (encodeFloat significand (-1074)))
+    , (7, do
+          exponent <- chooseInt (-1022, 899)
+          significand <- chooseInteger (2 ^ (52 :: Int), 2 ^ (53 :: Int) - 1)
+          pure (encodeFloat significand (exponent - 52)))
+    , (1, pure postedUpperBound)
+    ]
+
+-- | Smart-constructor identity throughout its accepted domain.
+propAcceptedIdentity :: Property
+propAcceptedIdentity = forAll genAccepted $ \value ->
+    case posted value of
+        Left failure  -> counterexample (show (value, failure)) False
+        Right checked -> counterexample (show value) (unPosted checked == value)
+
+-- | Every validated posting survives reading and revalidation.
+propPostedRoundTrip :: Property
+propPostedRoundTrip = forAll genAccepted $ \value ->
+    case posted value of
+        Left failure  -> counterexample (show failure) False
+        Right checked -> posted (unPosted checked) === Right checked
+
+-- | Generate checked integer amounts without floating-point rounding in sums.
+genExactPosted :: Gen Posted
+genExactPosted = do
+    value <- chooseInteger (0, 1000)
+    case posted (fromInteger value) of
+        Right checked -> pure checked
+        Left failure  -> error ("integer test amount rejected: " ++ show failure)
+
+-- | Generate every concrete side and occasional wildcard coordinates.
+genEntry :: Gen TestEntry
+genEntry = do
+    side <- elements [HatSide, NotSide]
+    value <- genExactPosted
+    title <- elements [Cash, Products, Sales, wildcard]
+    unit <- elements [Yen, Amount, Dollar, wildcard]
+    pure (side, value, (title, unit))
+
+-- | Generate queries with empty, duplicate, overlapping, partial, and full cases.
+genQueries :: Gen [TestBase]
+genQueries = frequency
+    [ (1, pure [])
+    , (2, (: []) <$> genQuery)
+    , (2, do
+          query <- genQuery
+          pure [query, query])
+    , (2, do
+          title <- elements [Cash, Products, Sales]
+          pure [Hat :< (title, Yen), HatNot :< (title, wildcard)])
+    , (2, do
+          title <- elements [Cash, Products, Sales]
+          unit <- elements [Yen, Amount, Dollar]
+          pure [Not :< (title, unit)])
+    , (1, pure [HatNot :< (wildcard, wildcard)])
+    , (2, do
+          count <- chooseInt (1, 4)
+          vectorOf count genQuery)
+    ]
+
+-- | Sample every query hat and wildcard positions independently.
+genQuery :: Gen TestBase
+genQuery = do
+    queryHat <- elements [Hat, Not, HatNot]
+    title <- elements [Cash, Products, Sales, wildcard]
+    unit <- elements [Yen, Amount, Dollar, wildcard]
+    pure (queryHat :< (title, unit))
+
+-- | Generate posting lists and queries without forcing every projection to match.
+genAlgebraCase :: Gen ([TestEntry], [TestBase])
+genAlgebraCase = do
+    count <- chooseInt (0, 20)
+    entries <- vectorOf count genEntry
+    queries <- genQueries
+    pure (entries, queries)
+
+-- | Convert one checked entry through the public constructor.
+single :: TestEntry -> Posting TestBase
+single (side, value, part) = entry side value part
+
+-- | Ignore only the internal sequence order, preserving each posting's value and base.
+sameMultiset :: Alg Double TestBase -> Alg Double TestBase -> Bool
+sameMultiset left right = toASCList left == toASCList right
+
+-- | IX-8a: projection distributes across the checked posting list.
+propProjection :: Property
+propProjection = forAll genAlgebraCase $ \(entries, queries) ->
+    let checked = postingAlg (foldMap single entries)
+        raw = foldr (.+) Zero [postingAlg (single item) | item <- entries]
+        projected = foldr (.+) Zero
+            [proj queries (postingAlg (single item)) | item <- entries]
+    in counterexample (show (entries, queries)) $
+        sameMultiset checked raw && sameMultiset (proj queries checked) projected
+
+-- | Checked concatenation has both identities and is associative in the algebra.
+propMonoid :: Property
+propMonoid = forAll genAlgebraCase $ \(entries, _) ->
+    let (first, rest) = splitAt (length entries `div` 3) entries
+        (second, third) = splitAt (length rest `div` 2) rest
+        x = foldMap single first
+        y = foldMap single second
+        z = foldMap single third
+        zero = mempty :: Posting TestBase
+    in counterexample (show entries) $
+        sameMultiset (postingAlg (zero <> x)) (postingAlg x)
+        && sameMultiset (postingAlg (x <> zero)) (postingAlg x)
+        && sameMultiset (postingAlg ((x <> y) <> z)) (postingAlg (x <> (y <> z)))
+
+-- | Conversion preserves a single append with the algebra's structural equality.
+propConversion :: Property
+propConversion = forAll genAlgebraCase $ \(entries, _) ->
+    let (leftEntries, rightEntries) = splitAt (length entries `div` 2) entries
+        left = foldMap single leftEntries
+        right = foldMap single rightEntries
+    in counterexample (show entries) $
+        postingAlg (left <> right) == (postingAlg left .+ postingAlg right)
+
+-- | Fail an ordinary Boolean assertion through the same test harness.
+assertTest :: String -> Bool -> IO ()
+assertTest label success = unless success $ do
+    putStrLn ("[FAIL] ledger posting: " ++ label)
+    exitFailure
+
+-- | Run a named QuickCheck property and fail the executable on a counterexample.
+quickProperty :: Testable property => String -> property -> IO ()
+quickProperty label proposition = do
+    result <- quickCheckWithResult stdArgs { maxSuccess = 200, chatty = False } proposition
+    unless (isSuccess result) $ do
+        putStrLn ("[FAIL] " ++ label ++ ": " ++ output result)
+        exitFailure
+    putStrLn ("[PASS] " ++ label)
+
+-- | Check every validation boundary, including negative zero normalization.
+testValidation :: IO ()
+testValidation = do
+    let positiveInfinity = 1 / 0 :: Double
+        negativeInfinity = -1 / 0 :: Double
+        nanValue = 0 / 0 :: Double
+        nextAboveBound = postedUpperBound * (1 + 2 ** (-52))
+        smallestSubnormal = encodeFloat 1 (-1074) :: Double
+    assertTest "NaN rejected" (posted nanValue == Left Posting.NonFinite)
+    assertTest "positive Infinity rejected" $
+        posted positiveInfinity == Left Posting.NonFinite
+    assertTest "negative Infinity rejected" $
+        posted negativeInfinity == Left Posting.NonFinite
+    assertTest "negative finite value rejected" $
+        posted (-1e-300) == Left Posting.Negative
+    assertTest "next representable value above bound rejected" $
+        posted nextAboveBound == Left Posting.AboveBound
+    assertTest "2^1000 rejected" (posted (2 ** 1000) == Left Posting.AboveBound)
+    assertTest "zero accepted" (fmap unPosted (posted 0) == Right 0)
+    assertTest "negative zero normalized" $ case posted (-0.0) of
+        Right checked -> isPositiveZero (unPosted checked)
+        Left _        -> False
+    assertTest "smallest subnormal accepted" $
+        fmap unPosted (posted smallestSubnormal) == Right smallestSubnormal
+    assertTest "one accepted" (fmap unPosted (posted 1) == Right 1)
+    assertTest "upper bound accepted" $
+        fmap unPosted (posted postedUpperBound) == Right postedUpperBound
+  where
+    isPositiveZero value = value == 0 && isInfinite (1 / value) && 1 / value > 0
+
+-- | Binary instances round-trip valid values and reject invalid Posted bytes.
+testBinary :: IO ()
+testBinary = do
+    let smallestSubnormal = encodeFloat 1 (-1074) :: Double
+        checkedValues =
+            [value | Right value <- map posted [0, smallestSubnormal, 1, postedUpperBound]]
+        sides = [HatSide, NotSide]
+        rejects value = case Binary.decodeOrFail (Binary.encode (value :: Double)) of
+            Left _                      -> True
+            Right (_, _, (_ :: Posted)) -> False
+        decodedNegativeZero = Binary.decodeOrFail (Binary.encode (-0.0 :: Double))
+    assertTest "Posted Binary round trip" $
+        all (\value -> Binary.decode (Binary.encode value) == value) checkedValues
+    assertTest "PostSide Binary round trip" $
+        all (\side -> Binary.decode (Binary.encode side) == side) sides
+    assertTest "Posted Binary decoder validates" $
+        all rejects
+            [ 0 / 0
+            , 1 / 0
+            , -1 / 0
+            , -1e-300
+            , postedUpperBound * (1 + 2 ** (-52))
+            , 2 ** 1000
+            ]
+    assertTest "Posted Binary normalizes negative zero" $ case decodedNegativeZero of
+        Left _                          -> False
+        Right (_, _, (value :: Posted)) ->
+            unPosted value == 0 && 1 / unPosted value > 0
+    assertTest "NFData and Hashable instances" $
+        force checkedValues `seq` force sides `seq`
+        sum (map hash checkedValues) `seq` sum (map hash sides) `seq` True
+    assertTest "base component NFData instances" $
+        rnf (Cash :: AccountTitles) `seq`
+        rnf (Yen :: CountUnit) `seq`
+        rnf (AxisKey Cash) `seq`
+        rnf (Hat :: Hat) `seq`
+        rnf (BaseForSingleHat :: BaseForSingleHat) `seq`
+        rnf (PS :: PIMO) `seq`
+        rnf (Assets :: AccountDivision) `seq`
+        rnf (Credit :: Side) `seq`
+        rnf (Current :: FixedCurrent) `seq`
+        rnf (CloseByDivision :: ClosingRule) `seq`
+        rnf (ContraAccount :: AccountRole) `seq`
+        rnf (OrdinaryPosting :: PostingCapability) `seq`
+        rnf (StatementDivision Assets :: DivisionSemantics) `seq`
+        rnf (FixedHomeSide Credit :: HomeSideSemantics) `seq`
+        rnf (StatementEligible :: ReportingEligibility) `seq`
+        rnf (Not :< (Yen, Cash) :: HatBase (CountUnit, AccountTitles)) `seq`
+        True
+
+-- | Both posting sides map to concrete Hat values only.
+testSides :: IO ()
+testSides = do
+    assertTest "HatSide maps to Hat" (sideHat HatSide == Hat)
+    assertTest "NotSide maps to Not" (sideHat NotSide == Not)
+    assertTest "PostSide excludes HatNot" $
+        all ((/= HatNot) . sideHat) [minBound .. maxBound]
+
+-- | Three equal-base entries expose structural ordering without breaking the multiset law.
+testAssociativityRegression :: IO ()
+testAssociativityRegression = case traverse posted [1, 2, 3] of
+    Left failure                 -> do
+        putStrLn ("[FAIL] ledger posting fixture: " ++ show failure)
+        exitFailure
+    Right [first, second, third] -> do
+        let part = (Cash, Yen)
+            x = entry HatSide first part :: Posting TestBase
+            y = entry HatSide second part :: Posting TestBase
+            z = entry HatSide third part :: Posting TestBase
+            left = postingAlg ((x <> y) <> z)
+            right = postingAlg (x <> (y <> z))
+        assertTest "equal-base grouping changes structural order" (left /= right)
+        assertTest "equal-base grouping preserves the multiset" (sameMultiset left right)
+    Right _                      -> assertTest "three checked fixture values" False
+
+-- | Fixed queries cover each Hat value and both coordinate wildcard positions.
+testQueryCoverage :: IO ()
+testQueryCoverage = case posted 3 of
+    Left failure -> do
+        putStrLn ("[FAIL] ledger posting fixture: " ++ show failure)
+        exitFailure
+    Right value  -> do
+        let entries =
+                [ (HatSide, value, (Cash, Yen))
+                , (NotSide, value, (Products, Amount))
+                , (HatSide, value, (Sales, Dollar))
+                ]
+            queries =
+                [ Hat :< (Cash, wildcard)
+                , Not :< (wildcard, Amount)
+                , HatNot :< (Sales, wildcard)
+                ]
+            checked = postingAlg (foldMap single entries)
+            projected = foldr (.+) Zero
+                [proj queries (postingAlg (single item)) | item <- entries]
+        assertTest "three query hats and coordinate wildcards" $
+            sameMultiset (proj queries checked) projected
+
+-- | Deferred errors prove that clients cannot request Num for Posted.
+testNoNum :: IO ()
+testNoNum = do
+    literal <- try (evaluate NoNum.literalPosted) :: IO (Either TypeError Posted)
+    assertTest "Posted numeric literal is rejected" (isTypeError literal)
+    case posted 1 of
+        Left failure  -> do
+            putStrLn ("[FAIL] ledger posting fixture: " ++ show failure)
+            exitFailure
+        Right checked -> do
+            arithmetic <- try (evaluate (NoNum.addPosted checked))
+                :: IO (Either TypeError Posted)
+            assertTest "Posted arithmetic is rejected" (isTypeError arithmetic)
+            generic <- try (evaluate (NoNum.genericPosted checked))
+                :: IO (Either TypeError ())
+            assertTest "Posted Generic is rejected" (isTypeError generic)
+            container <- try (evaluate (NoNum.addPosting (mempty :: Posting TestBase)))
+                :: IO (Either TypeError (Posting TestBase))
+            assertTest "Posting arithmetic is rejected" (isTypeError container)
+  where
+    isTypeError (Left _) = True
+    isTypeError (Right _) = False
+
+-- | Register checked-posting tests with ExchangeAlgebra-test.
+runTests :: IO ()
+runTests = do
+    testValidation
+    testBinary
+    testSides
+    testAssociativityRegression
+    testQueryCoverage
+    testNoNum
+    quickProperty "V-1 accepted-domain identity" propAcceptedIdentity
+    quickProperty "validated posting round trip" propPostedRoundTrip
+    quickProperty "IX-8a projection and raw conversion" propProjection
+    quickProperty "Posting monoid laws" propMonoid
+    quickProperty "Posting conversion preserves structural append" propConversion
+    putStrLn "[PASS] checked ledger posting"
diff --git a/test/Posting/SettleSpec.hs b/test/Posting/SettleSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Posting/SettleSpec.hs
@@ -0,0 +1,189 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+-- | Ordered settlement pairs preserve source nets and exact accounting balance.
+module Posting.SettleSpec (runTests) where
+
+import Control.Monad (forM_, unless)
+import Data.List (foldl', sort)
+import qualified Data.Map.Strict as Map
+import System.Exit (exitFailure)
+import Test.QuickCheck hiding (label)
+
+import ExchangeAlgebra.Algebra hiding (filter, map)
+import ExchangeAlgebra.Algebra.Transfer.Rule
+
+-- | Two coordinates exercise complete-base ordering and axis preservation.
+type TestBase = HatBase (CountUnit, AccountTitles)
+
+-- | Signed input amounts indexed by complete base coordinates.
+type Nets = Map.Map (CountUnit, AccountTitles) Double
+
+-- | Cover zero, both signs, fractions, subnormals, and amounts above Posted.
+genNet :: Gen Double
+genNet = do
+    magnitude <- frequency
+        [ (3, elements [0, 0.1, 0.2, 1, 2 ^ (53 :: Int), 2 ^ (950 :: Int)
+                       , encodeFloat 1 (-1074), encodeFloat (2 ^ (53 :: Int) - 1) 971])
+        , (2, do
+              significand <- chooseInteger (1, 2 ^ (53 :: Int) - 1)
+              exponent <- chooseInt (-1074, 971)
+              pure (encodeFloat significand exponent))
+        ]
+    sign <- elements [1, -1]
+    pure (sign * magnitude)
+
+-- | Include closing, non-closing, and destination accounts on several units.
+genNets :: Gen Nets
+genNets = do
+    count <- chooseInt (0, 30)
+    entries <- vectorOf count $ do
+        unit <- elements [Yen, Dollar, Amount]
+        title <- elements [Sales, Purchases, Depreciation, Cash, RetainedEarnings, NetIncome]
+        amount <- genNet
+        pure ((unit, title), amount)
+    pure (Map.fromList entries)
+
+-- | Read scalar entries without cancellation or approximate comparisons.
+scalars :: Alg Double TestBase -> [(Double, TestBase)]
+scalars = foldEntries (\previous value postingBase -> (value, postingBase) : previous) []
+
+-- | The exact signed net at one complete base.
+netAt :: (CountUnit, AccountTitles) -> Alg Double TestBase -> Rational
+netAt coordinates = foldEntries add 0
+  where
+    add total value postingBase
+        | base postingBase /= coordinates = total
+        | hat postingBase == Not = total + toRational value
+        | otherwise = total - toRational value
+
+-- | Sum magnitudes as rationals rather than through floating-point norm.
+exactMagnitude :: Alg Double TestBase -> Rational
+exactMagnitude = foldEntries (\total value _ -> total + toRational value) 0
+
+-- | The key set, pair structure, signs, and debit/credit equality hold exactly.
+propSettlement :: Property
+propSettlement = forAll genNets $ \amounts ->
+    case settleEntries retainedEarningsRule amounts of
+      Left failure -> counterexample (show failure) False
+      Right batch -> checkSettlement amounts (settlementSteps batch)
+
+-- | Check each generated pair with exact Rational accounting readouts.
+checkSettlement :: Nets -> [((CountUnit, AccountTitles), Alg Double TestBase)] -> Property
+checkSettlement amounts steps =
+    let expectedKeys = Map.keys (Map.filterWithKey eligible amounts)
+        keys = map fst steps
+        checkPair (coordinates@(unit, title), algebra) =
+            let amount = Map.findWithDefault 0 coordinates amounts
+                sourceSide = sideFor amount
+                reverseSide = revHat sourceSide
+                targetSide = case closingSide title of
+                    Just ClosingKeep -> sourceSide
+                    _                -> reverseSide
+                expected = sort
+                    [ (abs amount, reverseSide :< coordinates)
+                    , (abs amount, targetSide :< (unit, RetainedEarnings))
+                    ]
+                valid (value, postingBase) =
+                    value >= 0 && not (isNaN value || isInfinite value)
+                    && hat postingBase /= HatNot
+            in conjoin
+                [ sort (scalars algebra) === expected
+                , length (scalars algebra) === 2
+                , netAt coordinates algebra + toRational amount === 0
+                , exactMagnitude (decL algebra) === exactMagnitude (decR algebra)
+                , property (all valid (scalars algebra))
+                ]
+    in conjoin
+        [ keys === expectedKeys
+        , property (and (zipWith (<) keys (drop 1 keys)))
+        , conjoin (map checkPair steps)
+        ]
+  where
+    eligible (_, title) amount = amount /= 0 && title /= RetainedEarnings
+        && closingSide title /= Nothing
+    sideFor amount
+        | amount > 0 = Not
+        | otherwise  = Hat
+
+-- | Report fixed regression failures through the ordinary test executable.
+assertTest :: String -> Bool -> IO ()
+assertTest label success = unless success $ do
+    putStrLn ("[FAIL] settlement: " ++ label)
+    exitFailure
+
+-- | Exclusion, both directions, and large finite magnitudes are deterministic.
+testFixed :: IO ()
+testFixed = do
+    let steps amounts = fmap settlementSteps
+            (settleEntries retainedEarningsRule amounts ::
+                Either (SettleError TestBase) (SettlementBatch TestBase))
+        excluded = Map.fromList
+            [ ((Yen, Sales), 0)
+            , ((Dollar, Purchases), -0.0)
+            , ((Yen, Cash), 10)
+            , ((Yen, RetainedEarnings), 12)
+            , ((Yen, NetIncome), 5)
+            ]
+    assertTest "empty input" (fmap null (steps Map.empty) == Right True)
+    assertTest "only excluded keys" (fmap null (steps excluded) == Right True)
+    assertTest "known keep and flip accounts" $
+        closingSide Sales == Just ClosingKeep && closingSide Purchases == Just ClosingFlip
+    forM_ [Sales, Purchases] $ \title ->
+        forM_ [1, -1] $ \sign -> do
+            let magnitude = 2 ^ (950 :: Int)
+                amount = sign * magnitude
+                coordinates = (Yen, title)
+                result = steps (Map.singleton coordinates amount)
+            assertTest "finite 2^950 accepted without Posted validation" $
+                case result of
+                    Right [(source, algebra)] -> source == coordinates
+                        && length (scalars algebra) == 2
+                        && all ((== magnitude) . fst) (scalars algebra)
+                        && netAt source algebra == negate (toRational amount)
+                        && exactMagnitude (decL algebra) == exactMagnitude (decR algebra)
+                    _                         -> False
+    -- Select three ClosingKeep accounts by their actual key order so the
+    -- destination increments are T, 1, -T, independent of enum ordering.
+    let titles = take 3 [title | title <- [minBound .. maxBound]
+                             , closingSide title == Just ClosingKeep]
+        sourceKeys = sort [(Yen, title) | title <- titles]
+        large = 2 ^ (53 :: Int)
+        result = steps (Map.fromList (zip sourceKeys [large, 1, -large]))
+        increments = fmap
+            (map (\(_, algebra) ->
+                fromRational (netAt (Yen, RetainedEarnings) algebra) :: Double))
+            result
+    assertTest "three distinct keep accounts in fixture" (length sourceKeys == 3)
+    assertTest "sequential destination increments preserve source order" $
+        increments == Right [large, 1, -large]
+        && fmap (foldl' (+) 0) increments == Right 0
+        && foldl' (+) 0 [large, -large, 1] == 1
+
+-- | All input keys obey the finite-input contract, even excluded accounts.
+testNonFinite :: IO ()
+testNonFinite = forM_ [0 / 0, 1 / 0, -1 / 0] $ \amount ->
+    forM_ [Sales, Cash, RetainedEarnings] $ \title -> do
+        let first = (Dollar, title)
+            second = (Yen, Sales)
+            result = settleEntries retainedEarningsRule
+                (Map.fromList [(second, amount), (first, amount)])
+                :: Either (SettleError TestBase) (SettlementBatch TestBase)
+        assertTest "first non-finite key, including excluded keys" $ case result of
+            Left (NonFiniteNet coordinates) -> coordinates == min first second
+            Right _                          -> False
+        assertTest "excluded non-finite key alone is rejected" $ case
+            (settleEntries retainedEarningsRule (Map.singleton (Dollar, Cash) amount)
+                :: Either (SettleError TestBase) (SettlementBatch TestBase)) of
+            Left (NonFiniteNet coordinates) -> coordinates == (Dollar, Cash)
+            Right _                          -> False
+
+-- | Run generated laws and boundary regressions with the main test suite.
+runTests :: IO ()
+runTests = do
+    testFixed
+    testNonFinite
+    result <- quickCheckWithResult stdArgs { maxSuccess = 500, chatty = False } propSettlement
+    unless (isSuccess result) $ do
+        putStrLn ("[FAIL] settlement properties: " ++ output result)
+        exitFailure
+    putStrLn "[PASS] settlement (order, keys, exact pairs, sides, axes, bounds, and errors)"
diff --git a/test/Spec.hs b/test/Spec.hs
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -76,6 +76,9 @@
 import qualified Transfer.RuleSpec as TransferRuleSpec
 import qualified Algebra.ProjWildcardSpec as ProjWildcardSpec
 import qualified Algebra.ExactSumSpec as ExactSumSpec
+import qualified Posting.PostingSpec as PostingSpec
+import qualified Posting.SettleSpec as SettleSpec
+import qualified Journal.CarrySpec as CarrySpec
 import           Numeric             (showHex)
 import           Control.Monad       (forM_)
 import           Control.Monad.ST
@@ -6969,6 +6972,9 @@
     ExactSumSpec.runTests
     TransferRuleSpec.runTests
     ProjWildcardSpec.runTests
+    PostingSpec.runTests
+    SettleSpec.runTests
+    CarrySpec.runTests
     testAccountTitlesBinary
     testPracticalAndManufacturingAccountTitles
     testAccountTitleClassification
diff --git a/test/Transfer/RuleSpec.hs b/test/Transfer/RuleSpec.hs
--- a/test/Transfer/RuleSpec.hs
+++ b/test/Transfer/RuleSpec.hs
@@ -369,6 +369,99 @@
     assertTest "closing target postings are not aggregated" $
         length (vals retained) == 4 && all (not . isErrorValue) (vals retained)
 
+-- | Two goods share an owner and differ only in the axis collapsed below.
+data ValuationGood = GoodA | GoodB | AnyValuationGood
+    deriving (Eq, Ord, Show, Generic)
+
+instance Hashable ValuationGood
+
+instance Element ValuationGood where
+    wildcard = AnyValuationGood
+
+type ValuationBase = HatBase (AccountTitles, ValuationGood, Owner, CountUnit)
+
+-- | Retain the raw count in its own axes, then net the value across goods.
+testValuationCollapse :: IO ()
+testValuationCollapse = do
+    let source good = Not :< (Products, good, Alice, Amount)
+        target good = Not :< (Products, good, Alice, Yen)
+        ledger = 5 .@ source GoodA .+ 3 .@ source GoodB
+            :: Alg MoneyDecimal ValuationBase
+        patternBase = Not :< (Products, wildcard, Alice, Yen)
+        dropGood (title, _, owner, unit) = (title, wildcard, owner, unit)
+        expected = Not :< (Products, wildcard, Alice, Yen)
+    rules <- requireRight "valuation rules" $
+        mkTransferRules [scaleBy (source GoodA) (target GoodA) 2,
+                         scaleBy (source GoodB) (target GoodB) 10]
+    valuationEntries <- requireRight "valuation transfer" (transferEntries rules ledger)
+    let valued = ledger .+ valuationEntries
+        collapsed = bar (valued .+ collapseNetEntries [patternBase] dropGood valued)
+    assertTest "valuation of two goods becomes one 40 posting" $
+        rawObservation collapsed == Map.singleton expected 40
+        && length (vals collapsed) == 1
+
+-- | Opposite sides cancel only after their good coordinates coincide.
+testRetainedCollapse :: IO ()
+testRetainedCollapse = do
+    let source good side = side :< (RetainedEarnings, good, Alice, Yen)
+        ledger = 10 .@ source GoodA Not .+ 4 .@ source GoodB Hat
+            :: Alg MoneyDecimal ValuationBase
+        patternBase = HatNot :< (RetainedEarnings, wildcard, Alice, Yen)
+        dropGood (title, _, owner, unit) = (title, wildcard, owner, unit)
+        expected = source AnyValuationGood Not
+        collapsed = bar (ledger .+ collapseNetEntries [patternBase] dropGood ledger)
+    assertTest "retained earnings net to one Not 6 posting" $
+        rawObservation collapsed == Map.singleton expected 6
+        && length (vals collapsed) == 1
+
+-- | Exact values expose count, norm, non-negativity and net equivalence.
+propCollapse :: Property
+propCollapse = forAll genLedger $ \ledger ->
+    let patterns = [HatNot :< (Cash, wildcard)]
+        dropUnit (title, _) = (title, wildcard)
+        selected = proj patterns ledger
+        raw = collapseEntries patterns dropUnit ledger
+        net = collapseNetEntries patterns dropUnit ledger
+    in counterexample (show (rawObservation raw, rawObservation net)) $
+        property (bar (ledger .+ raw) == bar (ledger .+ net)
+            && norm raw == 2 * norm selected
+            && all (>= 0) (vals raw ++ vals net)
+            && length (vals raw) == 2 * length (vals selected))
+  where
+    genLedger = do
+        count <- chooseInt (0, 30)
+        postings <- vectorOf count $ do
+            value <- chooseInteger (1, 100)
+            side <- elements [Hat, Not]
+            title <- elements [Cash, Products]
+            unit <- elements [Yen, Amount, wildcard]
+            pure (fromInteger value .@ side :< (title, unit))
+        pure (Algebra.fromList postings :: Alg MoneyDecimal TestBase)
+
+-- | Ledger wildcards remain literal in transfer matching and closing output.
+testWildcardLedger :: IO ()
+testWildcardLedger = do
+    let source = Not :< (Sales, wildcard)
+        ledger = 7 .@ source :: Alg MoneyDecimal TestBase
+        target = Not :< (Deposits, wildcard)
+    concrete <- requireRight "concrete source rule" $
+        mkTransferRules [relabel (Not :< (Sales, Yen)) target]
+    concreteEntries <- requireRight "concrete source application" $
+        transferEntries concrete ledger
+    assertTest "concrete source does not match ledger wildcard" $
+        Algebra.isZero concreteEntries
+    wildcardRule <- requireRight "wildcard source rule" $
+        mkTransferRules [relabel source target]
+    wildcardEntries <- requireRight "wildcard source application" $
+        transferEntries wildcardRule ledger
+    assertTest "wildcard source matches ledger wildcard" $
+        rawObservation wildcardEntries == rawObservation
+            (7 .@ revHat source .+ 7 .@ target)
+    closed <- requireRight "wildcard ledger closing" (closingEntries ledger)
+    assertTest "closing retains wildcard axis on earnings" $
+        rawObservation closed == rawObservation
+            (7 .@ revHat source .+ 7 .@ Not :< (RetainedEarnings, wildcard))
+
 -- | A good axis owned only by this acceptance fixture.
 data Good
     = Widget
@@ -466,10 +559,14 @@
     quickProperty "L4 canonical rules" propCanonical
     quickProperty "L5 Double" (propNonnegative (Proxy :: Proxy Double))
     quickProperty "L5 MoneyDecimal" (propNonnegative (Proxy :: Proxy MoneyDecimal))
+    quickProperty "L6 collapse" propCollapse
     testValidation
     testLegacyMiss
     testApplication
     testClosing
     testClosingOverflow
+    testValuationCollapse
+    testRetainedCollapse
+    testWildcardLedger
     testAcceptance
     putStrLn "[PASS] transfer rule regressions and two-period acceptance"