diff --git a/trees/fcap-000T.tree b/trees/fcap-000T.tree
index ad5cff18..d8faf7a7 100644
--- a/trees/fcap-000T.tree
+++ b/trees/fcap-000T.tree
@@ -8,6 +8,6 @@
 \taxon{Remark}
 \title{Infinitesimal and global Clifford symmetry}
 
-\p{The quadratic Clifford Lie algebra is the infinitesimal part of the same conjugation action that produces reflections. Kostant proves that #{\bigwedge^2V=\operatorname{Lie}(\Spin(V))}, that its map to #{\mathfrak{so}(V)} is the differential of #{\Spin(V)\to SO(V)}, and that its commutator action extends as the corresponding derivation of the exterior algebra \citet{Section 2.4, Theorem 8, pp. 286--287}{kostant1997clifford}. Chevalley obtains the same two-vector Lie algebra inside the Clifford group \citet{II.2.9, pp. 67--68}{chevalley1954algebraic}.}
+\p{The quadratic Clifford Lie algebra is the infinitesimal part of the same conjugation action that produces reflections. Kostant proves that #{\bigwedge^2V=\operatorname{Lie}(\Spin(V))}, that its map to #{\mathfrak{so}(V)} is the differential of #{\Spin(V)\to SO(V)}, and that its commutator action extends as the corresponding derivation of the exterior algebra \citet{Section 2.4, Theorem 8, pp. 286--287}{kostant1997clifford}. Chevalley obtains the same two-vector Lie algebra inside the Clifford group \citet{Chapter II, Section 2.9, pp. 67--68}{chevalley1954algebraic}.}
 
-\p{The cards above identify the algebraic Lie layer. They do not construct Lie-group structures or identify a differential of a Lie-group covering map. The next chapter instead reaches the global orthogonal group by finite products of reflections.}
+\p{The results above identify the relevant Lie algebras. Constructing the Lie-group structures and identifying the differential of a covering homomorphism require additional arguments. The next chapter reaches the orthogonal group by finite products of reflections.}
diff --git a/trees/fcap-0010.tree b/trees/fcap-0010.tree
index 6011cc51..705bb737 100644
--- a/trees/fcap-0010.tree
+++ b/trees/fcap-0010.tree
@@ -11,8 +11,8 @@
 that plane tensors the Clifford algebra with two-by-two real matrices.
 Iteration removes the common part of a real signature, while a sign switch
 gives a complementary one-sided recurrence. These are algebraic steps toward
-the real classification; the real Pin and Spin groups follow a separate
-branch through the double-cover theory.}
+the real classification. The real Pin and Spin groups are instead constructed
+using the double-cover theory.}
 
 \related{\ref{ca-0001}}
 
diff --git a/trees/fcap-0011.tree b/trees/fcap-0011.tree
index 79590b1c..033627c9 100644
--- a/trees/fcap-0011.tree
+++ b/trees/fcap-0011.tree
@@ -6,7 +6,7 @@
 \tag{clifford}
 
 \taxon{Convention}
-\title{Real signature and Clifford signs \citet{II.2.9, pp. 65--66}{chevalley1954algebraic}}
+\title{Real signature and Clifford signs \citet{Chapter II, Section 2.9, pp. 65--66}{chevalley1954algebraic}}
 \lean/tauceti{TauCeti.realCliffordForm,TauCeti.realCliffordForm_apply}
 
 \p{For #{p,q\ge0}, put
diff --git a/trees/fcap-0014.tree b/trees/fcap-0014.tree
index 216be5ae..ce3775c1 100644
--- a/trees/fcap-0014.tree
+++ b/trees/fcap-0014.tree
@@ -6,7 +6,7 @@
 \tag{clifford}
 
 \taxon{Lemma}
-\title{Finite hyperbolic reduction \citet{II.2.9, pp. 65--66}{chevalley1954algebraic}}
+\title{Finite hyperbolic reduction \citet{Chapter II, Section 2.9, pp. 65--66}{chevalley1954algebraic}}
 \lean/tauceti{TauCeti.realCliffordBottIterEquiv,TauCeti.realCliffordSignatureReductionEquiv}
 
 \p{Chevalley splits a finite-dimensional real quadratic space into hyperbolic planes and a definite remainder. TauCeti combines that classical reduction with iteration of \ref{fcap-0013} and Kronecker equivalences to synthesize the explicit tensor and matrix packaging below. Iterating #{n} times gives
diff --git a/trees/fcap-0019.tree b/trees/fcap-0019.tree
index 36c1637b..1836f20a 100644
--- a/trees/fcap-0019.tree
+++ b/trees/fcap-0019.tree
@@ -7,16 +7,16 @@
 
 \title{Spin-representation roadmap}
 
-\p{This appendix follows the mathematical dependencies of the
+\p{This appendix follows the mathematics in the
 \href{https://github.com/TauCetiProject/TauCetiRoadmap/tree/main/TauCetiRoadmap/RepresentationTheory/SpinRepresentations}{spin-representation roadmap}
-of \href{https://github.com/TauCetiProject/TauCeti}{Tau Ceti}. The filtered
-Clifford algebra first exposes its exterior shadow. Reflections then lead to
-the global Pin and Spin extensions, while bivectors provide the algebraic
-infinitesimal orthogonal action. The Lie functor records the separate
-differential bridge from smooth group homomorphisms. A polarization joins the
-algebraic group and Lie constructions in the exterior spinor model. The
-real-signature recurrence and classification form a parallel algebraic branch
-and do not depend on the spinor-module or double-cover join.}
+of \href{https://github.com/TauCetiProject/TauCeti}{Tau Ceti}. The associated
+graded algebra of the filtered Clifford algebra is an exterior algebra.
+Reflections give the Pin and Spin extensions, while bivectors give the
+infinitesimal orthogonal action. Differentiating smooth group homomorphisms
+gives the Lie functor. A polarization equips the exterior algebra with its
+Clifford and Spin actions. The real Clifford classification follows from the
+hyperbolic and one-sided recurrences together with the real base cases. These
+Clifford-algebra calculations supply all the inputs to its proof.}
 
 \transclude{fcap-000F}
 
diff --git a/trees/fcap-001F.tree b/trees/fcap-001F.tree
index 3c9797e0..3f4b1a61 100644
--- a/trees/fcap-001F.tree
+++ b/trees/fcap-001F.tree
@@ -23,4 +23,4 @@ a general field and that square roots for all field elements suffice to
 normalize lifts. TauCeti's generic theorem instead assumes a field, a
 nontrivial finite-dimensional module, invertible #{2}, a nondegenerate
 quadratic form, and an explicit surjectivity proof. Its separably closed
-specialization obtains that proof from the formal Cartan--Dieudonne route.}
+specialization obtains that proof from the formalized Cartan--Dieudonne theorem.}
diff --git a/trees/fcap-001Q.tree b/trees/fcap-001Q.tree
index 16979ba5..3bfdad7c 100644
--- a/trees/fcap-001Q.tree
+++ b/trees/fcap-001Q.tree
@@ -8,11 +8,10 @@
 \title{Differentiating smooth group homomorphisms}
 
 \p{The quadratic Clifford construction in the preceding section is
-algebraic. A different bridge starts from a smooth homomorphism of Lie groups
-and differentiates it at the identity. This produces the functor from Lie
-groups to Lie algebras and explains which part of the Spin-representation
-roadmap is generic differential geometry, before any Lie-group structure on
-the abstract Spin and special orthogonal groups has been supplied.}
+algebraic. Separately, differentiating a smooth homomorphism of Lie groups at
+the identity produces a homomorphism of their Lie algebras. This defines the
+Lie functor before any Lie-group structure on the abstract Spin and special
+orthogonal groups has been supplied.}
 
 \transclude{fcap-001R}
 \transclude{fcap-001S}
diff --git a/trees/fcap-001W.tree b/trees/fcap-001W.tree
index 002ecf91..6f941114 100644
--- a/trees/fcap-001W.tree
+++ b/trees/fcap-001W.tree
@@ -6,18 +6,16 @@
 \tag{lie}
 
 \taxon{Remark}
-\title{Why explicit smoothness changes the roadmap
+\title{Smooth homomorphisms and automatic smoothness
 \citet{Sections 2.1--2.4 and 2.8, pp. 9--13, 19--20}{liu2016lie};
 \citet{Section 3.1.2, pp. 106--107}{isaev2018theory}}
 
 \p{The constructions in \ref{fcap-001R}--\ref{fcap-001V} start with a
 smooth homomorphism. Their tangent map, bracket law, functor laws, and
-exponential naturality therefore do not require a theorem that upgrades a
-continuous homomorphism to a smooth one. The generic theorem does not invoke
-the closed-subgroup theorem; that theorem belongs to the later specialization
-to concrete matrix subgroups. This is the dependency split proposed in
-\href{https://github.com/TauCetiProject/TauCetiRoadmap/pull/224}{TauCetiRoadmap
-PR 224}.}
+exponential naturality use the differential geometry of smooth maps. The
+automatic-smoothness theorem is needed when the homomorphism is only known to
+be continuous. The closed-subgroup theorem is needed when a closed matrix
+subgroup must first be given a Lie-group structure.}
 
 \p{The exponential input is separate from the tangent and bracket input.
 Likewise, the Baker--Campbell--Hausdorff calculation can first be made in a
diff --git a/trees/fcap-001Y.tree b/trees/fcap-001Y.tree
index be70772f..2d56a4c9 100644
--- a/trees/fcap-001Y.tree
+++ b/trees/fcap-001Y.tree
@@ -6,22 +6,16 @@
 \tag{clifford}
 
 \taxon{Remark}
-\title{Why algebraic periodicity is a separate branch
-\citet{II.2.1, II.2.5, and II.2.9, pp. 42--46, 65--66}{chevalley1954algebraic};
+\title{Algebraic periodicity and real Pin and Spin groups
+\citet{II.2.1 and II.2.5, pp. 42--46; Chapter II, Section 2.9, pp. 65--66}{chevalley1954algebraic};
 \citet{I.4, Theorems 4.1 and 4.3, pp. 25--29}{lawson2016spin}}
 
 \p{The recurrences in \ref{fcap-0013}, \ref{fcap-0014}, and
 \ref{fcap-001X} use Clifford universal properties, orthogonal sums, tensor
-products, coordinate isometries, and the real base entries. They do not use
-the Spin representation, the structure theorem obtained from a spinor
-module, or the Pin and Spin double covers. This is the algebraic branch of
-Layer 7.}
+products, coordinate isometries, and the real base entries.}
 
-\p{The real groups #{\Pin(p,q)} and #{\Spin(p,q)} form a different branch.
-Their actions, kernels, and algebraic extensions specialize the group theory
-developed in \ref{fcap-0007}, and therefore genuinely consume the Layer-2
-Pin/Spin work. The distinction between these branches is the dependency
-correction proposed in
-\href{https://github.com/TauCetiProject/TauCetiRoadmap/pull/225}{TauCetiRoadmap
-PR 225}. It changes the order in which the mathematics can be built; it does
-not turn the roadmap proposal itself into a formal theorem.}
+\p{The construction of the real groups #{\Pin(p,q)} and #{\Spin(p,q)} instead
+specializes the actions, kernels, and algebraic
+extensions developed in \ref{fcap-0007}. Thus the real Clifford
+classification can be proved from Clifford-algebra calculations before these
+group extensions are available.}