Returning path blocks and matrix units
Abstract
The last literal local path kernel generates exactly the returning endpoint matrix blocks.
Theorem 1.1 (An exact returning matrix-unit factorization).
Lean statement: D5/S3/Quantum/Algebra/Knot/WeightedPathReturningBlocks.returning_matrix_unit_factorization
Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/Knot/WeightedPathReturningBlocks.returning_matrix_unit_factorization (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let L be any finite decidable vertex type and R any relation on L. Let d be any real vertex weight function, delta any real number, and m any natural number. Fix s,v,a,c in L, legal edges v to a, v to c, a to v and c to v, a literal length-m LegalPath r from s to v, a length-(m+1) path x from s to a, and a length-(m+1) path y from s to c. All these parameters are universally quantified. No Perron, positivity, symmetry or connectedness assumption is needed for this exact identity.
Use precisely C, append, iota and lastProjection from WeightedPathMarkovTrace. The blockUnit at endpoint t and paths p,q is the matrix single(p,q,1) in block t and zero in every other block. Put X=blockUnit(a,x,append(r,a)) and Y=blockUnit(c,append(r,c),y), both at depth m+1. Then iota(X) lastProjection(m+1) iota(Y) equals sqrt(d(a)d(c))/(delta d(v)) times the depth-(m+2) blockUnit(v,append(x,v),append(y,v)). The real coefficient is cast to the complex scalar field, using the literal Real.sqrt and division conventions of pathProjection, including zero denominators.
The proof identifies the actual inclusion of a path matrix unit at each endpoint, reduces the sandwich to a single middle matrix entry, and shows that this entry forces the endpoint to equal v. Its square-root coefficient is retained literally. This is a proof on the existing full block algebra, rather than a definition of an algebra generated by the projections. The original append/split/inclusion helper declarations are exposed at their source owner and directly reused.
Theorem 1.2 (Exactly the full returning endpoint blocks).
Lean statement: D5/S3/Quantum/Algebra/Knot/WeightedPathReturningBlocks.weighted_path_returning_blocks
Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/Knot/WeightedPathReturningBlocks.weighted_path_returning_blocks (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every finite decidable L, every symmetric relation R, every strictly positive real vertex weight d, every strictly positive real delta, every natural m and every start s, the complex linear span of all iota(X) lastProjection(m+1) iota(Y), with X,Y ranging over the full C(R,m+1,s), equals the submodule of C(R,m+2,s) whose endpoint-v block is zero whenever there is no length-m LegalPath from s to v. All endpoint blocks and empty fibers remain in the quantifiers. Neither the Perron equality nor connectedness is required for this spanning statement.
For a returning endpoint v, choose one length-m path r to v and split arbitrary length-(m+2) paths p,q into their final edge and prefix. Symmetry gives the reverse edges. The matrix-unit factorization supplies blockUnit(v,p,q), since its coefficient is nonzero by the positive weights and delta. Existing Mathlib matrix-basis and dependent-Pi decomposition then supply every matrix in every returning block. Conversely, a nonzero local-kernel entry contains a length-m prefix ending at the block endpoint. Thus a nonreturning block of the last local kernel is zero, and every sandwich has zero there. Its established function name is lastProjection; idempotence is not asserted under these more general parameters.
This is the path-level basic-construction spanning step needed to prove fullness for endpoint-rooted A-type graphs. It does not yet prove the A-type reachability classification, generation of the entire tower, an abstract Temperley-Lieb presentation, a Jones-Wenzl cutoff, a reverse-kernel normal form or a quotient isomorphism. In particular, no geometric closure/Jones-polynomial identification follows from this theorem. Goodman and Wenzl, Ideals in the Temperley Lieb Category, arXiv:math/0206301v1, Proposition 2.1, supplies a separate classical tensor-ideal destination; that result is not assumed in this matrix-unit derivation.