diff --git a/kadison_kaplansky_projection_counter_v2.txt b/kadison_kaplansky_projection_counter_v2.txt
index 286e5e7..17f6884 100644
--- a/kadison_kaplansky_projection_counter_v2.txt
+++ b/kadison_kaplansky_projection_counter_v2.txt
@@ -747,10 +747,16 @@ number, bucket, x).
 UNIQUE LONG PATHS.  If two nonbacktracking paths of length at
 least L_i end or begin at a vertex in layer i, and they read the
 same oriented word in a fixed finite alphabet, they coincide as
-paths.  Reason: the triangular equations propagate bit by bit,
-and the block recovery above covers the first half of the path;
-the gated structure past the end lets the remaining bits be read
-off.
+paths.  Reason in one line: the triangular equations of 6.4
+propagate bit by bit along the common word, and the "gate" data
+included in each label records the block state sufficiently far
+back that a wrong start cannot reproduce the word.
+
+The full proof of this is deferred to the pruning section of
+6.7 (the "prefix-recovery" lemma), where the gated deletion
+rule and the two-layer comparison are laid out.  Nothing
+in 6.5 is used later except the conclusion; the machinery lives
+in 6.7.
 
 6.6  THE TWO GRAPHS Y^0 AND Y^#.
 
@@ -1533,7 +1539,7 @@ lemma.
 We want a FINITE list of coefficient templates, uniform in the
 layer index.  Two replacements make this possible.
 
-COMPACT SUPPORT.  Lemma nil:templates (Part 7) says: J_epsilon
+COMPACT SUPPORT.  the compactness result of Part 7 (Part 7) says: J_epsilon
 can be replaced by compactly supported smooth J_epsilon^flat at
 arbitrarily small L^1 coefficient cost, uniformly in the
 lattice mesh, for small enough ell.
@@ -1880,22 +1886,42 @@ cancellations actual, and the remaining nonempty cyclic path
 would contradict the girth hypothesis (2^C_* = 10^4 > 5000).
 So each bounded face has at least 20 arcs.
 
-EULER COUNT.  Let b be the number of arcs and M_mark be the
-number of marked vertices.  A plane Euler formula b = v + J - 1
-with each unmarked vertex of degree >= 3 gives
+EULER COUNT.  Write v for the number of vertices (marked plus
+unmarked) and b for the number of arcs.  Plane Euler gives
+v - b + (J + 1) = 2, i.e. b = v + J - 1.  Count the ends of
+every arc in two ways.  Each arc has two ends, so the sum of
+all face lengths is 2b; only bounded faces are counted, and
+each has at least 20 arcs by FACE CYCLE, so 20J <= 2b.  Each
+unmarked vertex has degree at least 3 after suppression by
+(R3), so summing degrees over unmarked vertices gives
+3(v - M_mark) <= 2b.  Substituting v = b - J + 1:
 
-   20 J  <=  2 b,       b  <=  3 J + 3 M_mark - 3,
-   b  <=  6 M_mark.
+   3(b - J + 1 - M_mark)  <=  2b,   so
+   b  <=  3 J + 3 M_mark - 3.
 
-INJECTIVITY.  Take an injectivity failure with M_mark = 1.
-The two inequalities 20J <= 2b and b <= 6 give
+Combine this with 20J <= 2b (i.e. 10J <= b):
 
-   20 J  <=  6 J,      so      J = 0.
+   10 J  <=  b  <=  3 J + 3 M_mark - 3,   so
+   7 J   <=  3 M_mark - 3.
 
-The diagram is a tree, its exterior word is freely trivial.  A
-path with freely-trivial word in a folded graph returns to its
-source.  That contradicts the chosen injectivity failure (the
-endpoints were supposed distinct).
+Therefore J <= (3 M_mark - 3)/7 and
+b <= 3 J + 3 M_mark - 3 <= (30/7) M_mark < 6 M_mark.
+
+INJECTIVITY.  Take an injectivity failure with M_mark = 1.
+The bound b <= 3 J + 3 M_mark - 3 becomes b <= 3 J, and
+10 J <= b then forces 10 J <= 3 J, hence J = 0.
+
+The diagram is therefore a single tree, and its exterior word
+(= the source path between the two distinct source vertices)
+is freely trivial, because there are no bounded faces to read
+relators from.  In the folded graph Y, a nonbacktracking path
+has a freely reduced word: two consecutive labels s, t satisfy
+s != t^{-1}, since otherwise the second edge would be the
+unique edge at that vertex with label t, forcing it to be the
+reverse of the first edge, a backtrack.  A freely reduced word
+can only be freely trivial if it is empty.  So the source path
+is empty, meaning its endpoints coincide; that contradicts the
+chosen injectivity failure (they were assumed distinct).
 
 Consequently every component map phi is injective, and the same
 argument applied to edges handles the edge case.  Since phi is
@@ -2415,7 +2441,7 @@ remove; the same bound is valid.
 WEIGHTED TRACE BOUND.  Fix t in (0, delta).  Write tr_id for the
 identity trace of 10.3 (sum over base and matrix indices, or over
 its central Fourier fiber; the countable amplification is handled
-by Lemma nil:trace).  Since P_i and E_P(t) are equivariant, the
+by the adjoint-square identity-trace lemma of Part 7).  Since P_i and E_P(t) are equivariant, the
 adjoint-square identity and positivity give
 
    tr_id(P_i E_P(t) P_i)
@@ -2506,8 +2532,8 @@ tr_{C^N}( E_Q(u, u) )  =  e_{type(u)}
 for every u in Q, where type(u) is the base vertex under the
 embedding Q -> X.  A lift u of the base vertex v lies over the
 same layer as v: the layer is preserved by the graph embedding.
-The weight estimate of Part 9 (geo:weight) says that for every
-vertex u of B(Q) over layer i = layer(u), the whole ball satisfies
+The weight estimate of Part 9 says that when the ball B(Q)
+lies over layer i, its whole vertex set satisfies
 
    |V(B(Q))|  <=  w_i  =  2^{C_bullet H_i}.