diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,13 @@
 # Changelog
 
+## 0.1.0.2 - 2026-08-21
+
+- Add the public quantale tower: `Quantale`, commutative, residuated, integral,
+  and chain refinements; Viterbi, Łukasiewicz, and tropical carriers; and
+  law coverage for the complete algebra.
+- Align focused and aggregate coherence tests with their actual dependency and
+  optimization boundaries.
+
 ## 0.1.0.1 - 2026-07-22
 
 - Documentation: the public `finite-lattice` sublibrary front door
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,6 +1,6 @@
 MIT License
 
-Copyright (c) 2026 The Blue Rose, Rosalia Fialkova
+Copyright (c) 2026 Blue Rose
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal
diff --git a/bench/abstract/Main.hs b/bench/abstract/Main.hs
--- a/bench/abstract/Main.hs
+++ b/bench/abstract/Main.hs
@@ -6,10 +6,8 @@
 import AbstractBench
   ( abstractBenchmarks,
   )
-import Moonlight.Pale.Bench.Runner
-  ( runBenchmark,
-  )
+import Test.Tasty.Bench (defaultMain)
 
 main :: IO ()
 main =
-  runBenchmark abstractBenchmarks
+  defaultMain [abstractBenchmarks]
diff --git a/bench/aggregate/Main.hs b/bench/aggregate/Main.hs
--- a/bench/aggregate/Main.hs
+++ b/bench/aggregate/Main.hs
@@ -9,13 +9,11 @@
 import FiniteLatticeBench
   ( finiteLatticeBenchmarkSuite,
   )
-import Moonlight.Pale.Bench.Runner
-  ( runBenchmarks,
-  )
+import Test.Tasty.Bench (defaultMain)
 
 main :: IO ()
 main =
-  runBenchmarks
+  defaultMain
     [ abstractBenchmarks,
       finiteLatticeBenchmarkSuite
     ]
diff --git a/bench/finite-lattice/Main.hs b/bench/finite-lattice/Main.hs
--- a/bench/finite-lattice/Main.hs
+++ b/bench/finite-lattice/Main.hs
@@ -6,10 +6,8 @@
 import FiniteLatticeBench
   ( finiteLatticeBenchmarkSuite,
   )
-import Moonlight.Pale.Bench.Runner
-  ( runBenchmark,
-  )
+import Test.Tasty.Bench (defaultMain)
 
 main :: IO ()
 main =
-  runBenchmark finiteLatticeBenchmarkSuite
+  defaultMain [finiteLatticeBenchmarkSuite]
diff --git a/moonlight-algebra.cabal b/moonlight-algebra.cabal
--- a/moonlight-algebra.cabal
+++ b/moonlight-algebra.cabal
@@ -1,6 +1,6 @@
 cabal-version:       3.4
 name:                moonlight-algebra
-version:             0.1.0.1
+version:             0.1.0.2
 homepage:            https://github.com/PaleRoses/moonlight
 bug-reports:         https://github.com/PaleRoses/moonlight/issues
 synopsis:            Algebraic type class tower for Pale Meridian.
@@ -57,6 +57,7 @@
     Moonlight.Algebra.Pure.Polynomial
     Moonlight.Algebra.Pure.PowerSet
     Moonlight.Algebra.Pure.Product
+    Moonlight.Algebra.Pure.Quantale
     Moonlight.Algebra.Pure.Quotient
     Moonlight.Algebra.Pure.Ring
     Moonlight.Algebra.Pure.SparseVec
@@ -128,6 +129,9 @@
   import: shared-properties
   visibility: private
   hs-source-dirs: src-laws
+  -- Law construction supports tests; it is absent from every benchmark link
+  -- graph and does not need production simplification.
+  ghc-options: -O0
   exposed-modules:
     Moonlight.Algebra.Effect.LawNames
     Moonlight.Algebra.Effect.Laws
@@ -153,8 +157,9 @@
   other-modules:
     AbstractTests
     OrderedLatticeSpec
+    QuantaleSpec
     SparseVecSpec
-  ghc-options: -Wall -Wcompat
+  ghc-options: -Wall -Wcompat -O0
   default-extensions:
     TypeFamilies
     UndecidableInstances
@@ -165,7 +170,6 @@
     , moonlight-algebra:abstract
     , moonlight-algebra:moonlight-algebra-laws
     , moonlight-core >= 0.1 && < 0.2
-    , moonlight-pale:test >= 0.1 && < 0.2
     , tasty >= 1.4 && < 1.6
     , tasty-hunit >= 0.10 && < 0.11
     , tasty-hedgehog >= 1.4 && < 1.5
@@ -176,6 +180,7 @@
   type: exitcode-stdio-1.0
   hs-source-dirs: test/finite-lattice
   main-is: Main.hs
+  ghc-options: -O0
   other-modules:
     FiniteLatticeSpec
     FiniteLatticeTests
@@ -187,20 +192,22 @@
     base >= 4.22 && < 5
     , containers >= 0.6 && < 0.9
     , moonlight-algebra:finite-lattice
-    , moonlight-pale:test >= 0.1 && < 0.2
     , tasty >= 1.4 && < 1.6
     , tasty-hunit >= 0.10 && < 0.11
     , tasty-quickcheck >= 0.10 && < 0.12
     , QuickCheck >= 2.14 && < 2.19
 
-test-suite moonlight-algebra-test
+-- The focused suites own behavior. This component owns only the union of their
+-- module, instance, and dependency surfaces, compiled at O0.
+test-suite moonlight-algebra-coherence-test
   import: shared-properties
   type: exitcode-stdio-1.0
   hs-source-dirs:
-    test/aggregate
+    test/coherence
     test/abstract
     test/finite-lattice
   main-is: Main.hs
+  ghc-options: -O0
   other-modules:
     AbstractTests
     FiniteLatticeSpec
@@ -208,6 +215,7 @@
     LawSpec
     OrderedLatticeSpec
     PresentationSpec
+    QuantaleSpec
     SparseVecSpec
   default-extensions:
     FunctionalDependencies
@@ -220,7 +228,6 @@
     , moonlight-algebra:finite-lattice
     , moonlight-algebra:moonlight-algebra-laws
     , moonlight-core >= 0.1 && < 0.2
-    , moonlight-pale:test >= 0.1 && < 0.2
     , tasty >= 1.4 && < 1.6
     , tasty-hedgehog >= 1.4 && < 1.5
     , tasty-hunit >= 0.10 && < 0.11
@@ -242,7 +249,6 @@
     , moonlight-algebra
     , moonlight-algebra:abstract
     , moonlight-core >= 0.1 && < 0.2
-    , moonlight-pale:bench >= 0.1 && < 0.2
     , tasty-bench >= 0.3 && < 0.6
     , vector >= 0.13 && < 0.14
 
@@ -270,7 +276,6 @@
     , deepseq >= 1.4 && < 1.6
     , lattices >= 2.2 && < 2.3
     , moonlight-algebra:finite-lattice
-    , moonlight-pale:bench >= 0.1 && < 0.2
     , tasty-bench >= 0.3 && < 0.6
     , vector >= 0.13 && < 0.14
 
@@ -305,6 +310,5 @@
     , moonlight-algebra:abstract
     , moonlight-algebra:finite-lattice
     , moonlight-core >= 0.1 && < 0.2
-    , moonlight-pale:bench >= 0.1 && < 0.2
     , tasty-bench >= 0.3 && < 0.6
     , vector >= 0.13 && < 0.14
diff --git a/src-abstract/Moonlight/Algebra/Pure/Quantale.hs b/src-abstract/Moonlight/Algebra/Pure/Quantale.hs
new file mode 100644
--- /dev/null
+++ b/src-abstract/Moonlight/Algebra/Pure/Quantale.hs
@@ -0,0 +1,218 @@
+-- | Quantales: monoids in the join-semilattice — 'tensor' distributes over
+-- 'join' and annihilates 'bottom' — with commutative and residuated
+-- refinements, and the Viterbi, Łukasiewicz and tropical carriers.
+--
+-- Laws: tensor is associative with unit 'tensorUnit'; tensor distributes over
+-- join on both sides and @tensor a bottom = bottom = tensor bottom a@;
+-- commutative quantales add @tensor a b = tensor b a@; residuated quantales
+-- satisfy the Galois law @joinLeq (tensor x y) z = joinLeq x (residual y z)@.
+-- 'IntegralQuantale' marks carriers whose unit is top; 'ChainQuantale' marks
+-- carriers whose join is selective.
+module Moonlight.Algebra.Pure.Quantale
+  ( Quantale (..),
+    CommutativeQuantale,
+    ResiduatedQuantale (..),
+    IntegralQuantale,
+    ChainQuantale,
+    ChainOrder (..),
+    Viterbi (..),
+    Lukasiewicz (..),
+    Tropical (..),
+    tensors,
+  )
+where
+
+import Data.Kind (Constraint, Type)
+import Moonlight.Algebra.Pure.Lattice
+  ( BoundedJoinSemilattice (..),
+    HeytingAlgebra (implies),
+    JoinSemilattice (..),
+    joinLeq,
+  )
+
+type Quantale :: Type -> Constraint
+class BoundedJoinSemilattice a => Quantale a where
+  tensor :: a -> a -> a
+  tensorUnit :: a
+
+instance Quantale () where
+  tensor _ _ = ()
+  tensorUnit = ()
+
+instance Quantale Bool where
+  tensor = (&&)
+  tensorUnit = True
+
+instance (Quantale left, Quantale right) => Quantale (left, right) where
+  tensor (leftA, rightA) (leftB, rightB) =
+    (tensor leftA leftB, tensor rightA rightB)
+  tensorUnit =
+    (tensorUnit, tensorUnit)
+
+instance Quantale value => Quantale (key -> value) where
+  tensor left right key =
+    tensor (left key) (right key)
+  tensorUnit =
+    const tensorUnit
+
+type CommutativeQuantale :: Type -> Constraint
+class Quantale a => CommutativeQuantale a
+
+instance CommutativeQuantale ()
+
+instance CommutativeQuantale Bool
+
+instance
+  (CommutativeQuantale left, CommutativeQuantale right) =>
+  CommutativeQuantale (left, right)
+
+instance CommutativeQuantale value => CommutativeQuantale (key -> value)
+
+type ResiduatedQuantale :: Type -> Constraint
+class CommutativeQuantale a => ResiduatedQuantale a where
+  residual :: a -> a -> a
+
+instance ResiduatedQuantale () where
+  residual _ _ = ()
+
+instance ResiduatedQuantale Bool where
+  residual = implies
+
+instance
+  (ResiduatedQuantale left, ResiduatedQuantale right) =>
+  ResiduatedQuantale (left, right)
+  where
+  residual (leftA, rightA) (leftB, rightB) =
+    (residual leftA leftB, residual rightA rightB)
+
+instance ResiduatedQuantale value => ResiduatedQuantale (key -> value) where
+  residual left right key =
+    residual (left key) (right key)
+
+-- | Marker law: 'tensorUnit' is the top element, so 'tensor' is two-sided
+-- deflationary and valuation fixpoints converge within the simple-path bound.
+type IntegralQuantale :: Type -> Constraint
+class Quantale a => IntegralQuantale a
+
+instance IntegralQuantale ()
+
+instance IntegralQuantale Bool
+
+instance
+  (IntegralQuantale left, IntegralQuantale right) =>
+  IntegralQuantale (left, right)
+
+instance IntegralQuantale value => IntegralQuantale (key -> value)
+
+-- | Marker law: 'join' is selective (returns one of its arguments), so a
+-- single witness attains any finite join.
+type ChainQuantale :: Type -> Constraint
+class Quantale a => ChainQuantale a
+
+instance ChainQuantale ()
+
+instance ChainQuantale Bool
+
+-- | The total order a selective 'join' induces on a chain quantale; the 'Ord'
+-- instance is lawful exactly when the 'ChainQuantale' law holds.
+type ChainOrder :: Type -> Type
+newtype ChainOrder a = ChainOrder {getChainOrder :: a}
+  deriving stock (Eq, Show)
+
+instance (ChainQuantale a, Eq a) => Ord (ChainOrder a) where
+  compare (ChainOrder left) (ChainOrder right)
+    | left == right = EQ
+    | joinLeq left right = LT
+    | otherwise = GT
+
+-- | Carrier discipline: values lie in the unit interval; the operations
+-- preserve it.
+type Viterbi :: Type -> Type
+newtype Viterbi a = Viterbi {getViterbi :: a}
+  deriving stock (Eq, Ord, Show)
+
+instance Ord a => JoinSemilattice (Viterbi a) where
+  join = max
+
+instance (Ord a, Num a) => BoundedJoinSemilattice (Viterbi a) where
+  bottom = Viterbi 0
+
+instance (Ord a, Num a) => Quantale (Viterbi a) where
+  tensor (Viterbi left) (Viterbi right) =
+    Viterbi (left * right)
+  tensorUnit = Viterbi 1
+
+instance (Ord a, Num a) => CommutativeQuantale (Viterbi a)
+
+instance (Ord a, Fractional a) => ResiduatedQuantale (Viterbi a) where
+  residual (Viterbi left) (Viterbi right)
+    | left <= right = Viterbi 1
+    | otherwise = Viterbi (right / left)
+
+instance (Ord a, Num a) => IntegralQuantale (Viterbi a)
+
+instance (Ord a, Num a) => ChainQuantale (Viterbi a)
+
+-- | Carrier discipline: values lie in the unit interval; the operations
+-- preserve it.
+type Lukasiewicz :: Type -> Type
+newtype Lukasiewicz a = Lukasiewicz {getLukasiewicz :: a}
+  deriving stock (Eq, Ord, Show)
+
+instance Ord a => JoinSemilattice (Lukasiewicz a) where
+  join = max
+
+instance (Ord a, Num a) => BoundedJoinSemilattice (Lukasiewicz a) where
+  bottom = Lukasiewicz 0
+
+instance (Ord a, Num a) => Quantale (Lukasiewicz a) where
+  tensor (Lukasiewicz left) (Lukasiewicz right) =
+    Lukasiewicz (max 0 (left + right - 1))
+  tensorUnit = Lukasiewicz 1
+
+instance (Ord a, Num a) => CommutativeQuantale (Lukasiewicz a)
+
+instance (Ord a, Num a) => ResiduatedQuantale (Lukasiewicz a) where
+  residual (Lukasiewicz left) (Lukasiewicz right) =
+    Lukasiewicz (min 1 (1 - left + right))
+
+instance (Ord a, Num a) => IntegralQuantale (Lukasiewicz a)
+
+instance (Ord a, Num a) => ChainQuantale (Lukasiewicz a)
+
+-- | Min-plus costs. The lattice order is the dual of the derived 'Ord': join
+-- is the numeric minimum and 'bottom' is 'TropicalInfinity'. The quantale
+-- laws hold over all of @a@; only integrality ('tensorUnit' as top) and the
+-- truncated 'residual' require the nonnegative cone.
+type Tropical :: Type -> Type
+data Tropical a
+  = TropicalFinite !a
+  | TropicalInfinity
+  deriving stock (Eq, Ord, Show)
+
+instance Ord a => JoinSemilattice (Tropical a) where
+  join = min
+
+instance Ord a => BoundedJoinSemilattice (Tropical a) where
+  bottom = TropicalInfinity
+
+instance (Ord a, Num a) => Quantale (Tropical a) where
+  tensor TropicalInfinity _ = TropicalInfinity
+  tensor _ TropicalInfinity = TropicalInfinity
+  tensor (TropicalFinite left) (TropicalFinite right) =
+    TropicalFinite (left + right)
+  tensorUnit = TropicalFinite 0
+
+instance (Ord a, Num a) => CommutativeQuantale (Tropical a)
+
+instance (Ord a, Num a) => ResiduatedQuantale (Tropical a) where
+  residual TropicalInfinity _ = TropicalFinite 0
+  residual (TropicalFinite _) TropicalInfinity = TropicalInfinity
+  residual (TropicalFinite left) (TropicalFinite right) =
+    TropicalFinite (max 0 (right - left))
+
+instance (Ord a, Num a) => ChainQuantale (Tropical a)
+
+tensors :: (Quantale a, Foldable foldable) => foldable a -> a
+tensors =
+  foldl' tensor tensorUnit
diff --git a/src-laws/Moonlight/Algebra/Effect/Laws.hs b/src-laws/Moonlight/Algebra/Effect/Laws.hs
--- a/src-laws/Moonlight/Algebra/Effect/Laws.hs
+++ b/src-laws/Moonlight/Algebra/Effect/Laws.hs
@@ -44,12 +44,11 @@
   )
 import Moonlight.Core qualified as Core
 import qualified Moonlight.Pale.Test.Laws.Algebraic as Algebraic
-import Moonlight.Pale.Test.LawSuite
-  ( LawBundle,
-    hedgehogLawDefinition,
-    lawBundleHedgehog,
-    lawSuiteGroup,
-    renderLawBundles,
+import Moonlight.Pale.Test.Laws.Suite
+  ( LawSuite,
+    lawGroup,
+    namedHedgehogLaw,
+    renderLawSuite,
   )
 import Test.Tasty (TestTree, testGroup)
 import Test.Tasty.Hedgehog (testProperty)
@@ -415,16 +414,14 @@
 testsWithConfig config =
   testGroup
     "moonlight-algebra"
-    [ lawSuiteGroup
-        "laws"
-        (renderLawBundles id (algebraLawBundles config)),
+    [ renderLawSuite (lawGroup "laws" (algebraLawSuites config)),
       representationBoundaryTests config,
       boolSemiringTests,
       latticeImplementationTests
     ]
 
-algebraLawBundles :: AlgebraGeneratorConfig -> [LawBundle String]
-algebraLawBundles config =
+algebraLawSuites :: AlgebraGeneratorConfig -> [LawSuite]
+algebraLawSuites config =
   let genFreeAbelianInt = genFreeAbelianGroup config (genIntBasis config)
       genAdditiveFreeAbelianInt = Additive <$> genFreeAbelianInt
       genAdditiveLaneVector = Additive <$> genLaneVector
@@ -435,87 +432,87 @@
       genPolynomialInteger = genPolynomial config genCoefficient
       genPowerSetAtom = genPowerSet config genAtom
       genSparseVecIntegerInt = genSparseVec config (genIntBasis config) genCoefficient
-   in [ lawBundleHedgehog
+   in [ lawGroup
           "additive-wrapper"
-          [ hedgehogLawDefinition MonoidAssoc (genTripleOf genAdditiveFreeAbelianInt) (applyTriple monoidAssoc),
-            hedgehogLawDefinition MonoidLeftId genAdditiveFreeAbelianInt monoidLeftId,
-            hedgehogLawDefinition MonoidRightId genAdditiveFreeAbelianInt monoidRightId,
-            hedgehogLawDefinition GroupInvLeft genAdditiveFreeAbelianInt groupInvLeft,
-            hedgehogLawDefinition GroupInvRight genAdditiveFreeAbelianInt groupInvRight,
-            hedgehogLawDefinition AbelianComm (genPairOf genAdditiveFreeAbelianInt) (applyPair abelianComm)
+          [ namedHedgehogLaw MonoidAssoc (genTripleOf genAdditiveFreeAbelianInt) (applyTriple monoidAssoc),
+            namedHedgehogLaw MonoidLeftId genAdditiveFreeAbelianInt monoidLeftId,
+            namedHedgehogLaw MonoidRightId genAdditiveFreeAbelianInt monoidRightId,
+            namedHedgehogLaw GroupInvLeft genAdditiveFreeAbelianInt groupInvLeft,
+            namedHedgehogLaw GroupInvRight genAdditiveFreeAbelianInt groupInvRight,
+            namedHedgehogLaw AbelianComm (genPairOf genAdditiveFreeAbelianInt) (applyPair abelianComm)
           ],
-        lawBundleHedgehog
+        lawGroup
           "lane-vector-additive"
-          [ hedgehogLawDefinition MonoidAssoc (genTripleOf genAdditiveLaneVector) (applyTriple laneVectorMonoidAssoc),
-            hedgehogLawDefinition MonoidLeftId genAdditiveLaneVector laneVectorMonoidLeftId,
-            hedgehogLawDefinition MonoidRightId genAdditiveLaneVector laneVectorMonoidRightId,
-            hedgehogLawDefinition GroupInvLeft genAdditiveLaneVector laneVectorGroupInvLeft,
-            hedgehogLawDefinition GroupInvRight genAdditiveLaneVector laneVectorGroupInvRight,
-            hedgehogLawDefinition AbelianComm (genPairOf genAdditiveLaneVector) (applyPair laneVectorAbelianComm),
-            hedgehogLawDefinition LaneVectorSubtraction (genPairOf genLaneVector) (applyPair laneVectorSubtraction)
+          [ namedHedgehogLaw MonoidAssoc (genTripleOf genAdditiveLaneVector) (applyTriple laneVectorMonoidAssoc),
+            namedHedgehogLaw MonoidLeftId genAdditiveLaneVector laneVectorMonoidLeftId,
+            namedHedgehogLaw MonoidRightId genAdditiveLaneVector laneVectorMonoidRightId,
+            namedHedgehogLaw GroupInvLeft genAdditiveLaneVector laneVectorGroupInvLeft,
+            namedHedgehogLaw GroupInvRight genAdditiveLaneVector laneVectorGroupInvRight,
+            namedHedgehogLaw AbelianComm (genPairOf genAdditiveLaneVector) (applyPair laneVectorAbelianComm),
+            namedHedgehogLaw LaneVectorSubtraction (genPairOf genLaneVector) (applyPair laneVectorSubtraction)
           ],
-        lawBundleHedgehog
+        lawGroup
           "free-monoid"
-          [ hedgehogLawDefinition FreeMonoidAssoc (genTripleOf genFreeMonoidInt) (applyTriple freeMonoidAssoc),
-            hedgehogLawDefinition FreeMonoidLeftId genFreeMonoidInt freeMonoidLeftId,
-            hedgehogLawDefinition FreeMonoidRightId genFreeMonoidInt freeMonoidRightId
+          [ namedHedgehogLaw FreeMonoidAssoc (genTripleOf genFreeMonoidInt) (applyTriple freeMonoidAssoc),
+            namedHedgehogLaw FreeMonoidLeftId genFreeMonoidInt freeMonoidLeftId,
+            namedHedgehogLaw FreeMonoidRightId genFreeMonoidInt freeMonoidRightId
           ],
-        lawBundleHedgehog
+        lawGroup
           "ring"
-          [ hedgehogLawDefinition RingAddAssoc (genTripleOf genZn7) (applyTriple ringAddAssoc),
-            hedgehogLawDefinition RingMulComm (genPairOf genZn7) (applyPair ringMulComm)
+          [ namedHedgehogLaw RingAddAssoc (genTripleOf genZn7) (applyTriple ringAddAssoc),
+            namedHedgehogLaw RingMulComm (genPairOf genZn7) (applyPair ringMulComm)
           ],
-        lawBundleHedgehog
+        lawGroup
           "lattice"
-          [ hedgehogLawDefinition (CommonLaw LatticeAbsorptionJoin) (genPairOf genPowerSetAtom) (applyPair latticeAbsorptionJoin),
-            hedgehogLawDefinition (CommonLaw LatticeAbsorptionMeet) (genPairOf genPowerSetAtom) (applyPair latticeAbsorptionMeet)
+          [ namedHedgehogLaw (CommonLaw LatticeAbsorptionJoin) (genPairOf genPowerSetAtom) (applyPair latticeAbsorptionJoin),
+            namedHedgehogLaw (CommonLaw LatticeAbsorptionMeet) (genPairOf genPowerSetAtom) (applyPair latticeAbsorptionMeet)
           ],
-        lawBundleHedgehog
+        lawGroup
           "heyting"
-          [ hedgehogLawDefinition HeytingImpliesSelfTop genPowerSetAtom heytingImpliesSelfTop,
-            hedgehogLawDefinition HeytingMeetImplication (genPairOf genPowerSetAtom) (applyPair heytingMeetImplication),
-            hedgehogLawDefinition HeytingConsequentMeetImplication (genPairOf genPowerSetAtom) (applyPair heytingConsequentMeetImplication),
-            hedgehogLawDefinition HeytingImplicationDistributesMeet (genTripleOf genPowerSetAtom) (applyTriple heytingImplicationDistributesMeet),
-            hedgehogLawDefinition HeytingNegDefault genPowerSetAtom heytingNegDefault,
-            hedgehogLawDefinition HeytingEquivalenceDefault (genPairOf genPowerSetAtom) (applyPair heytingEquivalenceDefault)
+          [ namedHedgehogLaw HeytingImpliesSelfTop genPowerSetAtom heytingImpliesSelfTop,
+            namedHedgehogLaw HeytingMeetImplication (genPairOf genPowerSetAtom) (applyPair heytingMeetImplication),
+            namedHedgehogLaw HeytingConsequentMeetImplication (genPairOf genPowerSetAtom) (applyPair heytingConsequentMeetImplication),
+            namedHedgehogLaw HeytingImplicationDistributesMeet (genTripleOf genPowerSetAtom) (applyTriple heytingImplicationDistributesMeet),
+            namedHedgehogLaw HeytingNegDefault genPowerSetAtom heytingNegDefault,
+            namedHedgehogLaw HeytingEquivalenceDefault (genPairOf genPowerSetAtom) (applyPair heytingEquivalenceDefault)
           ],
-        lawBundleHedgehog
+        lawGroup
           "module"
-          [ hedgehogLawDefinition ModuleDistribScalarAdd (genTriple genCoefficient genCoefficient genPolynomialInteger) (applyTriple moduleDistribScalarAdd),
-            hedgehogLawDefinition ModuleDistribVectorAdd (genTriple genCoefficient genPolynomialInteger genPolynomialInteger) (applyTriple moduleDistribVectorAdd)
+          [ namedHedgehogLaw ModuleDistribScalarAdd (genTriple genCoefficient genCoefficient genPolynomialInteger) (applyTriple moduleDistribScalarAdd),
+            namedHedgehogLaw ModuleDistribVectorAdd (genTriple genCoefficient genPolynomialInteger genPolynomialInteger) (applyTriple moduleDistribVectorAdd)
           ],
-        lawBundleHedgehog
+        lawGroup
           "unit"
-          [ hedgehogLawDefinition UnitInverseOne (pure ()) unitInverseOne,
-            hedgehogLawDefinition UnitInverseCorrect genIntegerUnit unitInverseCorrect,
-            hedgehogLawDefinition UnitInverseAbsent (genIntegerNonUnit config) unitInverseAbsent
+          [ namedHedgehogLaw UnitInverseOne (pure ()) unitInverseOne,
+            namedHedgehogLaw UnitInverseCorrect genIntegerUnit unitInverseCorrect,
+            namedHedgehogLaw UnitInverseAbsent (genIntegerNonUnit config) unitInverseAbsent
           ],
-        lawBundleHedgehog
+        lawGroup
           "gcd"
-          [ hedgehogLawDefinition GcdDividesLeft (genNonZeroGcdContext config) gcdDividesLeft,
-            hedgehogLawDefinition GcdDividesRight (genNonZeroGcdContext config) gcdDividesRight,
-            hedgehogLawDefinition ExtGcdBezout (genPairOf genInteger) (applyPair extGcdBezout),
-            hedgehogLawDefinition ModInverseCorrect (genModInverseContext isUnit config) modInverseCorrect,
-            hedgehogLawDefinition ModInverseAbsentNonunit (genModInverseContext (not . isUnit) config) modInverseAbsentNonunit,
-            hedgehogLawDefinition CrtSound (genCrtSoundContext config) crtSound
+          [ namedHedgehogLaw GcdDividesLeft (genNonZeroGcdContext config) gcdDividesLeft,
+            namedHedgehogLaw GcdDividesRight (genNonZeroGcdContext config) gcdDividesRight,
+            namedHedgehogLaw ExtGcdBezout (genPairOf genInteger) (applyPair extGcdBezout),
+            namedHedgehogLaw ModInverseCorrect (genModInverseContext isUnit config) modInverseCorrect,
+            namedHedgehogLaw ModInverseAbsentNonunit (genModInverseContext (not . isUnit) config) modInverseAbsentNonunit,
+            namedHedgehogLaw CrtSound (genCrtSoundContext config) crtSound
           ],
-        lawBundleHedgehog
+        lawGroup
           "canonicalization"
-          [ hedgehogLawDefinition PolynomialCanonicalizationIdempotent genPolynomialInteger polynomialCanonicalizationIdempotent
+          [ namedHedgehogLaw PolynomialCanonicalizationIdempotent genPolynomialInteger polynomialCanonicalizationIdempotent
           ],
-        lawBundleHedgehog
+        lawGroup
           "hedgehog-generators"
-          [ hedgehogLawDefinition ZnGeneratorNormalized genZn7 znGeneratorNormalized,
-            hedgehogLawDefinition PolynomialGeneratorCanonical genPolynomialInteger polynomialGeneratorCanonical,
-            hedgehogLawDefinition FreeAbelianGeneratorCanonical genFreeAbelianInt freeAbelianGeneratorCanonical,
-            hedgehogLawDefinition SparseVecGeneratorCanonical genSparseVecIntegerInt sparseVecGeneratorCanonical,
-            hedgehogLawDefinition PowerSetGeneratorCanonical genPowerSetAtom powerSetGeneratorCanonical
+          [ namedHedgehogLaw ZnGeneratorNormalized genZn7 znGeneratorNormalized,
+            namedHedgehogLaw PolynomialGeneratorCanonical genPolynomialInteger polynomialGeneratorCanonical,
+            namedHedgehogLaw FreeAbelianGeneratorCanonical genFreeAbelianInt freeAbelianGeneratorCanonical,
+            namedHedgehogLaw SparseVecGeneratorCanonical genSparseVecIntegerInt sparseVecGeneratorCanonical,
+            namedHedgehogLaw PowerSetGeneratorCanonical genPowerSetAtom powerSetGeneratorCanonical
           ],
-        lawBundleHedgehog
+        lawGroup
           "orientation"
-          [ hedgehogLawDefinition OrientationGroupInvLeft genOrientation orientationGroupInvLeft,
-            hedgehogLawDefinition OrientationGroupInvRight genOrientation orientationGroupInvRight,
-            hedgehogLawDefinition OrientationAbelianComm (genPairOf genOrientation) (applyPair orientationAbelianComm)
+          [ namedHedgehogLaw OrientationGroupInvLeft genOrientation orientationGroupInvLeft,
+            namedHedgehogLaw OrientationGroupInvRight genOrientation orientationGroupInvRight,
+            namedHedgehogLaw OrientationAbelianComm (genPairOf genOrientation) (applyPair orientationAbelianComm)
           ]
       ]
 
diff --git a/src-public/Moonlight/Algebra.hs b/src-public/Moonlight/Algebra.hs
--- a/src-public/Moonlight/Algebra.hs
+++ b/src-public/Moonlight/Algebra.hs
@@ -20,8 +20,9 @@
 * Free structures and actions — @FreeMonoid@, @FreeAbelianGroup@, @EndoPatch@,
   and monoid @Action@s with their invertible, group-acting refinement.
 * Lattices — join/meet semilattices up through distributive, Heyting and Boolean
-  algebras, and the two-element sign @Orientation@ group. Compiled finite
-  lattices live in the public @finite-lattice@ sublibrary, @Moonlight.FiniteLattice@.
+  algebras, quantales (commutative, residuated) with the Viterbi, Łukasiewicz
+  and tropical carriers, and the two-element sign @Orientation@ group. Compiled
+  finite lattices live in the public @finite-lattice@ sublibrary, @Moonlight.FiniteLattice@.
 * Rings and arithmetic — the semiring and commutative-ring laws extended with the
   @IntegralDomain@, @GCDDomain@ and @EuclideanDomain@ refinements, modular
   arithmetic (@Zn@), quotient rings @R/(n)@ (@Quotient@), @NumberTheory@ and @GCD@.
@@ -52,8 +53,9 @@
     module EndoPatch,
     -- * Actions
     module Action,
-    -- * Lattices and orientation
+    -- * Lattices, quantales and orientation
     module Lattice,
+    module Quantale,
     module Orientation,
     -- * Rings, modular arithmetic and number theory
     module Ring,
@@ -95,6 +97,7 @@
 import Moonlight.Algebra.Pure.Polynomial as Polynomial
 import Moonlight.Algebra.Pure.PowerSet as PowerSet
 import Moonlight.Algebra.Pure.Product as Product
+import Moonlight.Algebra.Pure.Quantale as Quantale
 import Moonlight.Algebra.Pure.Quotient as Quotient
 import Moonlight.Algebra.Pure.Ring as Ring
 import Moonlight.Algebra.Pure.SparseVec as SparseVec
diff --git a/test/abstract/AbstractTests.hs b/test/abstract/AbstractTests.hs
--- a/test/abstract/AbstractTests.hs
+++ b/test/abstract/AbstractTests.hs
@@ -5,6 +5,7 @@
 
 import Moonlight.Algebra.Effect.Laws qualified as EffectLaws
 import OrderedLatticeSpec qualified
+import QuantaleSpec qualified
 import SparseVecSpec qualified
 import Test.Tasty
   ( TestTree,
@@ -17,5 +18,6 @@
     "moonlight-algebra"
     [ EffectLaws.tests,
       OrderedLatticeSpec.tests,
+      QuantaleSpec.tests,
       SparseVecSpec.tests
     ]
diff --git a/test/abstract/Main.hs b/test/abstract/Main.hs
--- a/test/abstract/Main.hs
+++ b/test/abstract/Main.hs
@@ -1,8 +1,8 @@
 module Main (main) where
 
 import AbstractTests qualified
-import Moonlight.Pale.Test.Runner (runTestTree)
+import Test.Tasty (defaultMain)
 
 main :: IO ()
 main =
-  runTestTree AbstractTests.tests
+  defaultMain AbstractTests.tests
diff --git a/test/abstract/QuantaleSpec.hs b/test/abstract/QuantaleSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/abstract/QuantaleSpec.hs
@@ -0,0 +1,224 @@
+module QuantaleSpec
+  ( tests,
+  )
+where
+
+import Data.List (maximumBy)
+import Data.Ratio ((%))
+import Hedgehog qualified as HH
+import Hedgehog.Gen qualified as Gen
+import Hedgehog.Range qualified as Range
+import Moonlight.Algebra
+  ( BoundedJoinSemilattice (..),
+    ChainOrder (..),
+    ChainQuantale,
+    IntegralQuantale,
+    JoinSemilattice (..),
+    Quantale (..),
+    ResiduatedQuantale (..),
+    joinLeq,
+  )
+import Moonlight.Algebra
+  ( Lukasiewicz (..),
+    Tropical (..),
+    Viterbi (..),
+  )
+import Test.Tasty
+  ( TestTree,
+    testGroup,
+  )
+import Test.Tasty.Hedgehog
+  ( testProperty,
+  )
+
+tests :: TestTree
+tests =
+  testGroup
+    "quantale"
+    [ quantaleLawTests "Bool" Gen.bool,
+      quantaleLawTests "Viterbi Rational" genViterbiRational,
+      quantaleLawTests "Lukasiewicz Rational" genLukasiewiczRational,
+      quantaleLawTests "Tropical Rational" genTropicalRational,
+      quantaleLawTests "(Bool, Viterbi Rational)" genBoolViterbiPair,
+      testGroup
+        "integral markers"
+        [ integralQuantaleLawTests "Bool" Gen.bool,
+          integralQuantaleLawTests "Viterbi Rational" genViterbiRational,
+          integralQuantaleLawTests "Lukasiewicz Rational" genLukasiewiczRational,
+          integralQuantaleLawTests "(Bool, Viterbi Rational)" genBoolViterbiPair
+        ],
+      testGroup
+        "chain markers"
+        [ chainQuantaleLawTests "Bool" Gen.bool,
+          chainQuantaleLawTests "Viterbi Rational" genViterbiRational,
+          chainQuantaleLawTests "Lukasiewicz Rational" genLukasiewiczRational,
+          chainQuantaleLawTests "Tropical Rational (signed)" genTropicalSignedRational
+        ],
+      testGroup
+        "the chain order induced by a selective join"
+        [ chainOrderLawTests "Viterbi Rational" genViterbiRational,
+          chainOrderLawTests "Lukasiewicz Rational" genLukasiewiczRational,
+          chainOrderLawTests "Tropical Rational (signed)" genTropicalSignedRational
+        ]
+    ]
+
+quantaleLawTests ::
+  (ResiduatedQuantale carrier, Eq carrier, Show carrier) =>
+  String ->
+  HH.Gen carrier ->
+  TestTree
+quantaleLawTests label gen =
+  testGroup
+    label
+    [ testProperty "tensor is associative" $ HH.property $ do
+        left <- HH.forAll gen
+        middle <- HH.forAll gen
+        right <- HH.forAll gen
+        tensor (tensor left middle) right HH.=== tensor left (tensor middle right),
+      testProperty "tensorUnit is a left identity" $ HH.property $ do
+        value <- HH.forAll gen
+        tensor tensorUnit value HH.=== value,
+      testProperty "tensorUnit is a right identity" $ HH.property $ do
+        value <- HH.forAll gen
+        tensor value tensorUnit HH.=== value,
+      testProperty "tensor is commutative" $ HH.property $ do
+        left <- HH.forAll gen
+        right <- HH.forAll gen
+        tensor left right HH.=== tensor right left,
+      testProperty "tensor distributes over join on the left" $ HH.property $ do
+        left <- HH.forAll gen
+        middle <- HH.forAll gen
+        right <- HH.forAll gen
+        tensor left (join middle right)
+          HH.=== join (tensor left middle) (tensor left right),
+      testProperty "tensor distributes over join on the right" $ HH.property $ do
+        left <- HH.forAll gen
+        middle <- HH.forAll gen
+        right <- HH.forAll gen
+        tensor (join left middle) right
+          HH.=== join (tensor left right) (tensor middle right),
+      testProperty "bottom annihilates tensor on the left" $ HH.property $ do
+        value <- HH.forAll gen
+        tensor bottom value HH.=== bottom,
+      testProperty "bottom annihilates tensor on the right" $ HH.property $ do
+        value <- HH.forAll gen
+        tensor value bottom HH.=== bottom,
+      testProperty "residual is right adjoint to tensor" $ HH.property $ do
+        left <- HH.forAll gen
+        middle <- HH.forAll gen
+        right <- HH.forAll gen
+        joinLeq (tensor left middle) right HH.=== joinLeq left (residual middle right),
+      testProperty "tensorUnit is the greatest element" $ HH.property $ do
+        value <- HH.forAll gen
+        HH.assert (joinLeq value tensorUnit)
+    ]
+
+integralQuantaleLawTests ::
+  (IntegralQuantale carrier, Eq carrier, Show carrier) =>
+  String ->
+  HH.Gen carrier ->
+  TestTree
+integralQuantaleLawTests label gen =
+  testProperty (label <> ": tensor is two-sided deflationary") $ HH.property $ do
+    left <- HH.forAll gen
+    right <- HH.forAll gen
+    HH.assert (joinLeq (tensor left right) left)
+    HH.assert (joinLeq (tensor left right) right)
+
+chainQuantaleLawTests ::
+  (ChainQuantale carrier, Eq carrier, Show carrier) =>
+  String ->
+  HH.Gen carrier ->
+  TestTree
+chainQuantaleLawTests label gen =
+  testProperty (label <> ": join is selective") $ HH.property $ do
+    left <- HH.forAll gen
+    right <- HH.forAll gen
+    HH.assert (join left right == left || join left right == right)
+
+chainOrderLawTests ::
+  (ChainQuantale carrier, Eq carrier, Show carrier) =>
+  String ->
+  HH.Gen carrier ->
+  TestTree
+chainOrderLawTests label gen =
+  testGroup
+    label
+    [ testProperty "strict ascent is the lattice order minus equality" $ HH.property $ do
+        left <- HH.forAll gen
+        right <- HH.forAll gen
+        (compare (ChainOrder left) (ChainOrder right) == LT)
+          HH.=== (joinLeq left right && left /= right),
+      testProperty "the order is antisymmetric" $ HH.property $ do
+        left <- HH.forAll gen
+        right <- HH.forAll gen
+        compare (ChainOrder left) (ChainOrder left) HH.=== EQ
+        (chainOrderLeq left right && chainOrderLeq right left)
+          HH.=== (left == right),
+      testProperty "the order is transitive" $ HH.property $ do
+        left <- HH.forAll gen
+        middle <- HH.forAll gen
+        right <- HH.forAll gen
+        let triple = [left, middle, right]
+        HH.assert
+          ( and
+              [ not (chainOrderLeq lower between && chainOrderLeq between upper)
+                  || chainOrderLeq lower upper
+              | lower <- triple,
+                between <- triple,
+                upper <- triple
+              ]
+          ),
+      testProperty "the greatest element under the order attains the join" $ HH.property $ do
+        values <- HH.forAll (Gen.list (Range.linear 1 12) gen)
+        getChainOrder (maximumBy compare (map ChainOrder values))
+          HH.=== foldr1 join values
+    ]
+  where
+    chainOrderLeq :: (ChainQuantale value, Eq value) => value -> value -> Bool
+    chainOrderLeq lower upper =
+      compare (ChainOrder lower) (ChainOrder upper) /= GT
+
+genUnitIntervalRational :: HH.Gen Rational
+genUnitIntervalRational = do
+  denominator <- Gen.integral (Range.linear 1 12)
+  numerator <- Gen.integral (Range.linear 0 denominator)
+  pure (numerator % denominator)
+
+genViterbiRational :: HH.Gen (Viterbi Rational)
+genViterbiRational =
+  Viterbi <$> genUnitIntervalRational
+
+genLukasiewiczRational :: HH.Gen (Lukasiewicz Rational)
+genLukasiewiczRational =
+  Lukasiewicz <$> genUnitIntervalRational
+
+genTropicalRational :: HH.Gen (Tropical Rational)
+genTropicalRational =
+  Gen.frequency
+    [ (1, pure TropicalInfinity),
+      (6, TropicalFinite <$> genNonnegativeRational)
+    ]
+
+genTropicalSignedRational :: HH.Gen (Tropical Rational)
+genTropicalSignedRational =
+  Gen.frequency
+    [ (1, pure TropicalInfinity),
+      (6, TropicalFinite <$> genSignedRational)
+    ]
+
+genSignedRational :: HH.Gen Rational
+genSignedRational = do
+  denominator <- Gen.integral (Range.linear 1 12)
+  numerator <- Gen.integral (Range.linearFrom 0 (-12 * denominator) (12 * denominator))
+  pure (numerator % denominator)
+
+genNonnegativeRational :: HH.Gen Rational
+genNonnegativeRational = do
+  denominator <- Gen.integral (Range.linear 1 12)
+  numerator <- Gen.integral (Range.linear 0 (12 * denominator))
+  pure (numerator % denominator)
+
+genBoolViterbiPair :: HH.Gen (Bool, Viterbi Rational)
+genBoolViterbiPair =
+  (,) <$> Gen.bool <*> genViterbiRational
diff --git a/test/aggregate/Main.hs b/test/aggregate/Main.hs
deleted file mode 100644
--- a/test/aggregate/Main.hs
+++ /dev/null
@@ -1,13 +0,0 @@
-module Main (main) where
-
-import AbstractTests qualified
-import FiniteLatticeTests qualified
-import Moonlight.Pale.Test.Runner (runTestTreeGroup)
-
-main :: IO ()
-main =
-  runTestTreeGroup
-    "moonlight-algebra"
-    [ AbstractTests.tests,
-      FiniteLatticeTests.tests
-    ]
diff --git a/test/coherence/Main.hs b/test/coherence/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/coherence/Main.hs
@@ -0,0 +1,10 @@
+-- | Compile both focused test sections against their dependency union. Empty
+-- imports retain module and instance coherence without executing the focused
+-- behavioral suites a second time.
+module Main (main) where
+
+import AbstractTests ()
+import FiniteLatticeTests ()
+
+main :: IO ()
+main = pure ()
diff --git a/test/finite-lattice/Main.hs b/test/finite-lattice/Main.hs
--- a/test/finite-lattice/Main.hs
+++ b/test/finite-lattice/Main.hs
@@ -1,8 +1,8 @@
 module Main (main) where
 
 import FiniteLatticeTests qualified
-import Moonlight.Pale.Test.Runner (runTestTree)
+import Test.Tasty (defaultMain)
 
 main :: IO ()
 main =
-  runTestTree FiniteLatticeTests.tests
+  defaultMain FiniteLatticeTests.tests