diff a3632b1..a8edaab artin_parabolic_intersections_v2.txt
diff --git a/artin_parabolic_intersections_v2.txt b/artin_parabolic_intersections_v2.txt
index 380ed0e..67d4b4d 100644
--- a/artin_parabolic_intersections_v2.txt
+++ b/artin_parabolic_intersections_v2.txt
@@ -357,3 +357,291 @@ The height being bounded along a sequence of positive words forces
strong consequences. That is the central engine of the proof.
-- Section 10 continues in the next chunk of this file --
+
+================================================================
+10. REDUCTION TO PROPER SPHERICAL PARABOLICS
+================================================================
+
+Fix Y (a subset of S, possibly nonspherical) and x in A. The
+STABILIZER of the family at x inside A_Y is
+
+ H(Y, x) = { a in A_Y : the family E_L(x) is preserved by B_a
+ for every label L }.
+
+Equivalently: a in A_Y lies in H(Y, x) iff every member of the
+family at x is homotopy-equivalent to itself after B_a.
+
+For Y = S and x = 1 we will have H(S, 1) = A_X (Section 16). And
+the algebra X of the theorem becomes the Z we have defined.
+
+So the main theorem has become a statement about the stabilizer
+subgroups H(Y, x). Specifically:
+
+ STABILIZER THEOREM. For every Y and x, there exist a subset
+ R of Y and an element c of A_Y with
+
+ H(Y, x) = c^{-1} A_R c.
+
+That is the content of Section 14. The proof splits into two
+phenomena:
+
+ PHENOMENON 1 (spherical Y): a positive-word argument shows that
+ the stabilizer is either everything or is contained in a proper
+ spherical parabolic of smaller rank.
+
+ PHENOMENON 2 (nonspherical Y): a height argument shows that
+ the stabilizer is contained in a conjugate of a proper parabolic
+ whose intersection with A_Y has smaller rank.
+
+Both phenomena reduce the rank. Induction on |Y| then finishes.
+
+================================================================
+11. CAPS AND HARMONIC INTERPOLATION
+================================================================
+
+Fix Y, x, and the family E_L(x). For a colour subset D and an
+integer q, the family is CAPPED at q on D if no member has any
+generator of any colour in D at level greater than q. A cap is
+inclusive: level exactly q is allowed.
+
+Lemma 11.1 (Cap accessibility). If a cap holds on a colour set
+D that includes a visible colour, then it can be moved inward:
+there is another representative of the same coset with a cap on
+a strictly smaller set D'.
+
+The cap is a mechanism for reducing freedom. If we can cap on a
+set D that already saturates what we need, we're done: the level
+counts are controlled.
+
+Lemma 11.2 (Harmonic interpolation). For a spherical subset T
+of S, the linear map "value at exterior vertices" -> "interior
+entries" has a unique extension to the interior such that
+(C p)_T = 0, where C is the Cartan matrix of the spherical type.
+This extension is called the HARMONIC INTERPOLATION of the
+exterior data on T.
+
+The interpolation is nonnegative on nonnegative exterior data,
+by a positivity property of the inverse Cartan matrix C^{-1}.
+
+================================================================
+12. HARMONIC HEIGHT AND CONNECTED MINIMA
+================================================================
+
+Fix Y (any, no sphericity), x in A. The POSET OF SPHERICAL COSETS
+P(Y, x) has vertices:
+
+ (T, A_T z), where T subset of Y is spherical, z in A_Y x.
+
+So a vertex is a right coset of a SPHERICAL parabolic, inside the
+coset A_Y x. Two vertices are adjacent when their cosets are
+nested. The undirected comparability graph is connected.
+
+Each vertex v = (T, A_T z) and level k carries:
+
+ - m^k(z) : generator counts on A_T z (independent of the
+ representative);
+ - p^k(v) : harmonic interpolation of m^k(z) on T;
+ - eta^k(v): sign mask (+-1 or 0) depending on visibility.
+
+The HEIGHT of v is a lexicographic comparison of a "block"
+combining: total sum p^k(v), the vector (p_i^k(v))_i, and the
+sign coordinates eta_i^k(v) restricted to T. Blocks are ordered
+from the highest level k down.
+
+Key facts proved by structure of the interpolation:
+
+Lemma 12.1 (Well-order). The heights are well-ordered, and the
+least block has total sum zero.
+
+Lemma 12.2 (Descending upper). Ascending neighbours either
+don't exist or belong to a spherical extension. Specifically:
+a NULL VISIBLE component (a set on which the harmonic vector is
+a positive null vector with all signs 0) cannot be a positive
+support component; this is exactly the NULL-LAYER OBSTRUCTION of
+Section 13. Hence all "active" colours form a spherical set, and
+descending upper neighbours are connected.
+
+Lemma 12.3 (Descending lower). A descending lower neighbour is
+obtained by opening an ELIGIBLE colour (one whose actual count is
+strictly below the harmonic prediction, or equal with a +1 sign
+mask). Opening all eligible colours is a well-defined descending
+move; the resulting lower neighbours are connected.
+
+Proposition 12.4 (Connected minima). In P(Y, x), the vertices of
+minimum height form a nonempty connected subgraph. Their sets K
+(invisible colours) and T_+ (visible colours) are constant along
+this graph.
+
+PROPOSITION 12.5 (Containment from a minimum). Fix a minimum
+vertex (T, A_T z). Let K and T_+ be as above, and D = T_+ u K.
+Then T_+ and K are non-adjacent, T_+ is spherical, and
+
+ x^{-1} H(Y, x) x is contained in z^{-1} A_D z.
+
+So we have placed H(Y, x) inside a conjugate of A_D. If D is a
+proper subset of Y, we can apply the conjugation lemma and induct.
+
+The case D = Y is the hard case. That is exactly when Y itself
+is a positive null component: the harmonic vector on Y is a
+positive null vector and every representative strictly exceeds it.
+
+================================================================
+13. THE NULL-LAYER OBSTRUCTION
+================================================================
+
+This is the central technical lemma. It rules out the "bad case"
+D = Y of Proposition 12.5 unconditionally, using only:
+
+ (a) a NULL VECTOR hypothesis: c_I is a positive null vector of
+ the Cartan matrix C_I on a support I (so C_I c_I = 0 and
+ c_I > 0);
+
+ (b) a CONNECTED SUPPORT hypothesis: the minimal complex of any
+ single family member has connected color support containing
+ the f-frame generator.
+
+PROPOSITION 13.1 (Relative null-layer obstruction).
+
+ Fix a representative z of a spherical coset. Suppose
+
+ - every color of I is "run" in the sense that its level-q
+ generator count is strictly above c_I;
+ - every boundary color of I is capped at level q;
+ - some member of the family has a level-q top at a color of I;
+
+ and the additional exterior hypothesis:
+
+ - the exterior generators of the family are fixed and satisfy
+ no "strict" case at level q.
+
+ Then we get a contradiction.
+
+Proof outline (three steps):
+
+ STEP 1. By the cap projection of Section 11, reduce to a
+ representative that is capped on T (a set containing I).
+
+ STEP 2. The "excess" vector m^q(z) - c_I is a strictly positive
+ convex combination of generator dimensions of an actual
+ subobject M of the level-q layer (the "capped-layer hull").
+
+ STEP 3. Compute the TENSOR of the highest right divisor with
+ the left family. Using the weighted Euler characteristic
+ (a formula balancing two linear maps), we get an exact numeric
+ identity:
+
+ D_0 v^T C y = h_0 + h_0' - h_1
+
+ with h_j nonnegative dimensions from the linear Hom complex.
+ The left side is zero, so each h_j is zero. That vanishing
+ forces a boundary color to be occupied at level below q, but
+ the cap rules this out. Contradiction.
+
+The consequence: in the harmonic height filtration, no visible
+colored component can be a positive null component. Every
+"visible" color is surrounded by "invisible" neighbours on the
+side that matters. This is what turns the case D = Y into a
+contradiction (i.e., into a proper subset D < Y).
+
+================================================================
+14. STABILIZER THEOREM
+================================================================
+
+With Sections 10-13 in hand, we can now prove the STABILIZER
+THEOREM by induction on |Y|. Let us state the proof in stages.
+
+THEOREM 14.1 (Relative stabilizers are parabolic). For every
+subset Y of S and every x in A there exist R subset of Y and c in
+A_Y with
+
+ H(Y, x) = c^{-1} A_R c.
+
+LEMMA 14.2 (Conjugating a stabilizer). Let D subset of Y and
+b in A_Y. If H(Y, x) is contained in b^{-1} A_D b then
+
+ b H(Y, x) b^{-1} = H(D, b x).
+
+Proof: For c in A_D, invertibility of B_b gives the equivalence
+"E_L(c b x) is homotopy-equiv to E_L(b x)" iff "E_L(b^{-1} c b x)
+is homotopy-equiv to E_L(x)". Right side says precisely that
+b^{-1} c b is in H(Y, x). So H(D, b x) = A_D ∩ b H(Y, x) b^{-1},
+which by hypothesis is b H(Y, x) b^{-1}.
+
+PROOF OF 14.1. Induction on |Y|.
+
+ CASE Y = empty: trivial (H is the trivial group, R = empty,
+ c = 1).
+
+ CASE |Y| >= 1, two subcases:
+
+ SUBCASE A: Y is spherical. If all tests on the operated family
+ at x are acyclic (i.e., every test cohomology vanishes), then
+ every generator of A_Y fixes every family member, so H(Y, x) =
+ A_Y. Take R = Y, c = 1.
+
+ If not all tests are acyclic, Proposition 15.3 (Section 15)
+ gives a containment H(Y, x) inside b^{-1} A_D b for some b in
+ A_Y and some PROPER D subset of Y with D SPHERICAL. Apply
+ Lemma 14.2 to get H(Y, x) = b^{-1} H(D, b x) b. Then induction
+ on D applies, giving R subset D (thus R subset Y) and c in A_D
+ (thus c in A_Y) with H(D, bx) = c^{-1} A_R c. Hence
+ H(Y, x) = (bc)^{-1} A_R (bc). Done.
+
+ SUBCASE B: Y is nonspherical. By Proposition 12.5 with
+ a minimum vertex, we have H(Y, x) contained in z^{-1} A_D z for
+ some z in A_Y and some D = T_+ u K, where T_+ is spherical and
+ K is the invisible set. If D is PROPER in Y, we're done by the
+ same conjugation-and-induct argument. If D = Y, we are in the
+ bad case; but Proposition 13.1 rules out D = Y being a positive
+ null component (spherical). So D is proper. Done.
+
+================================================================
+15. SPHERICAL POSITIVE HEIGHT
+================================================================
+
+We need to fill the gap in SUBCASE A: for spherical Y and any x,
+if not all tests are acyclic, H(Y, x) is contained in a conjugate
+of a proper spherical parabolic.
+
+This is the "positive height" argument. Suppose for a
+contradiction that H(Y, x) is NOT contained in any proper
+parabolic. Then there is an infinite sequence a_1, a_2, ... of
+positive words in A_Y such that h(a_1) <= h(a_2) <= ... where
+h(a_k) is the height of any test at a_k, and all colours of Y
+appear in each a_k.
+
+But the height h is bounded above by a constant (if the operated
+test cohomology is nonzero) and by -infinity (if acyclic). The
+"bounded below" of h under positive words is thus the real issue.
+
+Lemma 15.1 (Path bound, Ocneanu/Jones-Wenzl). For spherical Y,
+there is an integer N = N(Y) >= 1 such that in a minimal bounded
+complex whose generators on a cochain interval all sit in Y, any
+composition of N successive arrow coefficient maps vanishes.
+
+This is a nilpotence statement in the Jones-Wenzl algebra, a
+finite-dimensional operator algebra. The proof uses the positive
+definiteness of the Cartan matrix C_Y.
+
+Lemma 15.2 (Cochain drop). Suppose all tests on Y in a bounded
+family have ordinary cochain cohomology in degrees at most m.
+Positive operations in Y preserve this bound. After a positive
+word that contains every colour of Y, the bound improves to m-1.
+
+Iterating 15.2 forces cochain degrees to drop without bound. The
+path bound 15.1 converts "cochain degree dropped below every
+exterior generator" into "empty cochain placement", which is
+zeroth-dimensional cohomology of a minimal complex -> the complex
+DECOMPOSES as a direct sum. But every family member E_L(x) is
+indecomposable. Contradiction.
+
+Hence:
+
+PROPOSITION 15.3 (Spherical containment). For spherical Y and
+any x in A: either all tests on Y at x are acyclic and H(Y, x) =
+A_Y, or H(Y, x) is contained in p^{-1} A_J p for some positive
+word p and some PROPER subset J of Y.
+
+That closes SUBCASE A of the stabilizer theorem.
+
+-- Sections 16-19 in the next chunk --