Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

All-depth generation of weighted A-path algebras

Abstract

Every endpoint-rooted A-path block algebra is generated by the existing local path kernels at all depths.

Theorem 1.1 (Exact path reachability).

Lean statement: D5/S3/Quantum/Algebra/Knot/WeightedPathFullGeneration.path_reachable_iff

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/Knot/WeightedPathFullGeneration.path_reachable_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural N with N at least two, every natural depth n and every v in Fin N, the existing LegalPath fiber of the adjacency relation of SimpleGraph.pathGraph N, with start zero, depth n and endpoint v, is nonempty if and only if v.val is at most n and v.val modulo two equals n modulo two. No bound on the depth is imposed.

Every prefix of a legal path has endpoint value at most its length and the same parity as its length, since each edge changes the vertex value by exactly one. Conversely, let a=n-v.val. The parity condition makes a even. At coordinates j at most a use j modulo two; at coordinates j greater than a use j-a. The first segment alternates between zero and one, which are available because N is at least two. The second segment ascends to v. The joining edge is zero to one. Every coordinate lies in Fin N, so this is an actual path in the original carrier.

Theorem 1.2 (The unique possible fresh endpoint).

Lean statement: D5/S3/Quantum/Algebra/Knot/WeightedPathFullGeneration.path_fresh_endpoint

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/Knot/WeightedPathFullGeneration.path_fresh_endpoint (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every N at least two, every natural m and every endpoint v in Fin N, if the length-m path fiber from zero to v is empty and the length-(m+2) fiber is nonempty, then v.val=m+2. In particular, any two nonempty fresh endpoints are equal. Exact reachability at the two depths gives equal parity, and failure of reachability at the lower depth forces v.val greater than m.

Theorem 1.3 (The actual fresh path fiber).

Lean statement: D5/S3/Quantum/Algebra/Knot/WeightedPathFullGeneration.path_fresh_fiber_subsingleton

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/Knot/WeightedPathFullGeneration.path_fresh_fiber_subsingleton (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every N at least two, every natural m and every v in Fin N, absence of a length-m path from zero to v implies that the actual length-(m+2) LegalPath fiber from zero to v is a subsingleton. Empty fibers are included. If this fresh fiber is nonempty, its endpoint value is m+2 and each coordinate j has vertex value j. It therefore consists exactly of the strictly ascending path.

For any length-n path ending at vertex value n, the endpoint coordinate equals n. Backward induction, together with the prefix upper bound, forces coordinate j to equal j: an edge to j+1 and the bound at j exclude every other value. Equality of Fin-valued coordinates gives equality of the original LegalPath subtypes. This is uniqueness in the actual path fiber, rather than an identification of a replacement coordinate type.

Theorem 1.4 (Literal generation at every depth).

Lean statement: D5/S3/Quantum/Algebra/Knot/WeightedPathFullGeneration.weighted_path_full_generation

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/Knot/WeightedPathFullGeneration.weighted_path_full_generation (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural N at least two, every strictly positive real weight function d on Fin N, every strictly positive real delta and every natural n, the unital complex subalgebra adjoin of the set of existing localProjection R d delta n zero i, at all natural sites with zero less than i less than n, equals the top subalgebra of the existing C R n zero, where R is the adjacency relation of SimpleGraph.pathGraph N. The product includes every endpoint block and every empty fiber. The weights need not satisfy a Perron equation; under these hypotheses the named kernels need not be idempotent.

At depths zero and one, exact reachability leaves one nonempty endpoint fiber, consisting of one path. Every block-algebra element is therefore its sole coefficient times the identity. Every unital complex subalgebra contains it, even though there are no interior local generators.

At depth m+2, reuse weighted_path_returning_blocks: the linear span of iota(X) lastProjection(m+1) iota(Y), for X,Y in the preceding full block algebra, is exactly the submodule with zero endpoint-v block whenever the depth-m path fiber to v is empty. A subalgebra containing the preceding algebra image and the last kernel contains that span. For the path graph there is at most one fresh nonempty block, and its actual matrix fiber is a singleton. Subtract its sole coefficient times the full identity. The remainder is zero on every nonreturning block, including all empty blocks, hence belongs to the returning span. Adding back the scalar identity gives every element of C.

Induct on the depth. Projection naturality sends each old literal generator to the same site at the new depth. The actual iotaHom and the adjoin/comap universal property consequently put the full preceding algebra image into the new generated subalgebra. The new lastProjection is precisely localProjection at site m+1. The fresh-block argument proves the induction step for every m, including depths beyond the last new endpoint.

The result is a derivation for the repository’s literal weighted path coordinates using its returning-block theorem. The line-graph path-model operators are classical: Aharonov, Jones and Landau, A Polynomial Quantum Algorithm for Approximating the Jones Polynomial, arXiv:quant-ph/0511096v2, Definition 3.2 and equation (4), provide related operators with specific weights. No claim of mathematical novelty is made for full path-algebra generation. This theorem does not identify an abstract Temperley-Lieb quotient kernel, prove a Jones-Wenzl cutoff, or construct a geometric knot invariant.

References