Named Tree Phase Transport
Abstract
Signed phases on an arbitrary selected named spanning tree give actual continuous multiplicative root transport and its gauge covariance.
Let V and E be arbitrary vertex and named edge types, with endpoint maps s,t:E to V. Only the selected subset T has simple support: its edges have different endpoints, and the map sending each selected named edge to its unordered endpoint pair is injective. The graph generated by exactly those pairs is connected and acyclic. There is no restriction on parallel edges, loops, or separately named reverse edges outside T.
For each adjacency in that support, choose its unique original named edge. Traversing it from its source to its target uses u_e; traversing it the other way uses its inverse. The latter is a formal comparison symbol, independent of execution permissions. Multiply these signed phases along the unique simple tree path from a chosen root r. Its value is h_v(u). Empty transport has value one. Uniqueness applies to simple paths and makes no claim about walks with backtracking.
Theorem 1.1 (Actual transport, selected-edge reconstruction and covariance).
Proof. Machine-checked in Lean as D5/S3/Observer/AgencyHolonomy/NamedTreePhaseTransport.selected_tree_transport (✓ std3). ∎
Source. Repository-derived.
Commentary.
On a selected edge, one of the two root paths is the other path with that adjacency appended. The acyclic simple-path concatenation law establishes this dichotomy. Reversing the selected named traversal inverts its phase, so in both orientations h_t=u_e h_s.
For g:V to Circle, the original edge field transforms as g_t u_e g_s inverse. The intermediate vertex factors cancel in the signed tree product, yielding g_v h_v g_r inverse. Each support adjacency is transferred to an original directed generator or its formal inverse. The resulting typed path in the symmetrified named quiver is evaluated by the public path-weight map in the group of continuous monoid homomorphisms. Its scalar evaluation equals the signed product. Hence each fixed tree product is continuous and multiplicative as a function of the whole edge field, and sends the constant unit field to one.