Higher Monads and Recursive Improvement
Manuscript and scope
The accompanying PDF is the full manuscript, with mathematical proofs, a substantial higher categorical neural-network example, two appendices, and twelve references. This journal body is a condensed guide to the full paper. It is not a claim that the paper has already been reviewed or accepted.
Recursive improvement is modeled as change to a system together with change to the procedure that proposes its subsequent changes. We distinguish updates to model parameters, architecture, optimizer representation, and improvement language. An objective and an admissibility contract remain explicitly fixed during each guarantee.
The principal contribution is the organization of established higher-monad and free-monad foundations into a constrained recursive-improvement specification, with application-level preservation results, a common carrier connecting syntax to certified histories, a detailed neural example, and explicit obstructions. We do not claim new foundational constructions of higher monads, free monads, or initial algebras.
1. Higher monads and directed histories
A higher monad on an infinity-category $\mathcal C$ is an associative algebra in the composition monoidal infinity-category of endofunctors:
$$T\in \operatorname{Alg}_{E_1}(\operatorname{Fun}(\mathcal C,\mathcal C)).$$
The unit and multiplication include their full homotopy coherent structure. Checking only the unit equations and one associativity equation would not establish this structure.
Let $\mathcal E$ be an infinity-topos and $S$ its object of states. The object $S$ records invertible state symmetries; directed changes are edges of a graph $G\to S\times S$. A certified edge includes preservation of a predicate $I$ and an inequality $J(t)\leq J(s)$ for a fixed ordered objective.
On $\mathcal E_{/S\times S}$, convolution is
$$(G\otimes_S H)(s,t)=\sum_{u:S}G(s,u)\times H(u,t).$$
It preserves colimits separately, so the free associative object is
$$\mathsf{Path}_S(G)=\coprod_{n\geq 0}G^{\otimes_S n}.$$
The associated higher monad inserts one edge and flattens paths of paths. Its algebras are coherent internal composition structures with specified state object. They are Segal presentations; completeness, when needed, is a separate completion.
Finite preservation. Every finite path of primitive invariant-preserving, nonincreasing edges has the same two properties. The proof composes predicate implications and order inequalities. It assumes the primitive certificates and does not infer that a nonidle improving step exists.
2. Recursive typed programs and a metamonad
For a presentable $\mathcal C$ and sequentially continuous endofunctor $P$, form the chain
$$Y_0=0,\qquad Y_{n+1}=X\amalg P(Y_n),\qquad T_PX=\operatorname*{colim}_{n<\omega}Y_n.$$
Sequential continuity identifies the colimit with $X\amalg P(T_PX)$. Its initial-algebra property supplies the free higher monad on $P$. Its unit returns an output; its multiplication substitutes programs at returned program values. These units differ from the edge-insertion unit of the graph monad.
A dependent signature is represented by
$$K\xleftarrow{s}E\xrightarrow{p}B\xrightarrow{t}K,\qquad P=\Sigma_t\Pi_p\Delta_s.$$
For finite locally constant discrete fibers of $p$, the polynomial preserves sequential colimits. Colors record endpoint states and compatible architecture and optimizer types. The resulting trees are finite well-founded syntax, not completed infinite executions.
The free-forgetful adjunction $F\dashv U$ from sequentially continuous endofunctors to monads induces a metamonad $\mathbb M=UF$ on the endofunctor category:
$$\mathbb M(P)=T_P,\qquad \mathbb M^2(P)=T_{T_P}\longrightarrow T_P.$$
Its multiplication expands operation labels that are themselves programs. This is distinct from substituting program-valued outputs under $T_P^2X\to T_PX$. Both expansions preserve an interpretation coherently. Neither expansion alone establishes better performance or increased computational power.
Common history carrier. For a fixed certified primitive graph $G$, the monad
$$\mathsf H_G(X)=\mathsf{Path}_S(G\amalg X)$$
freely adjoins variable edges to $G$. It is induced by the adjunction for internal categories equipped with a chosen map from $G$. A typed instruction interpretation $P\Rightarrow\mathsf H_G$ extends to a monad morphism $T_P\to\mathsf H_G$. At the empty variable graph it gives $T_P0\to\mathsf{Path}_SG$. This makes interpretation into certified histories explicit on a single carrier.
3. Self-modifying policies and admissibility
A state may have the dependent shape
$$s=(a,w,o,m,h),$$
where $a$ is architecture, $w$ model parameters, $o$ optimizer representation, $m$ optimizer memory, and $h$ retained history. A recursively changing policy reads $o$ while proposing its successor. The outer transition law and the fixed acceptance interpretation stay defined.
A proof-carrying proposal has type
$$1+\sum_{t:S}\mathsf{Cert}(s,t).$$
The first summand idles. The second supplies a candidate and evidence. This does not assume a decision procedure for all internal propositions.
Admissible-lift theorem. Let $j:\mathcal C_I\hookrightarrow\mathcal C$ be fully faithful and let $Tj\simeq jT_I$ coherently restrict a monad. Assume $\mathcal C_I$ is presentable and its restricted signature preserves sequential colimits. A primitive interpretation $P_I\Rightarrow T_I$ extends to $T_{P_I}\Rightarrow T_I$. All finite program substitutions and Kleisli composites remain inside $\mathcal C_I$. The proof combines the free universal property with closure of Kleisli composition.
A coherent monad morphism also induces a translation between Kleisli categories. Preservation of loss or cost additionally requires preservation of their interpretations; it is not implied solely by preservation of returned functions.
4. Compatible extension, budgets, and context
Sequential-extension theorem. For a sequence of sequentially continuous monads and coherent monad morphisms $T_0\to T_1\to\cdots$, the pointwise colimit $T_\infty X=\operatorname*{colim}_nT_nX$ is a higher monad in the same class. Its multiplication follows from
$$T_\infty T_\infty X\simeq\operatorname*{colim}_{i,j}T_iT_jX\simeq\operatorname*{colim}_kT_k^2X\longrightarrow\operatorname*{colim}_kT_kX.$$
The diagonal of the pair-indexing category is cofinal. Applying the same argument to every finite arity carries the coherent algebra structure. Invariants pass to this extension when the admissible inclusion creates the sequential colimits. This is a limit of languages, not a convergence theorem about a selected optimizer run.
Costs of primitive changes add along paths. Budget-restricted composition therefore takes grades $r,s$ to grade $r+s$. A fixed budget is not automatically closed under ordinary monad multiplication.
Geometric base change. For a geometric inverse image $f^*$, finite-limit and colimit preservation give
$$f^*\mathsf{Path}_S(G)\simeq\mathsf{Path}_{f^*S}(f^*G).$$
For finite locally constant discrete input fibers, the corresponding polynomial comparison and initial-chain argument also give $f^*T_PX\simeq T_{P'}f^*X$. General dependent products are excluded unless the needed comparison is supplied. These statements transport syntax and evidence; they do not establish statistical robustness under distribution change.
5. Numerical results require numerical hypotheses
If an accepted run satisfies
$$J(s_{n+1})\leq J(s_n)-a_n+b_n,\qquad J\geq J_*,\qquad a_n,b_n\geq0,$$
then telescoping gives
$$\sum_{n<N}a_n\leq J(s_0)-J_*+\sum_{n<N}b_n.$$
For an $M$-Lipschitz gradient on the used segments, every step $w'=w-\eta\nabla L(w)$ satisfies
$$L(w')\leq L(w)-\eta(1-M\eta/2)\|\nabla L(w)\|^2.$$
If the changing proposer always supplies executed step sizes in $[\underline\eta,\overline\eta]\subset(0,2/M)$ and the loss is bounded below, put $c=\underline\eta(1-M\overline\eta/2)$. Then
$$\min_{n<N}\|\nabla L(w_n)\|^2\leq \frac{L(w_0)-L_*}{cN}.$$
The gradient norm tends to zero along an infinite run satisfying these hypotheses; every cluster point is stationary. The argument does not prove state convergence, global optimality, infinitely frequent acceptance, or transfer across changing dimensions.
There is also an expected-progress statement: for nonnegative adapted integrable variables with conditional decrease $\mathbb E[J_{n+1}\mid\mathcal F_n]\leq J_n-a_n+b_n$ and summable $\mathbb E b_n$, telescoping and monotone convergence imply $\sum_na_n<\infty$ almost surely. The conditional inequality is assumed for the actual changing policy.
6. A substantial neural-network example
Interfaces are finite-dimensional real vector spaces. Network 1-cells are finite typed smooth circuits with parameter spaces $W_A$; invertible 2-cells are exact hidden-coordinate symmetries. Nerves of the hom groupoids give a genuine higher category. At the zero tuple of a width-$m$ hidden layer, the isotropy group is $S_m$, which a set quotient would erase.
For $F(x)=B\sigma(Ax+a)+b$, the permutation action is
$$A'=\Pi A,\quad a'=\Pi a,\quad B'=B\Pi^{-1},\quad b'=b.$$
Direct substitution proves exact equality of represented functions. An invariant differentiable loss and an orthogonal permutation action give $\nabla L(gw)=g\nabla L(w)$, so a scalar-step gradient updater descends through these groupoids. General coordinate changes do not preserve the Euclidean update without further metric and integration data.
Richer mapping spaces use exact behavioral fibers $W_{A,f}$ and their homotopy quotients, with a discrete coproduct over $f$. In the deep-linear gauge example, $GL_2^+(\mathbb R)$ fixes the all-zero factorization in the zero-function fiber, so its classifying space is a retract of the exact semantic mapping space. Polar decomposition and the universal principal bundle give a nontrivial $\mathbb Z$ in its second homotopy group. The training updater is not assumed to descend through this richer quotient without additional equivariance.
A directed widening replaces $v\sigma(a\cdot x+\alpha)$ by two contributions with output weights $\lambda v$ and $(1-\lambda)v$. It preserves the function but increases parameter space and cost. It is not automatically an invertible architecture equivalence.
Finally, a learned optimizer network and a meta-policy update their own parameters and memory. A fixed runner enforces the accepted-step and admissibility contracts. The paper proves finite preservation and permutation descent for this construction, and the analytic bound on fixed-architecture runs satisfying the uniform hypotheses. It does not infer that an optimizer-only parameter change improves future optimizer quality.
7. Explicit limitations
The identity transition satisfies monad laws without progress. Strictly decreasing loss can have an unattained infimum. Loss convergence need not imply state convergence. Training-loss preservation need not imply population-risk improvement.
There is no always-terminating effective improver that finds a strict improvement whenever one exists for every total computable $q:\mathbb N\to\{0,1\}$ with $q(0)=1$. Given a machine $e$, set $q_e(n+1)=0$ when it halts within $n$ steps and $1$ otherwise. A uniformly successful terminating improver would decide halting. This obstruction survives categorical reformulation.
No Lean code, executable proof checker, finite benchmark, or machine-checked higher-category theorem is claimed. The full paper includes explicit obligations for a future substantial neural-network mechanization.
References and automation disclosure
The full paper contains twelve verified primary reference links, including:
1. J. Lurie, Higher Algebra, Section 4.7. https://www.math.ias.edu/~lurie/papers/HA.pdf 2. J. Lurie, Higher Topos Theory. https://www.math.ias.edu/~lurie/papers/HTT.pdf 3. E. Riehl and D. Verity, homotopy coherent adjunctions and monads. https://arxiv.org/abs/1310.8279 4. D. Gepner, R. Haugseng, and J. Kock, analytic monads. https://arxiv.org/abs/1712.06469 5. B. Fong, D. I. Spivak, and R. Tuyéras, compositional backpropagation. https://arxiv.org/abs/1711.10455 6. G. S. H. Cruttwell et al., categorical gradient-based learning. https://arxiv.org/abs/2103.01931 7. T. Chen, I. Goodfellow, and J. Shlens, function-preserving network transfer. https://arxiv.org/abs/1511.05641
Prepared with AI assistance at a human request. The submitting researcher remains responsible for final scholarly review and submission. This condensed body must accompany the full manuscript and source artifacts; it is not a substitute for them.