diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,6 +1,17 @@
 # Changelog
 
-## 0.1.0.0 - unreleased
+## 0.1.0.1 - 2026-07-22
+
+- Documentation: the public `finite-lattice` sublibrary front door
+  `Moonlight.FiniteLattice` now carries a full module-header overview and worked
+  recipes — quick-start lattice construction, Heyting implication, least and
+  greatest fixpoints, and the resident fast path.
+- README reduced to a dependency/module map and build tooling; the tower's
+  shape, contract, and cookbook now live once, in the module headers.
+- Removed a stale `extra-doc-files` reference left by an earlier surface
+  consolidation.
+
+## 0.1.0.0
 
 - Initial release of the Level-1 algebraic tower over `moonlight-core`.
 - Group surface: standard `Semigroup`/`Monoid`, `Group`, `AbelianGroup`, and
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -5,170 +5,11 @@
 
 The law-governed algebraic tower the rest of the cathedral stands on.
 
-`moonlight-algebra` is Moonlight's algebraic tier. Building on
-[`moonlight-core`](../moonlight-core), it supplies a tower of
-pure, law-governed algebraic structures: standard semigroups/monoids with
-operation-selecting additive and multiplicative wrappers, group refinements, the
-lattice hierarchy up to Heyting and Boolean algebras, integral/GCD/Euclidean
-domain refinements, modules and vector spaces, modular arithmetic, number
-theory, free structures, and sparse vectors. Each structure is a thin type
-class or newtype boundary; its laws are stated in the module header and
-exercised by the private law-suite sublibrary.
-
-## Relationship to `moonlight-core`
-
-`moonlight-core` owns the operation-bearing numeric tower: `AdditiveMonoid`,
-`AdditiveGroup`, `MultiplicativeMonoid`, `Semiring`, `Ring`, `CommutativeRing`,
-and `Field`. `Moonlight.Algebra.Pure.Ring` re-exports the law-only semiring and
-commutative-ring classes from core and adds only the stronger domain refinements:
-`IntegralDomain`, `GCDDomain`, `EuclideanDomain`, and
-`CanonicalEuclideanDomain`. There is one arithmetic vocabulary; the ring layer
-reuses core's `zero`, `one`, `add`, and `mul`.
-
-## What it provides
-
-- **Groups, free structures and actions.** Standard `Semigroup`/`Monoid`,
-  `Group`/`AbelianGroup` law refinements, `Additive` and `Multiplicative`
-  wrappers for carriers with several lawful operations, free monoids and free
-  abelian groups, the two-element sign/orientation group (ℤ/2), and monoid
-  actions on a carrier with a group-acting refinement.
-- **The lattice hierarchy.** Join/meet semilattices up to Heyting and Boolean
-  algebras. Compiled finite lattices live in the public
-  `moonlight-algebra:finite-lattice` sublibrary.
-- **Rings and arithmetic.** Semiring → commutative ring → integral/GCD/Euclidean
-  domains; modular arithmetic (`Zn`); quotient rings `R/(n)` of a Euclidean
-  domain; number theory and gcd; and univariate polynomials over a coefficient
-  ring (Horner evaluation, a free module on monomial degrees).
-- **Modules and magnitudes.** Modules, free modules, vector spaces, bilinear
-  spaces over a field, and real-valued magnitudes for obstructions.
-- **Constructions.** Power-set lattices, finite *n*-fold product algebras with
-  coordinatewise structure, quotients, and sparse vectors with finite support.
-
-## Tiny usage examples
-
-```haskell
-import Moonlight.Algebra.Pure.Group
-
-difference :: Additive Integer
-difference = groupDifference (Additive 3) (Additive 5)
-
-product :: Multiplicative Integer
-product = Multiplicative 3 <> Multiplicative 5
-```
-
-Sparse kernels:
-
-```haskell
-compiled = compileSparseLinearMap 128 (\i -> [(i, 1), (i + 1, 2)])
-
-combined = add (fromEntries [('x', 2)]) (fromEntries [('x', 3), ('y', 1)])
-```
-
-## Finite lattices
-
-This public sublibrary owns checked finite-order compilation and the dense
-runtime views inside `moonlight-algebra`: `ContextLattice`, dense join/meet/`<=`
-plans, resident branded keys, Heyting implication, least/greatest fixpoints,
-cover edges, presentation builders, and generator support kernels.
-
-The main `moonlight-algebra` library remains the abstract algebra class tower.
-The `finite-lattice` sublibrary is the finite, validated, queryable realization
-of a lattice over a declared closed universe.
-
-### Quick start
-
-Declare a finite order by name binding. `latticeOf` infers the unique top and
-bottom, transitively closes the order, derives join and meet, and proves
-lattice-hood, returning a compiled `ContextLattice` or the first obstruction it
-finds.
-
-```haskell
-import Moonlight.FiniteLattice
-
-data Context = Bottom | West | East | Top
-  deriving (Eq, Ord, Show)
-
-diamond :: Either (LatticeBuildError Context) (ContextLattice Context)
-diamond =
-  latticeOf $ do
-    [bottom, west, east, top] <- elements [Bottom, West, East, Top]
-    below bottom west
-    below bottom east
-    below west top
-    below east top
-```
-
-`West` and `East` are incomparable; their least upper bound and greatest lower
-bound are derived from the order alone. On the compiled lattice, order, join and
-meet are total, checked lookups into the dense plan:
-
-```
->>> Right lattice = diamond
->>> joinContext lattice West East
-Right Top
->>> meetContext lattice West East
-Right Bottom
->>> leqContext lattice Bottom Top
-Right True
-```
-
-### Heyting implication
-
-The diamond is distributive, so it carries a Heyting structure. `compileContextHeyting`
-builds the residual plan once; `impliesContext` is then the relative pseudocomplement:
-the largest `x` with `antecedent ∧ x ≤ consequent`.
-
-```
->>> Right heyting = compileContextHeyting lattice
->>> impliesContext heyting West East
-Right East
->>> impliesContext heyting West West
-Right Top
-```
-
-### Least and greatest fixpoints
-
-Every monotone endomap on the lattice has a least and a greatest fixpoint
-(Knaster–Tarski). `leastContextFixpoint` climbs up from the bottom, `greatestContextFixpoint`
-descends from the top; a non-monotone step is rejected as a typed `ContextMonotoneMapError`.
-
-```haskell
-settle :: Context -> Context
-settle Bottom = West
-settle West   = West
-settle East   = Top
-settle Top    = Top
-```
-
-```
->>> leastContextFixpoint lattice settle
-Right West
->>> greatestContextFixpoint lattice settle
-Right Top
-```
-
-### The resident fast path
-
-`joinContext`, `meetContext`, and `impliesContext` resolve each domain value through a map
-on every call. When you sweep many queries, resolve once: `withResidentContext` hands you
-branded keys whose order, join, and meet are pure array indexing without per-query
-lookup inside the loop.
-
-```haskell
-leqRelationSize :: ContextLattice Context -> Int
-leqRelationSize lattice =
-  withResidentContext lattice $ \ctx ->
-    let keys = residentContextKeys ctx
-     in length [() | a <- keys, b <- keys, residentContextKeyLeq ctx a b]
-```
-
-```
->>> leqRelationSize lattice
-9
-```
-
-The count is the size of the `≤` relation: four reflexive pairs, plus `Bottom` under
-`West`, `East`, and `Top`, plus `West` and `East` each under `Top`.
+`moonlight-algebra` is Moonlight's algebraic tier, building on
+[`moonlight-core`](../moonlight-core). The front door is the umbrella module
+`Moonlight.Algebra`, whose header carries the tower's shape and its relationship
+to core; the public `finite-lattice` sublibrary has its own front door,
+`Moonlight.FiniteLattice`, whose header carries the compiled-lattice cookbook.
 
 ## Public modules
 
diff --git a/docs/finite-lattice/CHANGELOG.md b/docs/finite-lattice/CHANGELOG.md
deleted file mode 100644
--- a/docs/finite-lattice/CHANGELOG.md
+++ /dev/null
@@ -1,9 +0,0 @@
-# Changelog
-
-## 0.1.0.0 - unreleased
-
-- Initial release of the compiled finite context lattice public sublibrary
-  inside `moonlight-algebra`.
-- Owns checked context-order compilation, dense join/meet/order plans, cover
-  edges, Heyting implication, finite fixpoint iteration, resident branded keys,
-  support bases, and finite lattice presentation builders.
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.0
+version:             0.1.0.1
 homepage:            https://github.com/PaleRoses/moonlight
 bug-reports:         https://github.com/PaleRoses/moonlight/issues
 synopsis:            Algebraic type class tower for Pale Meridian.
@@ -9,13 +9,13 @@
 license-file:        LICENSE
 author:              Blue Rose
 maintainer:          rosaliafialkova@gmail.com
+copyright:           (c) 2026 Blue Rose
 category:            Math
 build-type:          Simple
 tested-with:         GHC == 9.14.1
 extra-doc-files:
   README.md
   CHANGELOG.md
-  docs/finite-lattice/CHANGELOG.md
   docs/finite-lattice/BENCHMARKS-m4-pro.md
 
 source-repository head
diff --git a/src-finite-lattice/Moonlight/FiniteLattice.hs b/src-finite-lattice/Moonlight/FiniteLattice.hs
--- a/src-finite-lattice/Moonlight/FiniteLattice.hs
+++ b/src-finite-lattice/Moonlight/FiniteLattice.hs
@@ -1,5 +1,88 @@
 {-# LANGUAGE GHC2024 #-}
 
+{-|
+The finite, validated, queryable realization of a lattice over a declared closed
+universe — the public @finite-lattice@ face of @moonlight-algebra@. Where the
+main library is the abstract algebra class tower, this sublibrary is checked
+finite-order compilation and the dense runtime views: @ContextLattice@, dense
+join\/meet\/@<=@ plans, resident branded keys, Heyting implication, least and
+greatest fixpoints, cover edges, presentation builders, and generator support.
+
+/Quick start./ Declare a finite order by name binding; @latticeOf@ infers the
+unique top and bottom, transitively closes the order, derives join and meet, and
+proves lattice-hood, returning a compiled @ContextLattice@ or the first
+obstruction it finds.
+
+> import Moonlight.FiniteLattice
+>
+> data Context = Bottom | West | East | Top
+>   deriving (Eq, Ord, Show)
+>
+> diamond :: Either (LatticeBuildError Context) (ContextLattice Context)
+> diamond =
+>   latticeOf $ do
+>     [bottom, west, east, top] <- elements [Bottom, West, East, Top]
+>     below bottom west
+>     below bottom east
+>     below west top
+>     below east top
+
+@West@ and @East@ are incomparable; their least upper bound and greatest lower
+bound are derived from the order alone. On the compiled lattice, order, join and
+meet are total, checked lookups into the dense plan:
+
+>>> Right lattice = diamond
+>>> joinContext lattice West East
+Right Top
+>>> meetContext lattice West East
+Right Bottom
+>>> leqContext lattice Bottom Top
+Right True
+
+/Heyting implication./ The diamond is distributive, so it carries a Heyting
+structure. @compileContextHeyting@ builds the residual plan once; @impliesContext@
+is then the relative pseudocomplement: the largest @x@ with
+@antecedent ∧ x ≤ consequent@.
+
+>>> Right heyting = compileContextHeyting lattice
+>>> impliesContext heyting West East
+Right East
+>>> impliesContext heyting West West
+Right Top
+
+/Least and greatest fixpoints./ Every monotone endomap has a least and a greatest
+fixpoint (Knaster–Tarski). @leastContextFixpoint@ climbs from the bottom,
+@greatestContextFixpoint@ descends from the top; a non-monotone step is rejected
+as a typed @ContextMonotoneMapError@.
+
+> settle :: Context -> Context
+> settle Bottom = West
+> settle West   = West
+> settle East   = Top
+> settle Top    = Top
+
+>>> leastContextFixpoint lattice settle
+Right West
+>>> greatestContextFixpoint lattice settle
+Right Top
+
+/The resident fast path./ @joinContext@, @meetContext@ and @impliesContext@
+resolve each domain value through a map on every call. To sweep many queries,
+resolve once: @withResidentContext@ hands you branded keys whose order, join and
+meet are pure array indexing with no per-query lookup inside the loop.
+
+> leqRelationSize :: ContextLattice Context -> Int
+> leqRelationSize lattice =
+>   withResidentContext lattice $ \ctx ->
+>     let keys = residentContextKeys ctx
+>      in length [() | a <- keys, b <- keys, residentContextKeyLeq ctx a b]
+
+>>> leqRelationSize lattice
+9
+
+The count is the size of the @≤@ relation: four reflexive pairs, plus @Bottom@
+under @West@, @East@ and @Top@, plus @West@ and @East@ each under @Top@.
+-}
 module Moonlight.FiniteLattice
   ( module Moonlight.FiniteLattice.Core,
     module Moonlight.FiniteLattice.Resident,
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
@@ -1,7 +1,46 @@
 {-|
-Convenience re-export of the whole "Moonlight.Algebra.Pure" tower as a single
-import. For finer-grained control, import the individual @Moonlight.Algebra.Pure.*@
-modules directly.
+The single import of the @moonlight-algebra@ tower: the named structures of
+abstract algebra — groups, lattices, rings and their domains, modules and
+polynomials — as law-governed classes and concrete carriers layered over
+"Moonlight.Core". Each structure is a thin class or newtype boundary whose laws
+are stated in its own module and machine-checked in the law suite.
+
+The operation-bearing numeric classes — @AdditiveMonoid@, @AdditiveGroup@,
+@MultiplicativeMonoid@, @Semiring@, @Ring@, @Field@ — are owned by
+"Moonlight.Core" and re-exported here; @moonlight-algebra@ adds the stronger
+refinements, the concrete carriers, and the constructions, reusing core's
+@zero@, @one@, @add@ and @mul@ rather than defining a second arithmetic.
+
+For finer control, import the individual @Moonlight.Algebra.Pure.*@ modules
+directly. The re-exported tower, by family:
+
+* Groups — standard @Semigroup@/@Monoid@, the @Group@/@AbelianGroup@ refinements,
+  the operation-selecting @Additive@/@Multiplicative@ wrappers, and @LaneVector@,
+  a 16-lane @Word64@ abelian group.
+* 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@.
+* 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@.
+* Modules and magnitude — @Module@, free modules, vector and bilinear spaces over
+  a field, and real-valued @Magnitude@ for obstructions.
+* Polynomials — univariate @Polynomial@s over a coefficient ring, a free module
+  on monomial degrees.
+* Constructions — @PowerSet@ lattices, finite n-fold @Product@ algebras with
+  coordinatewise structure, and @SparseVec@ with finite support.
+
+The laws are named and exercised in the private law-suite sublibrary, not
+restated here; each module's Haddock carries its signatures.
+
+The operation-selecting wrappers, in one example:
+
+> import Moonlight.Algebra
+>
+> Additive 3 <> Additive 5              -- Additive 8         (<> selects +)
+> Multiplicative 3 <> Multiplicative 5  -- Multiplicative 15  (<> selects *)
 -}
 module Moonlight.Algebra
   ( -- * Standard semigroups, monoids and groups