Directed paths and strictly positive convolution necessity
Abstract
The constant sequence one admits generalized action graphs at every stage: the directed paths from zero to n. Its convolution coefficients cannot all be strictly positive.
Definition 1.1 (The three generalized action-graph axioms).
Formalization. D5/S3/Combinatorics/Graph/ActionGraphs/PositiveNecessity.IsGeneralizedActionGraph (✓ std3).
Citation. S. Klanderman, K. McDicken, A. Tebbe (2026). Conditions for Building Generalized Action Graphs From Sequences. DOI: 10.46787/pump.v9i.6304. URL: https://journals.calstate.edu/pump/article/view/6304.
Commentary.
Definition 1.1: “The sequence Gn of generalized action graphs for a particular sequence sn of positive integers is a sequence of directed, labeled, rooted trees such that: Axiom 1 Define G0 as the graph with s0 vertices labeled 0 and no edges. Construct Gn from Gn−1 by adding sn new vertices, which are each labeled n. Axiom 2 For vertex v in Gn, the subtree of Gn with root v is isomorphic to some Gk such that k ≤ n. Axiom 3 All leaves in the graph Gn have label n.” Finite vertex types V(n), native directed graphs G(n), roots, labels and injective maps step(n) retain the actual graphs. The underlying simple graph is a tree, every vertex is reachable from the root, and there is no nonempty directed closed walk. The maps retain the old root, labels and edges; their complements have exactly s(n+1) vertices, all labeled n+1. The subtype in Axiom 2 consists of every descendant, including its root, with exactly the edges inherited from G(n). RelIso preserves and reflects directed adjacency. Its root equation and a single additive shift describe the rooted labeled isomorphism. Section 3.1 states: “Note that when we consider isomorphism in generalized action graphs, the labels on the vertices may be shifted, but the underlying structure of the graphs are the same.” A leaf is a vertex with no outgoing edge.
Definition 1.2 (The strictly positive necessity question).
Formalization. D5/S3/Combinatorics/Graph/ActionGraphs/PositiveNecessity.claim (✓ std3).
Citation. S. Klanderman, K. McDicken, A. Tebbe (2026). Conditions for Building Generalized Action Graphs From Sequences. DOI: 10.46787/pump.v9i.6304. URL: https://journals.calstate.edu/pump/article/view/6304.
Commentary.
Section 4 asks: “Another open question is whether the hypotheses of Theorem 1.1 are in fact necessary conditions for generalized action graphs to exist.” The displayed proposition quantifies every positive integer sequence and the existence of an entire family satisfying Definition 1.1. The conclusion includes s(0)=1 and a strictly positive coefficient z(i) for every i at least one. The unused value z(0) has no restriction and occurs in no sum. All graph stages and all convolution equations are quantified.
Theorem 1.3 (Refutation by the entire directed-path family).
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Graph/ActionGraphs/PositiveNecessity.result (✓ std3). ∎
Resolves. Problems/klanderman-2026-positive-action-graph-necessity (refuted) by D5/S3/Combinatorics/Graph/ActionGraphs/PositiveNecessity.result.
Source. Repository-derived.
Acknowledgement. S. Klanderman, K. McDicken, A. Tebbe (2026). Conditions for Building Generalized Action Graphs From Sequences. DOI: 10.46787/pump.v9i.6304. URL: https://journals.calstate.edu/pump/article/view/6304.
Commentary.
Set s(n)=1 for every natural n. At stage n take Fin(n+1), root zero, labels equal to vertex values and the directed covering relation: an edge goes from i to i+1. Forgetting orientation gives Mathlib’s pathGraph(n+1), which is a tree. Reachability is the order relation, and nonempty directed reachability is strict order, so directed cycles do not occur. Fin.castSuccEmb retains the previous graph and adds just its new last vertex. For any vertex i, translation j ↦ i+j is a bijection from Fin(n−i+1) to its actual descendant subtype, preserving directed edges and its root and shifting every label by i. The only leaf is n. These statements include n=0 and i=n. If strictly positive z satisfied the convolution, the equations at one and two would give z(1)=1 and 1=z(1)+z(2), forcing z(2)=0. The strictly positive necessity proposition is therefore false. No conclusion about the nonnegative-coefficient variant follows.