7 Residual transport categories
On this page · Permalink · Source line 648
Vertical lifting never changes a residual root. Horizontal coverage requires operations whose residual effect is not congruent to the identity. Examples that may define such transports include twisting, duality, restriction, induction, tensor product, symmetric powers, exterior powers, and functorial transfer. The word “may” is essential: each operation must preserve the deformation conditions and the realization statement being transported.
Definition 7.1: Admissible residual transport
An admissible transport from \(\bar\rho\) to \(\bar\rho'\) consists of
together with natural maps
for every coefficient algebra \(A\), compatible with base change and reduction. When the transport is reversible, it is an isomorphism in the residual transport groupoid. One-way operations give a directed category.
Visual guide: An atlas of the objects · Visual guide: A transport must work at every depth · Permalink · Source line 652 · Claim record · Lean coverage · Code · Worked examples
For a finite collection of roots, record a directed edge \(u\to v\) whenever occupancy or the relevant property is known to propagate from \(u\) to \(v\).
Definition 7.2: Directed seed rank
For a directed transport graph \(G\), define
where \({\operatorname{Cl}}_G(S)\) is the set of vertices reachable from \(S\).
Visual guide: An atlas of the objects · Permalink · Source line 666 · Claim record · Lean coverage · Code · Worked examples
Theorem 7.3: Directed minimum-seed theorem
Let \(G\) be a finite directed graph. Collapse every strongly connected component to one vertex, obtaining the condensation DAG. Then
One representative from each source component is a minimum seed set.
Read proof · Visual guide: How many starting seeds are necessary? · Read statement and proof side by side · Permalink · Source line 676 · Claim record · Lean coverage · Code · Worked examples
Proof of Theorem 7.3
Every vertex of a finite DAG is reachable from a source, so one seed in each source component reaches the entire condensation graph. Within a strongly connected component, one vertex reaches every other. Hence the source representatives are sufficient.
Conversely, a source component has no incoming edge from another component. It cannot be reached from a seed outside itself, so every generating seed set must meet it. Therefore the number of source components is also a lower bound.
Back to statement · Read statement and proof side by side · Permalink · Source line 688 · Claim record · Lean coverage · Code · Worked examples
For reversible transports the condensation has one vertex per connected component, recovering the undirected minimum-seed theorem.
Formal scope and propagation.
On this page · Permalink · Source line 696
Reachability is the reflexive-transitive closure of the supplied directed edge relation, and a strongly connected component is the actual quotient by mutual reachability. The minimum seed count is defined independently as the least cardinality of a set that reaches all vertices. Every covering set must meet every source component; conversely, meeting every source component suffices in a finite graph. Thus any choice of one representative from each source is optimal. Empty graphs have rank zero, and self-loops are permitted. Adding admissible edges cannot increase the minimum seed count.
If a property \(P\) propagates along every supplied edge and holds at all selected seeds, it holds at every reached vertex. These are explicit hypotheses. The minimum-seed theorem does not construct valid arithmetic edges or supply initial occupancy.
Why the finite hypothesis cannot be dropped.
On this page · Permalink · Source line 711
Take vertices \(\{*\}\sqcup\{v_n:n\in\mathbf N\}\), with \(*\) isolated and edges \(v_{n+1}\to v_n\). Every strongly connected component is a singleton, and \(\{*\}\) is the unique source component. No finite seed set covers all vertices: it can reach only indices no larger than the largest chosen index. Both the unique-source statement and the failure of every finite cover are checked in Lean. Hence one source component in an infinite condensation does not imply that one seed reaches all objects.
Numerical certificate 7.4: Directed seed count
The test graph has five strongly connected components and three source components. The theorem gives seed rank three. Exhaustive search over every subset of vertices independently returns three, and the selected representatives reach all seven roots.
New explicit checked realization.
Separately from the unretrieved original companion implementation, Block 05 specifies vertices \(A,B,C,D,E,F,G\) and the eight edges
The source components are \(\{A,B\}\), \(\{D,E\}\), and \(\{G\}\); the other components are \(\{C\}\) and \(\{F\}\). A bounded path search to length three is proved closed under every original edge, which certifies equality with unbounded reachability. The resulting label certificate is identified with the actual quotient by mutual reachability. Lean checks seed rank three and exactly the four minimum sets
Independent exact tests enumerate every directed graph on zero through four vertices, including loops, and every seed subset. These finite tests audit the implementation; the universal theorem is a separate formal proof.
Permalink · Source line 734 · Claim record · Lean coverage · Code · Worked examples