Paper deep dive
Andy: A Mathematical Agent for Rigorous Proof and Autonomous Research
Zi'an Wang
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 93%
Last extracted: 8/21/2026, 2:52:13 AM
Summary
The paper introduces Andy, an autonomous mathematical research agent that automates the workflow from problem formulation to rigorous proof verification. Andy utilizes a dual-model architecture separating solver (DeepSeek V4 Pro) and evaluator (Claude Sonnet 5) roles. It employs a research-value gate to filter new problems based on literature grounding and originality, and organizes proofs in an executable Directed Acyclic Graph (DAG) to enable independent verification, local repair, and incremental progress. The system is demonstrated through a case study on global exponential leader-follower synchronization for delayed heterogeneous networks.
Entities (9)
Relation Signals (7)
Zi’an Wang → affiliatedwith → Tongji University
confidence 98% · Address: School of Mathematical Sciences, Tongji University
Andy → uses → DeepSeek-v4-pro
confidence 95% · The main solver uses DeepSeek V4 Pro.
Andy → uses → Claude Sonnet 5
confidence 95% · The mathematical correctness evaluator uses Claude Sonnet 5.
Andy → implements → Proof DAG
confidence 90% · It organizes proof steps in an executable DAG
Andy → solves → Leader-Follower Synchronization
confidence 90% · Andy formulates a global exponential leader-follower synchronization problem... Sufficient conditions... are established
Andy → uses → Research-value Gate
confidence 90% · formulates a literature-grounded new problem through a research-value gate
Andy → uses → Tavily
confidence 85% · Andy can use Tavily to search for related literature as needed.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Andy is an autonomous mathematical research agent that turns a mathematical problem into a traceable proof. It solves or verifies a submitted problem, formulates a literature-grounded new problem through a research-value gate, and carries it through proof construction and final verification. It organizes proof steps in an executable DAG, verifies each step independently and binds the result to a certificate, retains verified work whose interfaces remain unchanged during local repair, and records the full path from problem formulation to final proof. The system separates proof generation from correctness evaluation and can acquire, retain, retrieve, and reuse knowledge from existing results. Starting from a self-triggered impulsive consensus result, Andy formulates a global exponential leader-follower synchronization problem for delayed heterogeneous networks with switching communication topologies. The proposed hybrid control combines self-triggered impulses with execution delay and continuous feedback over a recovery window. After each delayed impulse, the feedback cancels the delayed error channel until the pre-impulse history leaves the active delay interval. Sufficient conditions for global exponential synchronization are established, Zeno behavior is excluded for both timing sequences, and a numerical example illustrates the result.
Tags
Links
- Source: https://arxiv.org/abs/2608.15052v2
- Canonical: https://arxiv.org/abs/2608.15052v2
Trouble viewing inline? Open PDF directly →
Full Text
77,886 characters extracted from source content.
Expand or collapse full text
Global Exponential Leader-Follower Synchronization of Delayed Heterogeneous Networks via Switching Hybrid Control Zi’an Wang wza1012@tongji.edu.cn Address: School of Mathematical Sciences, Tongji University, Shanghai 200092, China Address: Key Laboratory of Intelligent Computing and Applications (Tongji University), Ministry of Education, Shanghai 200092, China Address: Project homepage and source code:https://github.com/mowaiwaim/Andy Abstract Andy is an autonomous mathematical research agent that turns a mathematical problem into a traceable proof. It solves or verifies a submitted problem, formulates a literature-grounded new problem through a research-value gate, and carries it through proof construction and final verification. It organizes proof steps in an executable DAG, verifies each step independently and binds the result to a certificate, retains verified work whose interfaces remain unchanged during local repair, and records the full path from problem formulation to final proof. The system separates proof generation from correctness evaluation and can acquire, retain, retrieve, and reuse knowledge from existing results. Starting from a self-triggered impulsive consensus result [1], Andy formulates a global exponential leader-follower synchronization problem for delayed heterogeneous networks with switching communication topologies. The proposed hybrid control combines self-triggered impulses with execution delay and continuous feedback over a recovery window. After each delayed impulse, the feedback cancels the delayed error channel until the pre-impulse history leaves the active delay interval. Sufficient conditions for global exponential synchronization are established, Zeno behavior is excluded for both timing sequences, and a numerical example illustrates the result. keywords Autonomous mathematical research agent ,Executable proof DAG ,Local verification ,Incremental repair ,Hybrid control ,Exponential synchronization 1 Introduction Large language models and mathematical reasoning systems can solve increasingly difficult fixed problems. Mathematical research requires a broader workflow. A research system must identify a meaningful question, ground it in relevant literature, construct a long proof, distinguish generation from correctness evaluation, and revise local failures without discarding verified work. These capabilities are often studied separately, so it remains unclear whether a mathematical agent can carry a research task from a verified starting point to a traceable theorem, proof, and numerical certificate. Related systems provide useful context for this objective. FunSearch pairs programs proposed by a pretrained large language model with a problem-specific systematic evaluator. AlphaGeometry uses a neural model to generate auxiliary constructions and a symbolic engine to complete geometry proofs [2, 3]. These systems demonstrate how learned generation can be combined with an explicit external evaluation or deduction mechanism. Recent mathematical research agents move beyond fixed benchmark problems. Moonshine extracts structure from classical problems, formulates conjectures, builds connections, and identifies obstacles [4]. Research Math Agents (RMA) targets long-horizon research problems through literature grounding, structured knowledge, iterative proof refinement, and coordinated proposer and verifier roles [5]. QED organizes multiple agents around failure modes observed in open-problem proving and emphasizes structured verification and expert assessment of generated proofs [6]. Recent systems distribute the research cycle differently. ProofCouncil uses an author–critic loop implemented by a conditional workflow-DAG library [7]. Danus coordinates parallel workers through a verifier-gated fact graph that stores proofs and logical dependencies and supports transitive revocation [8]. Rethlas and Archon couple informal research reasoning with Lean formalization [9], while MMAT combines natural-language and formal-language provers with a knowledge-base manager in a full-cycle co-pilot architecture [10]. Table 1 compares mechanisms explicitly documented in the primary reports. Table 1: Capabilities reported by representative mathematical research systems. System Primary research object New problem Proof decomp. Indep. check Long-term memory Formal proof Local revocation Moonshine [4] Conjecture generation and theory exploration E NR P E NR NR RMA [5] Literature-grounded long-horizon proofs NR E E P NR NR QED [6] Natural-language proofs for open problems NR E E P NR P ProofCouncil [7] Author–critic open-problem solving NR P E P P NR Danus [8] Verifier-gated fact-graph proof search NR E E E NR E Rethlas– Archon [9] Informal reasoning followed by Lean formalization NR E E E E P MMAT [10] Natural- and formal-language research co-pilot P E E E E P Andy Value-gated problem formulation and incremental proof E E E E NR E E denotes an explicitly implemented or reported capability. P denotes partial, case-specific, run-local, or architecturally non-equivalent support. NR records only a lack of reporting in the cited primary source and leaves possible implementations unassessed. Together, these developments motivate mathematical agents whose research objects, proof dependencies, and evaluations remain explicit and auditable. To address this gap, we developed Andy, a verification-centered autonomous mathematical research agent. Andy combines solver and evaluator separation, literature-grounded problem generation, a research-value gate, DAG-based proof execution, independent verification, targeted repair, and reusable memory in one auditable workflow. The case study in this paper examines whether this workflow can transform a verified control-theoretic result into a technically meaningful new problem and complete the corresponding theorem, proof, and numerical verification. The main contributions of Andy are summarized as follows. (1) We define an executable, version-bound proof DAG. Each node is a five-part research object consisting of a statement, assumptions, dependencies, a proof, and a verification certificate. The certificate is tied to the exact node version that it verifies. This representation converts a proof outline into an executable dependency structure with explicit admissibility and audit conditions. (2) We implement a verification-controlled DAG executor. A node becomes available only after all its predecessors have been certified. The executor performs topological execution, freezes certified nodes, compares node interfaces after revision, propagates invalidation only when an interface changes, activates backup routes when a branch fails, and re-verifies the assembled proof. Local repair therefore retains certified work whose dependencies remain valid. (3) We provide an end-to-end control-theoretic case study with a complete audit trail. Starting from a verified self-triggered impulsive consensus result, Andy revised the proposed problem eight times across nine versions and explored seven proof routes. It ultimately produced a recovery-window synchronization theorem for delayed heterogeneous networks under switching hybrid control, a complete proof, and a numerical illustration. The recorded trace identifies failed routes, preserved nodes, and the reason for selecting the final route. The remainder of this paper is organized as follows. Section 2 presents the Andy agent architecture. Section 3 gives the control-theoretic case study. Section 4 concludes the paper. 2 Andy Agent Architecture Andy organizes problem solving, problem generation, proof construction, and verification as a single revisable process. Figure 1 summarizes the complete workflow, and the following subsections describe its main components. Submitted problem and optional solution Solve the problem or verify the supplied solution Independent correctness check: premises, calculations, and logic Literature-grounded new-problem formulation Evaluate importance, originality, feasibility, and coherence Targeted revision until the selected threshold is met Explore proof routes and select a promising strategy Build a lemma DAG with explicit dependencies Execute, verify, freeze, or locally repair each node Assemble the complete proof and perform final verification Deliver the proof, certificates, literature links, and research log repair if neededre-evaluaterepair affected node and descendants Figure 1: The research workflow of Andy. 2.1 Solver–Evaluator Separation Andy uses a dual-model architecture that separates the roles of solver and evaluator. The main solver uses DeepSeek V4 Pro. It is responsible for solving the original problem, generating proofs, generating new problems, and revising proofs. The mathematical correctness evaluator uses Claude Sonnet 5. It reviews answers and proofs along three dimensions: use of premises, correctness of calculations, and logical completeness. The evaluator cannot directly modify a proof. It can only provide structured verification conclusions, error locations, and revision suggestions. The main solver then completes the revisions. This separation of roles prevents the solver model from approving its own answer without external review. To use Andy, the user must first provide a problem. If no answer is provided, Andy independently constructs a solution or proof and submits it to the correctness evaluator for review. If an answer is provided, Andy directly verifies that answer without solving the problem independently again. Remark 2.1. During this study, Codex running GPT-5.6 Sol was placed outside Andy and used as a simulated human monitor. It inspected the exposed intermediate reasoning, identified mathematical and strategic errors, and returned targeted guidance. The external monitor supplied the guidance, and Andy’s solver retained responsibility for implementing every revision. This setup shows that the current workflow can still benefit from external oversight when deep reasoning errors are difficult for the internal roles to detect. 2.2 Literature-grounded Problem Generation After the original problem and its proof pass verification, Andy proposes a new research problem. Before a task begins, the user can separately specify the direction for generating the problem or upload reference papers. This guidance is used only during the generation, evaluation, and revision of the new problem. It does not affect the solution and verification of the original problem. Andy analyzes the common features, differences, complementary relations, and research gaps among the papers. In the new problem, it explains which papers were used, which conditions or methods were inherited, and which substantive modifications were made. When the available materials are insufficient to assess originality, related work, or proof tools, Andy can use Tavily to search for related literature as needed. 2.3 Research-value Gate The basic evaluation of a new problem covers four dimensions: importance, originality, feasibility, and coherence. Importance measures whether solving the problem could advance a theory, method, or application. Originality checks whether the problem only renames, rewrites, or directly restates an existing problem. Feasibility examines whether there is a concrete proof strategy, usable tools, and a reasonable point of entry for the research. Coherence examines whether the new problem follows naturally from the original problem or the references and whether it has one clear research objective. It also checks that the problem is not a simple combination of several small problems. If the user provides reference papers, the evaluation system adds a literature support dimension. This dimension checks whether the new problem has traceable links to the papers and contains substantive modifications. The user can specify the target difficulty of the new problem. Every dimension is scored on a ten-point scale. An easy problem requires a total score of at least 6.06.0 and a score of at least 4.54.5 in every dimension. A standard problem requires a total score of at least 7.07.0 and a score of at least 5.55.5 in every dimension. A research-level problem requires a total score of at least 7.57.5 and a score of at least 6.06.0 in every dimension. A pure rewriting of an existing problem triggers a hard gate. A simple combination of several conclusions, the lack of a concrete feasible method, or the inclusion of several parallel subproblems also triggers a hard gate. Such a problem does not pass verification. The user’s choice of difficulty changes only the threshold for research value and the research cost. It does not reduce the correctness requirements for the final proof. If a problem does not pass the evaluation, the evaluation stage explains the reason for each score deduction. It also gives revision instructions that include the specific defect, the mathematical modification, and the acceptance criterion after modification. The generator then revises the same problem draft in a targeted manner and returns it to the evaluation stage for another review. By default, the system automatically enters the proof stage after the problem reaches the threshold. The user can also choose to pause after the evaluation and intervene manually. Algorithm 1 summarizes this formulation, evaluation, and targeted-revision loop. Algorithm 1 Problem formulation and quality gating 1: Verified starting result R, literature L, user direction U, and target thresholds θ 2: Accepted problem Q⋆Q and audit record A 3: Q0←Formulate(R,L,U)Q_0← Formulate(R,L,U) and initialize A 4: for j=0,1,…j=0,1,… do 5: (j,j)←Evaluate(Qj,L,θ)(s_j,g_j)← Evaluate(Q_j,L,θ) 6: Append QjQ_j, dimension scores js_j, and gate verdicts jg_j to A 7: if all score thresholds and hard gates pass then 8: Q⋆←QjQ ← Q_j; return (Q⋆,)(Q ,A) 9: end if 10: Δj←TargetedRevision(Qj,j,j) _j← TargetedRevision(Q_j,s_j,g_j) 11: Qj+1←Revise(Qj,Δj)Q_j+1← Revise(Q_j, _j) 12: end for 2.4 DAG Proof Execution For the proof of a new problem, Andy provides two routes: a rigorous DAG proof route and a deep research route. A directed acyclic graph (DAG) is a directed graph with no directed cycles and therefore admits a topological ordering. In artificial intelligence, DAGs are widely used to encode conditional-dependence structures and organize probabilistic inference [11]. Andy adapts this dependency structure to proof construction. The rigorous DAG proof route first generates only a proof outline, necessary definitions, and lemmas. Andy then represents the proof as a directed acyclic graph. Each node corresponds to a lemma or proof step with explicit inputs, assumptions, and a conclusion. Directed edges represent logical dependencies between nodes. The system first checks node identifiers, dependency relations, and reachability of the target. It then executes the nodes one by one in topological order. DAG mode starts a main proof branch. If the main branch cannot be completed mathematically, Andy activates an alternative branch. If the new DAG executor and the alternative branch both fail, the system can also use a multibranch proof chain as a fallback and try several proof routes. For a research-level problem, the deep research route can be selected. This route first explores several proof strategies at low cost. It compares only the key construction, required lemmas, main risks, and likelihood of completion for each route. After selecting the most promising route, the system converts it into a DAG. It then completes the proof rigorously through node-by-node execution, local verification, freezing, and final overall verification. For a difficult and open-ended problem, this route first obtains the necessary breadth of exploration at low cost. It then concentrates most of the computational effort on the most promising route. For execution, a node version is recorded as v=(Sv,Av,Dv,Πv,Cv)v=(S_v,A_v,D_v, _v,C_v), where SvS_v, AvA_v, DvD_v, Πv _v, and CvC_v are its statement, assumptions, dependency set, proof, and verification certificate, respectively. Its dependency interface is Iv=(Sv,Av,Dv)I_v=(S_v,A_v,D_v), and hv=H(Iv)h_v=H(I_v) is the corresponding interface fingerprint. The certificate is bound to the exact node version and its execution metadata. Algorithm 2 gives the corresponding topological execution and verification procedure. Algorithm 2 Proof-DAG execution 1: Accepted problem Q⋆Q and planned main and backup routes 2: A frozen target node or a certified failure record 3: Build a versioned DAG G and reject cycles, missing dependencies, or an unreachable target 4: while the target node is not frozen do 5: Select a ready node v in topological order; every node in DvD_v must be frozen 6: Πv←Execute(Sv,Av,Dv) _v← Execute(S_v,A_v,D_v) 7: Cv←IndependentVerify(Sv,Av,Dv,Πv)C_v← IndependentVerify(S_v,A_v,D_v, _v) 8: if CvC_v passes then 9: Bind CvC_v to the node version and execution metadata; Freeze(v) Freeze(v) 10: else 11: Repair v, recompute hvh_v, and apply Algorithm 3 12: end if 13: if the active route is mathematically infeasible then 14: Activate the highest-ranked unused backup route 15: end if 16: end while 17: Assemble the proof from frozen nodes and perform an independent final verification Remark 2.2. The present evaluation is preliminary and focuses on the efficiency of DAG execution in one representative task. The main purpose of the DAG is to freeze the parts that have been confirmed as correct and confine errors to local regions. This reduces repeated generation and repeated verification of the entire proof. We used Andy twice to process the problem “Study the zeros and monotonicity of the function x3−x^3-x.” An ordinary proof attempt and verification process serves as the baseline. It took 11 hour, 2222 minutes, and 1212 seconds. The DAG process took approximately 3737 minutes and 59.759.7 seconds. The time decreased by approximately 53.8%53.8\%. The new research problems generated by Andy in the two runs were not identical because of the randomness of the LLM. The experiment shows that the DAG avoided unnecessary execution of complete branches and substantially reduced the running time in this case. The entire time difference cannot be attributed to the DAG. 2.5 Verification and Targeted Repair When a node is executed, the solver can use only the available materials and dependency nodes that have passed verification. After each new node is completed, it undergoes a separate local verification of premises, calculations, and logic. A node is frozen after it passes verification. If a node fails, Andy repairs only that node and the descendants affected by it. Unrelated sibling nodes are not regenerated. If a revision changes only the proof text and leaves the proposition, assumptions, and dependency interface of the node unchanged, verified downstream results can be retained. After all necessary nodes pass, the system assembles the complete proof and performs a unified final verification. If the assembly stage requires a new bridging result, that result must first become a new node and pass a separate verification. Let DescG(v)Desc_G(v) denote the direct and transitive descendants of node v in G. Algorithm 3 makes the repair and assembly contract explicit. Algorithm 3 Invalidation and final assembly 1: Proof DAG G, revised node v, and old and new interface fingerprints hvold,hvnewh_v^old,h_v^new 2: Updated valid DAG and a final verification record 3: ℐ(v)←v,hvold=hvnew,v∪DescG(v),hvold≠hvnewI(v)← cases\v\,&h_v^old=h_v^new,\\ \v\ _G(v),&h_v^old≠ h_v^new cases 4: for all w∈ℐ(v)w (v) do 5: Revoke the frozen state and certificate of w 6: end for 7: Re-execute affected nodes in topological order under Algorithm 2 8: Assemble the final proof using frozen nodes only 9: if assembly introduces a new bridging proposition then 10: Create a new node for that proposition and verify it before continuing 11: end if 12: Independently verify the assembled proof and bind the final record to all cited node versions The executor maintains four system invariants. (1) Dependencies must consist exclusively of verified nodes. (2) Each certificate is strictly bound to a specific statement, proof, context, model, prompt, and code version. (3) Any bridging proposition introduced during assembly must be represented and verified as a new node. (4) The final proof must not cite any invalidated node. 2.6 Memory and Knowledge Acquisition Andy is designed for long-term use and debugging by researchers. It therefore also has a memory function. Andy manages logs and long-term memory separately. The logs provide complete records of problem versions, model rounds, reasoning content returned by model interfaces, tool calls, search results, evaluation reasons, verification certificates, DAG node revisions, frozen and invalidated states, causes of errors, and task checkpoints. These materials are saved as session records and written to the project-level research log. A failed or interrupted task can therefore resume from the corresponding stage. Long-term memory contains selected reusable research information. Andy can store proof-method preferences and evaluation preferences explicitly stated by the researcher. Examples include “Prefer the Lyapunov method for problems of this type in the future” and “A rewriting that only changes notation should not receive a high originality score.” It also stores verified conclusions, successful proof patterns, failed routes, key difficulties, and connections among papers. A new task retrieves only a small amount of memory relevant to the current problem. Failure records help avoid repeating unsuccessful routes and are stored separately from mathematical evidence. Andy organizes its data around a runtime home directory. This directory contains configurations and credentials, project workspaces, session logs, a session database, a knowledge base, long-term memory, Agent definitions, Skills, Tools, runtime logs, and MCP server description files. During a research task, Andy can independently select memory retrieval, knowledge-base queries, literature searches, and verification tools according to the current stage. It updates the research state through a cycle of planning, execution, verification, and local revision. We also designed a research front end to make the system easier to use and review. The front end integrates the creation of a research task, a real-time research workspace, and the final report into a complete workflow. Users can upload materials for the main problem and reference papers. They can separately enter the research requirements for the original problem and the direction for generating a new problem. They can also select the target difficulty and proof mode. During execution, users can view stable stage progress, total running time, the actual reasoning_content returned by the model interface, the verification process, evaluation reasons, literature connections, and the dependencies, revisions, frozen states, and certificate states of DAG nodes. If users find an error in the model’s reasoning, they can append a prompt to correct the research direction. This provides an interface for human intervention. After the task is complete, users can directly download research outputs at different levels from the front end. Andy can ultimately deliver the original problem and its verification conclusion or complete solution, the new problem generated by Andy, itemized scores and revision records, the complete proof of the new problem, and connections to reference papers and retrieved literature. If the proof fails, it returns the reason for failure and subsequent reduced-scope problems. The system can export Markdown, structured JSON, and both complete and concise PDF reports. The complete report retains scores, tools, certificates, versions, and the research process for review and auditing. The concise report retains only the original problem and its complete solution, together with the problem generated by Andy and its complete proof. It is suitable for direct reading and communication. 3 Case Study 3.1 Source Problem The verified source problem is the self-triggered impulsive consensus problem of Hong and Zhang [1]. It studies switched delay multi-agent systems under self-triggered impulsive control. Andy uses this result as a starting point and asks how its scheduling and impulsive-control structure can be extended to a heterogeneous leader-follower network with switching topology and impulse execution delay. 3.2 Problem Proposed by Andy We made only minor formatting adjustments to the model and theorem proposed by Andy. The result is presented below. This case study considers a class of leader-follower heterogeneous networks with switching communication topologies, time-varying delays, and impulse execution delays. The aim is to establish sufficient conditions for synchronization under the joint action of continuous and impulsive control. The model and its regularity assumptions are introduced first. Let N and n be positive integers. Throughout this section, ImI_m denotes the m×m× m identity matrix, ⊗ denotes the Kronecker product, and ∥⋅∥\|·\| denotes the Euclidean vector norm or its induced matrix norm. For symmetric matrices, X⪯YX Y means that Y−XY-X is positive semidefinite. Let skk≥0\s_k\_k≥ 0 be the sampling instants determined by the self-triggered algorithm introduced below. Let τ>0τ>0 be the known impulse execution delay, and define the corresponding impulse execution instants by tk:=sk+τt_k:=s_k+τ. All state trajectories are taken to be right-continuous at the impulse execution instants. Let h¯>0 h>0, let h:[s0,∞)→ℝh:[s_0,∞) be a time-varying delay, and let f,g:ℝn→ℝnf,g:R^n ^n be nonlinear functions. Consider the following n-dimensional leader: s˙(t)=−Cs(t)+Af(s(t))+Bg(s(t−h(t))), s(t)=-Cs(t)+Af(s(t))+Bg(s(t-h(t))), (1) where C,A,B∈ℝn×nC,A,B ^n× n. The iith follower, i=1,…,Ni=1,…,N, satisfies the hybrid dynamics x˙i(t)=−Cixi(t)+Aif(xi(t))+Big(xi(t−h(t)))+uic(t),t≠tk,Δxi(tk):=xi(tk+)−xi(tk−)=uip(tk),t=tk, \ aligned x_i(t)&=-C_ix_i(t)+A_if(x_i(t))+B_ig (x_i(t-h(t)) )+u_i^c(t),&&t≠ t_k,\\ x_i(t_k)&:=x_i(t_k^+)-x_i(t_k^-)=u_i^p(t_k),&&t=t_k, aligned . (2) where Ci,Ai,Bi∈ℝn×nC_i,A_i,B_i ^n× n may differ among the nodes. The terms uic(t)u_i^c(t) and uip(tk)u_i^p(t_k) denote the continuous and impulsive control inputs, respectively. The communication topology among the network nodes can switch and will be introduced below. Assumption 3.1. The time-varying delay h is absolutely continuous and satisfies 0≤h(t)≤h¯,h˙(t)≤δ<1a.e.0≤ h(t)≤ h, h(t)≤δ<1\,a.e. The nonlinear functions f and g are globally Lipschitz continuous. Namely, there exist lf,lg>0l_f,l_g>0 such that, for any x,y∈ℝnx,y ^n, ‖f(x)−f(y)‖≤lf‖x−y‖,‖g(x)−g(y)‖≤lg‖x−y‖.\|f(x)-f(y)\|≤ l_f\|x-y\|, \|g(x)-g(y)\|≤ l_g\|x-y\|. (3) 3.3 Key Idea: Recovery Window Andy adopts the following hybrid control idea. The network error is sampled, and impulsive control is applied after a prescribed execution delay. A recovery window whose length equals the upper bound on the time-varying state delay is then introduced. During this window, the continuous controller temporarily cancels the delay channel in the error system. When the window ends, the pre-impulse history has left the active delay interval. The delayed error channel is then reactivated, and the stability analysis resumes with the complete Lyapunov-Krasovskii functional. The continuous controller is designed as uic(t)= u_i^c(t)= (Ci−C)s(t)+(A−Ai)f(s(t))+(B−Bi)g(s(t−h(t))) (C_i-C)s(t)+(A-A_i)f(s(t))+(B-B_i)g(s(t-h(t))) −Ki(xi(t)−s(t))−(1−q(t))Bi[g(xi(t−h(t)))−g(s(t−h(t)))], -K_i (x_i(t)-s(t) )-(1-q(t))B_i [g(x_i(t-h(t)))-g(s(t-h(t))) ], (4) where Ki∈ℝn×nK_i ^n× n is the feedback gain. The phase indicator q(t)∈0,1q(t)∈\0,1\ is right-continuous, distinguishes the recovery phase from the normal-flow phase, and is coordinated with the impulse instants. Specifically, (i) choose the initial sampling instant s0s_0 such that q(s0−)=1q(s_0^-)=1, and set q(t)=1q(t)=1 on the initial interval [s0,t0)[s_0,t_0). (i) Set q(tk)=q(tk+)=0q(t_k)=q(t_k^+)=0 whenever t=tkt=t_k. (i) Keep q=0q=0 in the recovery window [tk,tk+h¯)[t_k,t_k+ h), and set q=1q=1 on [tk+h¯,tk+1)[t_k+ h,t_k+1). (iv) A topology switch that does not coincide with an impulse does not reset q. We next introduce impulsive control with a switching communication topology. First, consider the switching graphs. Let l be a positive integer, and let σ(t)∈:=1,…,lσ(t) :=\1,…,l\ be a left-continuous, piecewise constant switching signal. In mode r∈r , the communication graph rG_r is a connected undirected graph. Its Laplacian matrix is denoted by Lr=(ℓijr)N×N.L_r=( _ij^r)_N× N. Let aijra_ij^r denote the communication weight between nodes i and j in mode r. Then ℓijr=−aijr,i≠j,∑m≠iaimr,i=j. _ij^r= cases-a_ij^r,&i≠ j,\\[2.84526pt] _m≠ ia_im^r,&i=j. cases Let Nσ(t,u)N_σ(t,u) denote the number of topology switches in the interval [u,t)[u,t), and assume that Nσ(t,u)≤t−uTa+N0,t≥u≥s0,N_σ(t,u)≤ t-uT_a+N_0, t≥ u≥ s_0, (5) where Ta>0T_a>0 is the average dwell time and N0≥0N_0≥ 0 is the chatter bound. Assumption 3.2. The mode schedule satisfies σ(t)=rk:=σ(sk−),sk≤t≤tk+h¯,k≥0.σ(t)=r_k:=σ(s_k^-), s_k≤ t≤ t_k+ h, k≥ 0. (6) It also satisfies σ((tk+h¯)+)=rk,k≥0.σ ((t_k+ h)^+ )=r_k, k≥ 0. (7) Thus, the topology mode remains rkr_k from each sampling instant sks_k to the end of the corresponding recovery window. Its right limit at the endpoint of the recovery window is also rkr_k. In particular, no topology switching is allowed in [sk,tk+h¯][s_k,t_k+ h], including at tkt_k. An immediate switch to the right of the endpoint of the recovery window is also excluded. Choose the pinning matrix D=diag(d1,…,dN),di≥0,D=diag(d_1,…,d_N),d_i≥ 0, where di>0d_i>0 means that the iith follower has an additional leader-pinning channel in the impulsive coupling. When di=0d_i=0, the node receives the leader’s influence only indirectly through its neighbors in the impulsive topology. Given the impulse gain μk>0 _k>0, define the topology-dependent impulse mapping matrix Mk:=μk(Lσ(sk−)+D),M_k:= _k (L_σ(s_k^-)+D ), where the active topology immediately before the sampling instant sks_k is used. The mode-scheduling assumption in (6) and (7) avoids a mismatch between the sampling topology and the impulse execution topology. Remark 3.3. The impulsive control law selects the corresponding Laplacian matrix according to the active communication topology at the sampling instant. It is therefore a topology-dependent switching impulsive controller. This design can describe practical situations such as changes in adjacency relations caused by moving nodes, failures and recovery of communication links, and time-sharing schedules for wireless channels. The controller can then implement impulsive corrections according to the communication relations available at the sampling instant. Define the synchronization errors by ei(t):=xi(t)−s(t),e(t):=col(e1(t),…,eN(t)).e_i(t):=x_i(t)-s(t),e(t):=col(e_1(t),…,e_N(t)). Assume that the leader and follower state histories are continuous on [s0−h¯,s0][s_0- h,s_0]. Define the initial error segment by es0(θ):=e(s0+θ),θ∈[−h¯,0],e_s_0(θ):=e(s_0+θ), θ∈[- h,0], so es0∈([−h¯,0],ℝNn)e_s_0 ([- h,0],R^Nn), where C denotes the space of continuous functions. Define its norm by ‖es0‖h¯:=sup−h¯≤θ≤0‖e(s0+θ)‖.\|e_s_0\|_ h:= _- h≤θ≤ 0\|e(s_0+θ)\|. Let [z]i[z]_i denote the iith n-dimensional block of the stacked vector z∈ℝNnz ^Nn. Since the leader state s(t)s(t) is continuous at the impulse execution instants, the impulsive control input is designed as uip(tk) u_i^p(t_k) :=[(Mk⊗In)e(sk−)]i−ei(tk−) := [(M_k I_n)e(s_k^-) ]_i-e_i(t_k^-) (8) =−ei(tk−)+μk[∑j=1Naijσ(sk−)(ei(sk−)−ej(sk−))+diei(sk−)]. =-e_i(t_k^-)+ _k [ _j=1^Na_ij^σ(s_k^-) (e_i(s_k^-)-e_j(s_k^-) )+d_ie_i(s_k^-) ]. Since xi(tk)=xi(tk−)+uip(tk)x_i(t_k)=x_i(t_k^-)+u_i^p(t_k), the stacked error after impulse execution is e(tk)=(Mk⊗In)e(sk−).e(t_k)=(M_k I_n)e(s_k^-). (9) Substituting (4) into the leader and follower systems in (1) and (2) gives the unified closed-loop error system e˙i(t)=−(Ci+Ki)ei(t)+AiΔfi(t)+q(t)BiΔgi(t−h(t)),t≠tk,ei(tk)=[(Mk⊗In)e(sk−)]i,t=tk, \ aligned e_i(t)&=-(C_i+K_i)e_i(t)+A_i f_i(t)+q(t)B_i g_i(t-h(t)),&&t≠ t_k,\\ e_i(t_k)&= [(M_k I_n)e(s_k^-) ]_i,&&t=t_k, aligned . (10) where Δfi(t):=f(xi(t))−f(s(t)),Δgi(t−h(t)):=g(xi(t−h(t)))−g(s(t−h(t))). f_i(t):=f(x_i(t))-f(s(t)),\, g_i(t-h(t)):=g(x_i(t-h(t)))-g(s(t-h(t))). It follows from (10) that the delay channel in the error system is exactly canceled when q(t)=0q(t)=0. This delay channel is reactivated when q(t)=1q(t)=1. Furthermore, suppose that the error is identically zero at a given instant and throughout the required delay-history interval. Then Δfi(t)=0 f_i(t)=0 and Δgi(t−h(t))=0 g_i(t-h(t))=0, so the continuous flow satisfies e˙i(t)=0 e_i(t)=0. If e(sk−)=0e(s_k^-)=0, the impulse mapping gives e(tk)=(Mk⊗In)e(sk−)=0.e(t_k)=(M_k I_n)e(s_k^-)=0. Therefore, the continuous flow and the impulsive jumps both preserve the zero-error state. Once the system reaches synchronization, it remains synchronized. We next introduce self-triggered impulsive control. Let the triggering parameters be λ¯≥0 λ≥ 0 and ρ>0ρ>0, and the parameter sequence be akk≥0\a_k\_k≥ 0, where ak>0a_k>0. Assume additionally that τ≥h¯τ≥ h. The selected triggering parameter λ¯ λ will be further constrained in the theorem below by the Lyapunov matrices and their related constants. At the computed sampling instant sks_k, set Wk2:=eλ¯τW_k^2:=e λτ and define the self-triggering function for a candidate instant t≥tkt≥ t_k as Ψk(t):=(λ¯+ρ)(t−tk)−ak−lnWk2. _k(t):=( λ+ρ)(t-t_k)-a_k- W_k^2. (11) Since λ¯+ρ>0 λ+ρ>0, the function Ψk(t) _k(t) is strictly increasing in t. Therefore, the next sampling instant is defined as the first instant at which Ψk(t) _k(t) reaches a nonnegative value. Namely, sk+1:=inft>tk:Ψk(t)≥0.s_k+1:= \t>t_k: _k(t)≥ 0 \. (12) Define the time length from the kkth actual impulse execution instant tkt_k to the next sampling instant sk+1s_k+1 by Φk:=sk+1−tk=ak+lnWk2λ¯+ρ=ak+λ¯τλ¯+ρ. _k:=s_k+1-t_k= a_k+ W_k^2 λ+ρ= a_k+ λτ λ+ρ. (13) Hence, sk+1=tk+Φk=sk+τ+Φk,s_k+1=t_k+ _k=s_k+τ+ _k, Therefore, the sampling sequence and the impulse execution sequence are interlaced as s0<t0<s1<t1<⋯,s_0<t_0<s_1<t_1<·s, and tk+1−tk=sk+1−sk=τ+Φk>0.t_k+1-t_k=s_k+1-s_k=τ+ _k>0. Both the sampling intervals and the impulse execution intervals have the uniform strict positive lower bound τ. Thus, any finite time interval contains only finitely many sampling instants and impulse execution instants. Therefore, neither the self-triggered sampling sequence nor the impulse execution sequence exhibits Zeno behavior. Remark 3.4. The recovery-window feedback in (4) reveals a useful control-design idea. It matches a controller term with a difficult term in the error dynamics and removes that term during the part of the hybrid evolution in which it is most troublesome. Andy’s construction complements standard delay-analysis methods with a structural heuristic. It first identifies the term that makes the Lyapunov derivative difficult. The controller and the Lyapunov function are then co-designed so that this term is canceled or absorbed in a controlled phase. This principle also appears in PD-controlled multi-weighted networks. A derivative feedback term can be matched with a coupling-weighted quadratic term in the Lyapunov function so that the corresponding cross-derivative terms cancel pairwise [12, 13]. In PI designs, related weight terms can be balanced in an augmented Lyapunov functional [12]. A broader version of this idea appears in recursive adaptive control. Coordinate changes, parameter-update laws, and the feedback law are constructed step by step, and stability is established through a Lyapunov argument [14]. A related learning-based approach jointly trains a nonlinear controller and a neural Lyapunov function. An SMT-based falsification step checks the Lyapunov conditions and returns counterexamples when they fail [15]. These connections suggest that Andy’s control design can inform the construction of Lyapunov functions and PID-type controllers for systems with several coupling weights, delayed channels, or derivative couplings. Exact delay-channel cancellation in (4) is demanding in practice because it requires accurate knowledge of the delayed model and online access to the complete delayed states. Mature delay-system methods can retain the delayed channel and estimate its effect through Lyapunov-Krasovskii functionals, comparison arguments, and delayed impulsive inequalities [1, 16, 17]. When exact delayed states are unavailable, a natural extension is to use observer-based or adaptive approximate cancellation and bound the residual mismatch with standard delay-analysis tools. 3.4 Main Theorem For any candidate symmetric positive definite matrices Pr,Sr,Rr∈ℝn×nP_r,S_r,R_r ^n× n, constants λ1,r≥0 _1,r≥ 0, and scalars εi,r>0 _i,r>0 appearing in condition (i) below, where r∈r and i=1,…,Ni=1,…,N, define Qi,r:= Q_i,r:= Pr(Ci+Ki)+(Ci+Ki)Pr, P_r(C_i+K_i)+(C_i+K_i) TP_r, Λi,r(11):= _i,r^(11):= −Qi,r+2‖PrAi‖lfIn+εi,rIn+λmax(Sr)In+h¯λmax(Rr)In, -Q_i,r+2\|P_rA_i\|l_fI_n+ _i,rI_n+ _ (S_r)I_n+ h _ (R_r)I_n, Λi,r(22):= _i,r^(22):= εi,r−1‖PrBi‖2lg2In−(1−δ)λmin(Sr)In. _i,r^-1\|P_rB_i\|^2l_g^2I_n-(1-δ) _ (S_r)I_n. Further define βr(0) _r^(0) :=max1≤i≤N−λmin(Qi,r)+2‖PrAi‖lf,βr:=max0,βr(0)λmin(Pr), := _1≤ i≤ N \- _ (Q_i,r)+2\|P_rA_i\|l_f \, _r:= \0, _r^(0)\ _ (P_r), γr(0) _r^(0) :=max1≤i≤Nλmax(Qi,r)+2‖PrAi‖lf,γr:=max0,γr(0)λmin(Pr). := _1≤ i≤ N \ _ (Q_i,r)+2\|P_rA_i\|l_f \, _r:= \0, _r^(0)\ _ (P_r). Let χ~r χ_r :=e(βr+γr)h¯(1+h¯λmax(Sr)+h¯22λmax(Rr)λmin(Pr)), :=e^( _r+ _r) h (1+ h _ (S_r)+ h^22 _ (R_r) _ (P_r) ), χ~max χ_ :=maxr∈χ~r,β+:=maxr∈βr,λ¯1:=maxr∈λ1,r. := _r χ_r, _+:= _r _r, λ_1:= _r _1,r. For a candidate sequence ηkk≥0⊂(0,1)\ _k\_k≥ 0⊂(0,1) appearing in condition (i) below, define the effective contraction over the kkth impulsive period by c~k:=−lnηk−β+h¯−lnχ~max. c_k:=- _k- _+ h- χ_ . (14) For any α>0α>0, define αeff:=α+λ¯−λ¯1. _ eff:=α+ λ- λ_1. Theorem 3.5. Consider the systems in (1) and (2) under the continuous controller (4), the impulsive controller (8), and the self-triggering mechanism defined by (11) through (13). Assumption 3.1, the average dwell-time constraint (5), the execution-delay requirement τ≥h¯τ≥ h, and the mode-scheduling assumption in (6) and (7) are imposed throughout. If the following conditions hold: (i) For each switching mode r∈r , there exist symmetric positive definite matrices Pr,Sr,Rr∈ℝn×n,P_r,S_r,R_r ^n× n, and a constant λ1,r≥0 _1,r≥ 0 that is valid for all nodes. For every i=1,…,Ni=1,…,N, there exists εi,r>0 _i,r>0 such that [Λi,r(11)00Λi,r(22)]⪯λ1,r[Pr000], bmatrix _i,r^(11)&0\\ 0& _i,r^(22) bmatrix _1,r bmatrixP_r&0\\ 0&0 bmatrix, (15) In addition, λ¯≥maxλ¯1,β+. λ≥ \ λ_1, _+\. (i) There exists a sequence ηkk≥0⊂(0,1)\ _k\_k≥ 0⊂(0,1) such that, for every k≥0k≥ 0, the impulsive map satisfies MkMk⪯ηkIN.M_k TM_k _kI_N. (16) In addition, there exists a constant μ≥1μ≥ 1 such that, for all r,j∈r,j , Pr⪯μPj,Sr⪯μSj,Rr⪯μRj.P_r μ P_j, S_r μ S_j, R_r μ R_j. (17) (i) The self-triggering parameters satisfy ak>ρh¯,k≥0.a_k>ρ h, k≥ 0. (18) There exist constants α>0α>0 and φ>0 >0 such that, for all t≥u≥s0t≥ u≥ s_0, λ¯(t−u)+lnμTa(t−u)+∑k:u≤tk<t[−c~k+(λ¯+ρ)τ]≤−α(t−u)+φ. λ(t-u)+ μT_a(t-u)+ _k:\,u≤ t_k<t [- c_k+( λ+ρ)τ ]≤-α(t-u)+ . (19) Then αeff≥α>0 _ eff≥α>0, and the closed-loop system achieves global exponential leader-follower synchronization. Specifically, there exists a constant CGE≥1C_ GE≥ 1, independent of the initial history, such that every admissible initial history satisfies ‖e(t)‖≤CGE‖es0‖h¯e−αeff2(t−s0),t≥s0,\|e(t)\|≤ C_ GE\|e_s_0\|_ he^- _ eff2(t-s_0), t≥ s_0, (20) Proof. The stated regularity and non-Zeno timing assumptions ensure that the closed-loop system admits a unique global right-continuous solution. It remains to establish the exponential estimate. Fix matrices Pr,Sr,RrP_r,S_r,R_r and constants λ1,r,εi,r _1,r, _i,r satisfying condition (i). In each recovery window, construct the quadratic Lyapunov function r0(t):=e(t)(IN⊗Pr)e(t),V_r^0(t):=e T(t)(I_N P_r)e(t), (21) In each normal phase, construct the Lyapunov-Krasovskii functional r1(t):= _r^1(t):= e(t)(IN⊗Pr)e(t)+∫t−h(t)te(v)(IN⊗Sr)e(v)v+∫−h¯0∫t+θte(v)(IN⊗Rr)e(v)vθ. e T(t)(I_N P_r)e(t)+ _t-h(t)^te T(v)(I_N S_r)e(v)\,\,dv+ _- h^0 _t+θ^te T(v)(I_N R_r)e(v)\,\,dv\,\,dθ. (22) In the following, write (t)=σ(t)0(t) V(t)=V_σ(t)^0(t) when q(t)=0q(t)=0, and write (t)=σ(t)1(t) V(t)=V_σ(t)^1(t) when q(t)=1q(t)=1. The initialization of q gives q=1q=1 at s0−s_0^- and throughout [s0,t0)[s_0,t_0). For k≥1k≥ 1, the conditions τ≥h¯τ≥ h and (18) imply that q=1q=1 at each sampling instant sks_k and each pre-impulse instant tk−t_k^-. Thus, V is the full functional at these instants. First, consider the continuous flow in a recovery window. When q=0q=0 and the mode is fixed, (10) has no delay term. Its error trajectory is absolutely continuous. Hence, r0V_r^0 is also absolutely continuous. It follows from (21), the definition of Qi,rQ_i,r, and (3) that, for almost every t, ˙r0(t)= V_r^0(t)= ∑i=1N[−eiQi,rei+2eiPrAiΔfi]≤βr(0)∑i=1N‖ei‖2≤βrr0(t). _i=1^N [-e_i TQ_i,re_i+2e_i TP_rA_i f_i ]≤ _r^(0) _i=1^N\|e_i\|^2≤ _rV_r^0(t). (23) Similarly, ˙r0(t) V_r^0(t) ≥−γr(0)∑i=1N∥ei∥2≥−γr0(t). ≥- _r^(0) _i=1^N\|e_i\|^2≥- _rV_r^0(t). (24) Therefore, in the almost-everywhere sense, −γrr0(t)≤˙r0(t)≤βrr0(t)- _rV_r^0(t)≤ V_r^0(t)≤ _rV_r^0(t). Apply the standard Gronwall inequality to these two differential inequalities. In a recovery window with a fixed mode, for any tk≤u≤v≤tk+h¯t_k≤ u≤ v≤ t_k+ h, this gives r0(v)≤eβr(v−u)r0(u),r0(u)≤eγr(v−u)r0(v).V_r^0(v)≤ e _r(v-u)V_r^0(u), _r^0(u)≤ e _r(v-u)V_r^0(v). (25) Next, consider the continuous flow in a normal phase. Let ei,h:=ei(t−h(t))e_i,h:=e_i(t-h(t)). When q=1q=1, take the Dini derivative of the quadratic term in (22) along (10). We obtain D+[e(t)(IN⊗Pr)e(t)]=∑i=1N[−eiQi,rei+2eiPrAiΔfi+2eiPrBiΔgi(t−h(t))]. D^+\! [e T(t)(I_N P_r)e(t) ]= _i=1^N [-e_i TQ_i,re_i+2e_i TP_rA_i f_i+2e_i TP_rB_i g_i(t-h(t)) ]. The Lipschitz conditions and Young’s inequality give, respectively, 2eiPrAiΔfi≤2‖PrAi‖lf‖ei‖2, 2e_i TP_rA_i f_i≤ 2\|P_rA_i\|l_f\|e_i\|^2, 2eiPrBiΔgi(t−h(t))≤εi,r‖ei‖2+εi,r−1‖PrBi‖2lg2‖ei,h‖2. 2e_i TP_rB_i g_i(t-h(t))≤ _i,r\|e_i\|^2+ _i,r^-1\|P_rB_i\|^2l_g^2\|e_i,h\|^2. Apply the Leibniz rule to the single-integral term. Using h˙(t)≤δ h(t)≤δ, we obtain D+[∫t−h(t)te(v)(IN⊗Sr)e(v)v]≤λmax(Sr)∑i=1N‖ei‖2−(1−δ)λmin(Sr)∑i=1N‖ei,h‖2. D^+\! [ _t-h(t)^te T(v)(I_N S_r)e(v)\,\,dv ]≤ _ (S_r) _i=1^N\|e_i\|^2-(1-δ) _ (S_r) _i=1^N\|e_i,h\|^2. The Dini derivative of the double-integral term satisfies D+[∫−h¯0∫t+θte(v)(IN⊗Rr)e(v)vθ] D^+\! [ _- h^0 _t+θ^te T(v)(I_N R_r)e(v)\,\,dv\,\,dθ ] =h¯e(t)(IN⊗Rr)e(t)−∫t−h¯te(v)(IN⊗Rr)e(v)v = h\,e T(t)(I_N R_r)e(t)- _t- h^te T(v)(I_N R_r)e(v)\,\,dv ≤h¯λmax(Rr)∑i=1N‖ei‖2. ≤ h _ (R_r) _i=1^N\|e_i\|^2. Combining the above estimates gives the following bound for the Dini derivative of the full functional: D+r1(t)≤∑i=1N[eiΛi,r(11)ei+ei,hΛi,r(22)ei,h]. D^+V_r^1(t)≤ _i=1^N [e_i T _i,r^(11)e_i+e_i,h T _i,r^(22)e_i,h ]. (26) By (15), D+r1(t)≤λ1,re(t)(IN⊗Pr)e(t)≤λ1,rr1(t).D^+V_r^1(t)≤ _1,re T(t)(I_N P_r)e(t)≤ _1,rV_r^1(t). (27) Suppose that a switch from mode r to mode j occurs during a normal phase. Applying (17) term by term to (22) gives j1(t+)≤μr1(t−).V_j^1(t^+)≤ _r^1(t^-). (28) We next estimate the functional transition at the end of a recovery window. Let tk⋆:=tk+h¯t_k :=t_k+ h. Since h(tk⋆)≤h¯h(t_k )≤ h, all history involved in (22) at tk⋆t_k lies in the recovery window [tk,tk⋆][t_k,t_k ]. By (25), every v in this interval satisfies r0(v)≤e(βr+γr)h¯r0(tk⋆−).V_r^0(v)≤ e^( _r+ _r) hV_r^0(t_k -). (29) Moreover, ‖e(v)‖2≤r0(v)/λmin(Pr)\|e(v)\|^2 _r^0(v)/ _ (P_r). Hence, ∫tk⋆−h(tk⋆)tk⋆e(v)(IN⊗Sr)e(v)v≤e(βr+γr)h¯h¯λmax(Sr)λmin(Pr)r0(tk⋆−), _t_k -h(t_k )^t_k e T(v)(I_N S_r)e(v)\,\,dv≤ e^( _r+ _r) h h _ (S_r) _ (P_r)V_r^0(t_k -), ∫−h¯0∫tk⋆+θtk⋆e(v)(IN⊗Rr)e(v)vθ≤e(βr+γr)h¯h¯2λmax(Rr)2λmin(Pr)r0(tk⋆−). _- h^0 _t_k +θ^t_k e T(v)(I_N R_r)e(v)\,\,dv\,\,dθ≤ e^( _r+ _r) h h^2 _ (R_r)2 _ (P_r)V_r^0(t_k -). Therefore, the definition of χ~r χ_r and (7) yield r1((tk⋆)+)≤χ~rr0(tk⋆−).V_r^1((t_k )^+)≤ χ_rV_r^0(t_k -). (30) By (6) and (7), the mode rk=σ(sk−)=σ(tk−)r_k=σ(s_k^-)=σ(t_k^-) remains unchanged on [sk,tk+h¯][s_k,t_k+ h]. Using (9), (16), and the dominance of the full functional over its current-state quadratic term, we have rk0(tk+) _r_k^0(t_k^+) =e(sk−)(MkMk⊗Prk)e(sk−)≤ηke(sk−)(IN⊗Prk)e(sk−)≤ηkrk1(sk−). =e T(s_k^-)(M_k TM_k P_r_k)e(s_k^-)≤ _ke T(s_k^-)(I_N P_r_k)e(s_k^-)≤ _kV_r_k^1(s_k^-). (31) Successive application of (23), (30), and (14) gives rk1((tk+h¯)+) _r_k^1((t_k+ h)^+) ≤χ~maxeβ+h¯ηkrk1(sk−)=e−c~krk1(sk−). ≤ χ_ e _+ h _kV_r_k^1(s_k^-)=e^- c_kV_r_k^1(s_k^-). (32) By (18), τ≥h¯τ≥ h, and (13), Φk−h¯=ak−ρh¯+λ¯(τ−h¯)λ¯+ρ>0. _k- h= a_k-ρ h+ λ(τ- h) λ+ρ>0. (33) Thus, [tk+h¯,sk+1)[t_k+ h,s_k+1) is a nondegenerate normal phase. Let NkswN_k sw denote the number of switches in this interval. Combining (27), (28), and (32), we obtain (sk+1−)≤eλ¯1(Φk−h¯)−c~kμNksw(sk−). V(s_k+1^-)≤ e λ_1( _k- h)- c_kμ^N_k sw V(s_k^-). (34) Condition (6) excludes mode switches in all other intervals of the current cycle. Thus, NkswN_k sw is also the total number of switches in [sk,sk+1)[s_k,s_k+1). Iterate (34) and use ∑i=0k−1Φi=(sk−s0)−kτ,∑i=0k−1Nisw≤sk−s0Ta+N0, _i=0^k-1 _i=(s_k-s_0)-kτ,\, _i=0^k-1N_i sw≤ s_k-s_0T_a+N_0, to obtain ln(sk−)≤ V(s_k^-)≤ ln(s0−)+λ¯1[(sk−s0)−kτ−kh¯]−∑i=0k−1c~i+lnμTa(sk−s0)+N0lnμ. V(s_0^-)+ λ_1 [(s_k-s_0)-kτ-k h ]- _i=0^k-1 c_i+ μT_a(s_k-s_0)+N_0 μ. (35) Set u=s0u=s_0 and t=skt=s_k in (19). Then −∑i=0k−1c~i+lnμTa(sk−s0)≤−(α+λ¯)(sk−s0)−k(λ¯+ρ)τ+φ.- _i=0^k-1 c_i+ μT_a(s_k-s_0)≤-(α+ λ)(s_k-s_0)-k( λ+ρ)τ+ . (36) Substitute (36) into (35) and discard the nonpositive terms involving k. Let φeff:=φ+N0lnμ _ eff:= +N_0 μ. We obtain (sk−)≤eφeff(s0−)e−αeff(sk−s0). V(s_k^-)≤ e _ eff V(s_0^-)e^- _ eff(s_k-s_0). (37) We next estimate a uniform upper bound for the triggering intervals. Fix k and take 0<ε<Φk0< < _k. Set u=tk+εu=t_k+ and t=sk+1t=s_k+1 in (19). The interval [tk+ε,sk+1)[t_k+ ,s_k+1) contains no impulse and has length Φk−ε _k- . Hence, (α+λ¯+lnμTa)(Φk−ε)≤φ. (α+ λ+ μT_a )( _k- )≤ . Letting ε↓0 0 gives 0<Φk≤Φmax:=φα+λ¯+lnμTa<∞.0< _k≤ _ := α+ λ+ μT_a<∞. (38) Thus, Φk _k has the uniform upper bound required for the estimate over the entire time domain. We now extend the estimate at the sampling instants to all times. If t∈[sk,tk)t∈[s_k,t_k), then (27) and (6) give (t)≤eλ¯τ(sk−). V(t)≤ e λτ V(s_k^-). If t∈[tk,tk+h¯)t∈[t_k,t_k+ h), then (23) and (31) give (t)≤eβ+h¯(sk−)≤eλ¯h¯(sk−). V(t)≤ e _+ h V(s_k^-)≤ e λ h V(s_k^-). If t∈[tk+h¯,sk+1)t∈[t_k+ h,s_k+1), then (30), (27), (28), (5), and (38) give (t)≤χ~maxeβ+h¯+λ¯1ΦmaxμN0+Φmax/Ta(sk−). V(t)≤ χ_ e _+ h+ λ_1 _ μ^N_0+ _ /T_a V(s_k^-). Therefore, for every t∈[sk,sk+1)t∈[s_k,s_k+1), (t)≤Ccyc(sk−), V(t)≤ C_ cyc V(s_k^-), (39) where Ccyc:=max C_ cyc:= \ eλ¯τ,eλ¯h¯,χ~maxeβ+h¯+λ¯1ΦmaxμN0+Φmax/Ta. e λτ,e λ h, χ_ e _+ h+ λ_1 _ μ^N_0+ _ /T_a \. (40) Moreover, t−sk<τ+Φmaxt-s_k<τ+ _ . It follows from (37) and (39) that (t)≤Ccyceφeff+αeff(τ+Φmax)(s0−)e−αeff(t−s0). V(t)≤ C_ cyce _ eff+ _ eff(τ+ _ ) V(s_0^-)e^- _ eff(t-s_0). (41) Define p¯ p :=minr∈λmin(Pr), := _r _ (P_r), Ch C_h :=maxr∈λmax(Pr)+h¯maxr∈λmax(Sr)+h¯22maxr∈λmax(Rr). := _r _ (P_r)+ h _r _ (S_r)+ h^22 _r _ (R_r). By (21) and (22), (t)≥p¯‖e(t)‖2,(s0−)≤Ch‖es0‖h¯2. V(t)≥ p\|e(t)\|^2, V(s_0^-)≤ C_h\|e_s_0\|_ h^2. (42) Substituting (42) into (41) gives (20), where we can take CGE:=(CcycChp¯)1/2exp[φeff+αeff(τ+Φmax)2].C_ GE:= ( C_ cycC_h p )^1/2 \! [ _ eff+ _ eff(τ+ _ )2 ]. (43) Since ei(t)=xi(t)−s(t)e_i(t)=x_i(t)-s(t), (20) shows that every follower error ei(t)e_i(t) converges to zero at an exponential rate of at least αeff/2 _ eff/2. Therefore, the closed-loop system achieves global exponential leader-follower synchronization. ∎ Remark 3.6. When γr(0)≤0 _r^(0)≤ 0 holds for every mode, γr=0 _r=0. The phase-transition factor χ~r χ_r then automatically reduces to its original form without the bidirectional growth compensation. This reduction leaves all other conditions of the theorem and the proof structure unchanged. 3.5 Numerical Verification Example 3.1. Consider one three-dimensional leader and five three-dimensional heterogeneous followers. The nonlinear functions are applied componentwise and are chosen as f(z)=g(z)=tanh(z),lf=lg=1.f(z)=g(z)= (z),\,l_f=l_g=1. The matrices of the leader system are C=diag(0.45,0.50,0.55),B=diag(0.12,0.10,0.09),C=diag(0.45,0.50,0.55),\,B=diag(0.12,0.10,0.09), and A=[1.05−0.250.150.200.95−0.20−0.150.251.00].A= bmatrix1.05&-0.25&0.15\\ 0.20&0.95&-0.20\\ -0.15&0.25&1.00 bmatrix. The follower matrices are diagonal and are chosen as C1 C_1 =diag(0.30,0.36,0.42), =diag(0.30,0.36,0.42), A1 A_1 =diag(1.20,0.95,1.05), =diag(1.20,0.95,1.05), B1 B_1 =diag(0.15,0.10,0.12), =diag(0.15,0.10,0.12), C2 C_2 =diag(0.34,0.31,0.46), =diag(0.34,0.31,0.46), A2 A_2 =diag(1.10,1.18,0.92), =diag(1.10,1.18,0.92), B2 B_2 =diag(0.11,0.14,0.09), =diag(0.11,0.14,0.09), C3 C_3 =diag(0.38,0.44,0.32), =diag(0.38,0.44,0.32), A3 A_3 =diag(0.98,1.08,1.15), =diag(0.98,1.08,1.15), B3 B_3 =diag(0.13,0.08,0.15), =diag(0.13,0.08,0.15), C4 C_4 =diag(0.33,0.48,0.37), =diag(0.33,0.48,0.37), A4 A_4 =diag(1.16,1.02,1.10), =diag(1.16,1.02,1.10), B4 B_4 =diag(0.10,0.12,0.14), =diag(0.10,0.12,0.14), C5 C_5 =diag(0.41,0.35,0.50), =diag(0.41,0.35,0.50), A5 A_5 =diag(1.05,1.12,1.19), =diag(1.05,1.12,1.19), B5 B_5 =diag(0.14,0.15,0.11). =diag(0.14,0.15,0.11). The continuous feedback gains are Ki=1.20I3K_i=1.20I_3 for i=1,…,5i=1,…,5. The time-varying delay is h(t)=0.075+0.025sin(0.8t),h(t)=0.075+0.025 (0.8t), so 0.05≤h(t)≤h¯=0.100.05≤ h(t)≤ h=0.10 and maxth˙(t)=0.02<δ=0.05<1 _t h(t)=0.02<δ=0.05<1. The two switching topologies are a five-node ring and a star centered at follower 3. Their Laplacian matrices are L1=[2−100−1−12−1000−12−1000−12−1−100−12],L2=[10−10001−100−1−14−1−100−11000−101].L_1= bmatrix2&-1&0&0&-1\\ -1&2&-1&0&0\\ 0&-1&2&-1&0\\ 0&0&-1&2&-1\\ -1&0&0&-1&2 bmatrix, L_2= bmatrix1&0&-1&0&0\\ 0&1&-1&0&0\\ -1&-1&4&-1&-1\\ 0&0&-1&1&0\\ 0&0&-1&0&1 bmatrix. Only follower 1 has a direct pinning channel, and hence D=diag(1,0,0,0,0)D=diag(1,0,0,0,0). For the impulsive controller, choose μk=0.05,ηk=0.07,τ=1.00,λ¯=0,ρ=0.10,ak=0.10 _k=0.05, _k=0.07,τ=1.00, λ=0,ρ=0.10,a_k=0.10. The switch in each cycle is scheduled at sk+1.50s_k+1.50 s, after the protected interval ends at sk+τ+h¯=sk+1.10s_k+τ+ h=s_k+1.10 s. The two impulsive topology modes alternate over successive triggering cycles. The switching parameters are Ta=2.00T_a=2.00 and N0=1N_0=1. The Lyapunov parameters are selected as Pr=I3,Sr=0.25I3,Rr=0.05I3,εi,r=0.10,P_r=I_3,S_r=0.25I_3,R_r=0.05I_3, _i,r=0.10, for both modes, with λ1,r=0,μ=1,α=0.80,φ=1.97. _1,r=0,μ=1,α=0.80, =1.97. The initial histories are constant on [−0.10,0][-0.10,0]. They are specified by s(θ)=[0.60−0.400.80],[e1(θ)e2(θ)e3(θ)e4(θ)e5(θ)]=[51−342−2−5−2010−1−7−31],−0.10≤θ≤0.s(θ)= bmatrix0.60&-0.40&0.80 bmatrix T, bmatrixe_1 T(θ)\\ e_2 T(θ)\\ e_3 T(θ)\\ e_4 T(θ)\\ e_5 T(θ) bmatrix= bmatrix5&1&-3\\ 4&2&-2\\ -5&-2&0\\ 1&0&-1\\ -7&-3&1 bmatrix, -0.10≤θ≤ 0. These values satisfy all conditions of Theorem 3.5. Therefore, the network achieves global exponential leader-follower synchronization under the proposed hybrid control. Figure 2 shows that all synchronization errors converge to zero under the hybrid control. The maximum error at t=12t=12 s is 4.3163×10−74.3163× 10^-7. For comparison, all control and inter-node coupling are removed in Figure 3. The error curves remain separated, and the maximum error at t=12t=12 s is approximately 8.45278.4527. Figure 2: Synchronization errors ‖xi(t)−s(t)‖2\|x_i(t)-s(t)\|_2 of the five followers under the proposed hybrid control. Figure 3: Synchronization errors ‖xi(t)−s(t)‖2\|x_i(t)-s(t)\|_2 of the five followers without control. 4 Conclusion Andy provides an end-to-end workflow that turns a mathematical problem into a traceable proof. It organizes proof steps in an executable DAG, binds each local verification result to a certificate, uses node interfaces to confine repairs to the affected proof region, and records the complete path from problem formulation to final proof. The system separates proof generation from correctness evaluation and can acquire, retain, retrieve, and reuse knowledge from existing results. The case study shows that Andy can develop a technically meaningful problem from an established result and carry it through theorem construction, proof, and numerical illustration. Starting from the self-triggered impulsive consensus result in [1], Andy formulated a global exponential leader-follower synchronization problem for delayed heterogeneous networks with switching communication topologies. The control-theoretic contribution is the recovery-window design. After each delayed impulse, model-matching feedback temporarily removes the delayed error channel until the pre-impulse history leaves the active delay interval. This separation permits a quadratic Lyapunov estimate during recovery and restores the full Lyapunov-Krasovskii functional afterward. It brings switching topology, impulse execution delay, and self-triggered updates into one exponential-synchronization proof. Sufficient conditions were established, Zeno behavior was excluded for both timing sequences, and the numerical example illustrates the expected synchronization behavior. Future work will investigate CrewAI-style role-based multi-agent orchestration in which the solver, evaluator, and human-like monitor operate as distinct agents. Independent roles can reduce correlated self-evaluation errors and make disagreements explicit. Parallel exploration can increase proof-route coverage and shorten the time spent on unsuccessful branches. Role-specific messages and certificates can also improve traceability, while dynamic routing, escalation, and cross-checking can make the workflow more robust to errors from a single model or reasoning route. References [1] S. Hong, Y. Zhang, Consensus of switched delay multi-agent systems via self-triggered impulsive control, International Journal of Control 95 (12) (2022) 3252–3261. doi:10.1080/00207179.2021.1970815. [2] B. Romera-Paredes, M. Barekatain, A. Novikov, M. Balog, M. P. Kumar, E. Dupont, F. J. R. Ruiz, J. S. Ellenberg, P. Wang, O. Fawzi, P. Kohli, A. Fawzi, Mathematical discoveries from program search with large language models, Nature 625 (2024) 468–475. doi:10.1038/s41586-023-06924-6. [3] T. H. Trinh, Y. Wu, Q. V. Le, H. He, T. Luong, Solving olympiad geometry without human demonstrations, Nature 625 (2024) 476–482. doi:10.1038/s41586-023-06747-5. [4] X. Chen, X. Jiang, Moonshine: An autonomous mathematical research agent centered on conjecture generation (2026). arXiv:2606.10806. URL https://arxiv.org/abs/2606.10806 [5] Z. Zhao, B. Yuan, J. Choi, Y. Chen, RMA: An agentic system for research-level mathematical problems (2026). arXiv:2605.22875. URL https://arxiv.org/abs/2605.22875 [6] C. An, Q. Ye, M. Pan, J. Zhang, QED: An open-source multi-agent system for generating mathematical proofs on open problems (2026). arXiv:2604.24021. URL https://arxiv.org/abs/2604.24021 [7] J. Schmitt, T. Gehrunger, J. Dekoninck, G. Bérczi, U. Kreitner, L. Price, D. Holmes, ProofCouncil: An LLM agent for solving open mathematical problems (2026). arXiv:2607.09474. URL https://arxiv.org/abs/2607.09474 [8] J. Liu, G. Gao, Z. Sun, B. Wu, S. Liu, J. Jiang, H. Ju, L. Chen, R. Cheng, X. Zhang, B. Dong, Danus: Orchestrating mathematical reasoning agents with fact-graph memory (2026). arXiv:2607.06447. URL https://arxiv.org/abs/2607.06447 [9] H. Ju, G. Gao, J. Jiang, B. Wu, Z. Sun, S. Liu, L. Chen, Y. Wang, Y. Wang, Z. Wang, W. He, P. Wu, L. Xiao, R. Liu, B. Dai, B. Dong, Automated conjecture resolution with formal verification (2026). arXiv:2604.03789. URL https://arxiv.org/abs/2604.03789 [10] Y. Cao, R. Qiu, J. Liu, J. Wang, D. Guo, R. Feng, L. Zhi, X.-S. Gao, Mechmath agent team: LLM driven agents for mathematical research (2026). arXiv:2607.04394. URL https://arxiv.org/abs/2607.04394 [11] J. Pearl, Probabilistic Reasoning in Intelligent Systems: Networks of Plausible Inference, Morgan Kaufmann, San Mateo, CA, 1988. [12] J.-L. Wang, L.-H. Zhao, PD and PI control for passivity and synchronization of coupled neural networks with multi-weights, IEEE Transactions on Network Science and Engineering 8 (1) (2021) 790–802. doi:10.1109/TNSE.2021.3052889. [13] J.-L. Wang, L.-H. Zhao, H.-N. Wu, T. Huang, Finite-time passivity and synchronization of multi-weighted complex dynamical networks under PD control, IEEE Transactions on Neural Networks and Learning Systems 35 (1) (2024) 507–518. doi:10.1109/TNNLS.2022.3175747. [14] I. Kanellakopoulos, P. V. Kokotović, A. S. Morse, Systematic design of adaptive controllers for feedback linearizable systems, IEEE Transactions on Automatic Control 36 (11) (1991) 1241–1253. doi:10.1109/9.100933. [15] R. Zhou, T. Quartz, H. De Sterck, J. Liu, Neural Lyapunov control of unknown nonlinear systems with stability guarantees, in: Advances in Neural Information Processing Systems, Vol. 35, 2022, p. 29113–29125. doi:10.52202/068431-2111. [16] L. Zhang, J. Lu, F. Liu, J. Lou, Synchronization of time-delay coupled neural networks with stabilizing delayed impulsive control, IEEE Transactions on Neural Networks and Learning Systems 35 (12) (2024) 18899–18906. doi:10.1109/TNNLS.2023.3320651. [17] X. Xie, X. Li, S. Song, X. Liu, A self-triggered impulsive approach to group consensus of MASs with sensing/actuation delays, IEEE Transactions on Systems, Man, and Cybernetics: Systems 54 (2) (2024) 1168–1179. doi:10.1109/TSMC.2023.3326830. Appendix A Research Trace of the Case Study This appendix records the main research decisions made during the case study. It summarizes the problem-revision history, the low-cost exploration of proof routes, the construction of the proof dependency graph, and the selection of the final proof chain. A.1 Problem Revision and Research-Value Evaluation The evaluator recorded nine consecutive versions of the proposed research problem, indexed from 0 to 8. Thus, the initial proposal was followed by eight revision cycles. Each version was scored for importance, originality, feasibility, and coherence. Acceptance required a weighted total of at least 7.57.5, a score of at least 66 in every dimension, and a single research objective that could be answered by one principal conclusion. Table 2 gives the complete evaluation trace. Table 2: Evaluation trace for the proposed research problem. Version Imp. Orig. Feas. Coh. Total 0 6.5 6 6 5.5 6.07 1 6 5 3 4 4.65 2 7 7 6 7 6.75 3 7 8 6 7 7.05 4 8 8 7 8 7.75 5 8 8 7 8 7.75 6 8 8 7 8 7.75 7 8 8 7 8 7.75 8 8 8 7 8 7.75 Example A.1. In Version 1, Andy proposed the following problem. Consider a leader and N heterogeneous followers governed by s˙(t) s(t) =−Cs(t)+Af(s(t))+Bg(s(t−h(t))), =-Cs(t)+Af(s(t))+Bg(s(t-h(t))), x˙i(t) x_i(t) =−Cixi(t)+Aif(xi(t))+Big(xi(t−h(t)))+uic(t)+uip(t), =-C_ix_i(t)+A_if(x_i(t))+B_ig(x_i(t-h(t)))+u_i^c(t)+u_i^p(t), with ei=xi−se_i=x_i-s, use the manifold-compensation feedback uic=(Ci−C)s+(A−Ai)f(s)+(B−Bi)g(s(t−h(t)))−Kieiu_i^c=(C_i-C)s+(A-A_i)f(s)+(B-B_i)g(s(t-h(t)))-K_ie_i. At each delayed impulse time tk=sk+τt_k=s_k+τ, impose e(tk+)=(Mk⊗In)e(sk−)e(t_k^+)=(M_k I_n)e(s_k^-). For the switching quadratic function V(t)=e(t)(IN⊗Pσ(t))e(t)V(t)=e T(t)(I_N P_σ(t))e(t), introduce the scalar comparison system W˙=λ¯1W+κ W= λ_1W+κ between impulses and W(tk)=ηkW(sk−)W(t_k)= _kW(s_k^-) at impulses. Generate the next sampling time from sk+1=inft>sk+τ:t−sk−τ−Φ(k,Wk2)≥0,Φ(k,Wk2)=ak+lnWk2λ¯1+ρ.s_k+1= \t>s_k+τ:t-s_k-τ- (k,W_k^2)≥ 0 \, (k,W_k^2)= a_k+ W_k^2 λ_1+ρ. The task was to select the controller and triggering parameters so that the switching, impulse-contraction, and cumulative-decay conditions guaranteed global exponential leader-follower synchronization and a uniform positive lower bound on the intersampling intervals. This version received scores of 66, 55, 33, and 44 for importance, originality, feasibility, and coherence, respectively, with a total score of 4.654.65. Feasibility was the principal failure. The proposed argument claimed that a fixed constant κ could absorb the delayed state-dependent term λ2W(t−h(t)) _2W(t-h(t)). Such a constant cannot dominate that term while the same comparison system is required to converge to zero. The Halanay-Li comparison bridge therefore did not close. The impulsive condition also constrained only the instantaneous quadratic term and did not control the history terms of a complete Lyapunov-Krasovskii functional. Coherence fell below the threshold because the delay, switching, and impulsive mechanisms were not connected by one valid estimate, and the required condition h˙(t)≤δ<1 h(t)≤δ<1 had not been stated. The originality score was also below the threshold because the claimed integration of the mechanisms depended on this invalid step and two literature attributions were incomplete. The evaluator recommended removing the additive-constant absorption step, constructing an explicit mode-dependent Lyapunov-Krasovskii functional, adding the delay-derivative assumption, deriving verifiable block matrix inequalities, and treating the jump of the complete functional at impulsive instants. It also requested a concrete intermediate lemma that connected the flow, delay, and impulse estimates before the revised problem proceeded to full proof execution. Versions 4 through 7 had already cleared every numerical threshold. They were rejected solely because the proposal still presented several parallel subquestions as separate targets. The final revision retained the mathematical content and reorganized these requests into one objective: establish global exponential leader-follower synchronization under a unified switching hybrid-control theorem. A.2 Low-Cost Route Exploration and DAG Construction The route planner first explored several strategies at low computational cost. The first round considered scalar comparison domination, direct interval-wise Lyapunov stitching, and a discrete impulse-map approach. The second round refined the comparison route into a Li-type scalar comparison argument with a cumulative condition and also considered multiple-Lyapunov stitching, unified growth-rate absorption, and a direct impulsive Gronwall-Halanay recurrence. These two rounds produced seven route records. The comparison route received the highest feasibility assessment and became the main route. The strongest structurally different candidates were retained as backups. The discrete-map and unified-growth approaches were discarded because they either lost essential delay and switching information or introduced excessive conservatism. The seven records therefore represent broad preliminary exploration, while only three route families were promoted to executable branches. A.3 Proof-Node Responsibilities and Exact Dependencies Here and below, NiN_i denotes the iith proof node in the execution plan. Each proof node is a mathematical work unit with a specified input, conclusion, dependency set, and verification criterion. The subscript i is a stable node identifier; model iterations, difficulty levels, and branch numbers use different notation. The notation Ni-rjN_i-r_j denotes the immutable jjth revision of node NiN_i. Table 3 defines every node. Table 3: Proof-node responsibilities, direct dependencies, and final records. Node Responsibility Direct predecessors Record N1N_1 Two-stage error system, recovery-window controller, and impulsive error map None Frozen at r2r_2 N2N_2 Recovery-window quadratic growth bound N1N_1 Frozen at r1r_1 N3N_3 Normal-phase LKF Dini-derivative estimate N1N_1 Frozen at r1r_1 N4N_4 Impulse jump estimate and effective contraction factor N1N_1 Frozen at r1r_1 N5N_5 Interface between the recovery and normal phases N1,N2N_1,N_2 Frozen at r5r_5 N6N_6 Li-type scalar comparison dominating the full functional N2,N3,N4,N5N_2,N_3,N_4,N_5 Invalidated N7N_7 Cauchy factor and exponential-decay estimate N6N_6 Invalidated N8N_8 Main-branch theorem assembly N7N_7 Invalidated N9N_9 Direct interval-wise stitching without a scalar comparator N2,N3,N4,N5N_2,N_3,N_4,N_5 Failed after r3r_3 N10N_10 First backup-theorem assembly N9N_9 Not run; invalidated N11N_11 Direct impulsive Gronwall-Halanay cumulative recurrence N2,N3,N4,N5N_2,N_3,N_4,N_5 Frozen at r2r_2 N12N_12 Final synchronization-theorem assembly N11N_11 Frozen at r4r_4 The common prefix of the graph contained the system reduction and the four estimates needed by every branch. The planner then attached three alternative tails to this verified prefix. Figure 4 shows the resulting execution graph. N1N_1N2N_2N3N_3N4N_4N5N_5N6N_6N7N_7N8N_8N9N_9N10N_10N11N_11N12N_12 Figure 4: Executed proof DAG. Node responsibilities and direct predecessors are listed in Table 3. Green nodes were verified and frozen, red marks the failed backup node, and gray nodes were invalidated after an upstream change or branch failure. A.4 Failed Branches and Final Route Selection The main branch comprised N6N_6, N7N_7, and N8N_8. During the repair of N5N_5, the interface factor was replaced by the corrected mode-dependent quantity χ~r χ_r. This change altered the dependency fingerprint of the downstream comparison construction. The three nodes were therefore invalidated before further execution. Their invalidation records an upstream interface change and leaves the local validity of individual statements in the abandoned branch undecided. The first backup branch failed at N9N_9 after three revisions. The first revision contained a sign error in the logarithmic exponent and counted the average-dwell-time chatter term twice. The second introduced an undeclared maximum interval and omitted a time-dependent switching factor. The third relied on an unavailable growth-rate inequality, counted the recovery cost twice, and omitted switches between a sampling instant and its delayed impulse. These failures showed that direct interval stitching was too fragile for the coupled recovery, delay, and switching interfaces. Consequently, N10N_10 was never executed. The second backup branch retained the interval estimates and changed only their assembly mechanism. The first revision of N11N_11 omitted the corrected phase condition and did not verify that the normal interval had nonnegative length. Its second revision used χ~max χ_ , added the required trigger margin, and completed the cumulative recurrence. The first three revisions of N12N_12 still exposed mismatches between the theorem statement and the verified proof interface. Revision 44 made the actual assumptions explicit and passed independent verification. The final proof chain was therefore N1-r2⟶N2-r1,N3-r1,N4-r1⟶N5-r5⟶N11-r2⟶N12-r4.N_1-r_2 \N_2-r_1,N_3-r_1,N_4-r_1\ N_5-r_5 N_11-r_2 N_12-r_4. The braces indicate that N2N_2, N3N_3, and N4N_4 were verified in parallel. The dependency of N5N_5 was limited to N1N_1 and N2N_2, while N11N_11 used all four shared estimates N2N_2 through N5N_5. At the end of the run, seven nodes were frozen, one node had failed, and four nodes had been invalidated. The graph contained nineteen immutable node revisions, which preserved the complete repair history while allowing the verified prefix to be reused.