Appendix A: Lean Formalization Structure

The main theorems developed in Chapters 2—7–including the global attractor theorem, the frozen invariant-law proposition, the finite-time tracking theorem, and the upper-semicontinuity corollary–have been formalized in the Lean 4 proof assistant with no axioms, placeholders, or proof stubs. Because the verified results are stated for a general finite state space, both the two-state system of Chapter 0 and the three-state routing model of Chapter 2 are instances of it; no model-specific Lean development is needed for either example.

This appendix describes the structure of the formalization for readers who wish to inspect the machine-checked proofs. The proof scripts are publicly available at https://codeberg.org/VladP/Notes-on-Dynamical-Systems-for-Actor-Critic-Learning, under formalization/DynsysFormalization/.

To verify the formalization from scratch:

The script uses the pinned Lean/Lake configuration, fetches the mathlib cache, builds DynsysFormalization, and checks that the sources contain no sorry, admit, or axiom stubs. The final keyword check matters because Lean accepts sorry with only a warning and accepts axiom declarations without any message.

The main results of Chapters 2—7 map to Lean statements as follows. Labels and statement numbers in parentheses are those of the short note (V. Prytula, “Global attractors and fast-slow reduction for finite-state actor-critic mean dynamics”), the paper version of these results; the LaTeX source is included in the repository under submission/.

• Generator assumptions (Chapter 2, label ass:gen): ShortNoteGeneratorAssumptions in FrozenInvariantLaw/Core.lean.
• Mixing assumption (Chapter 6, label ass:mix): UniformExponentialMixing in FrozenInvariantLaw/Core.lean.
• Pathwise contraction (Chapter 7, label ass:path): PathwiseFastStateContraction in ShortNoteReduction/Tracking.lean.
• Local Lipschitz regularity (Chapter 3, no label): shortNoteClampedPhaseVelocity_locallyLipschitz in ShortNoteSystem.lean.
• Actor-box invariance (Chapter 4, no label): actorBox_forwardInvariant in Level1/ActorBox.lean.
• Simplex invariance (Chapter 4, no label): simplex_forwardInvariant_forward in Level1/Simplex.lean.
• Critic coercivity (Chapter 4, no label): criticBall_forwardInvariant in Level1/Critic.lean.
• Absorbing set (Chapter 4, no label): absorbingSet_compact in ShortNoteTheorems.lean.
• Global attractor (Theorem 2, Chapter 5, label thm:attractor): shortNotePhaseSpace_globalAttractor_of_exact_explicit in ShortNoteTheorems.lean.
• Frozen invariant law (Proposition 5, Chapter 6, label prop:invlaw): frozenInvariantLaw_existsUniqueLipschitz_of_uniformExponentialMixing in FrozenInvariantLaw/Existence.lean.
• Tracking estimate (Theorem 8, Chapter 7, label thm:tracking): shortNote_phaseState_tracking_of_simplexBound_and_gronwallProjection in ShortNoteReduction/Tracking.lean.
• Upper semicontinuity (Corollary 9, Chapter 7, label cor:usc): shortNotePhaseStateUpperSemicontinuity_of_minorization_explicit and shortNotePhaseStateUpperSemicontinuity_of_pathwiseFamily_explicit in ShortNoteReduction.lean.
• Minorization criterion (Proposition 10, Chapter 7, label prop:minorization): pathwiseExactLawEvolutionFamilyOnZeroMass_shortNote_minorization_implies_pathwise in ShortNoteReduction/Minorization.lean.

The file structure mirrors the mathematical structure of the lecture notes. The prescribed-closure results (Chapters 3—5) live in Level1/, ShortNoteSystem.lean, and ShortNoteTheorems.lean as reusable confinement, absorption, and omega-limit machinery. The paper-facing Lean theorem named shortNotePhaseSpace_globalAttractor_of_exact_explicit applies that machinery to the exact generator-law phase space. In the book’s taxonomy, that exact generator-law attractor statement is the exact-system theorem recorded in Chapter 7, Section 7.1; it is not merely the prescribed-closure theorem of Chapter 5 with notation changed. The bridge theorem (Chapter 6) lives in FrozenInvariantLaw/. The fast-slow reduction (Chapter 7) is split across the four files under ShortNoteReduction/: ReducedState.lean for the reduced flow and metric bridges, PathwiseCore.lean for non-autonomous law evolution, Tracking.lean for the finite-time comparison estimates, and Minorization.lean for the reference-state criterion. The export file ShortNoteReduction.lean collects the Lean statements corresponding to the tracking estimate and the upper-semicontinuity corollary (the paper’s Theorem 8 and Corollary 9).

Three design choices in the formalization are worth noting because they reflect genuine mathematical content rather than Lean implementation detail.

Phase space as subtype. The global attractor theorem is stated on PhaseSpaceState data, a subtype of the product space that enforces the actor box, critic ball, and simplex constraints. This matches the paper’s phase space .

Pathwise contraction split. The paper’s pathwise contraction assumption (ass:path, its Assumption 7) is a single clean hypothesis. In Lean it is represented by PathwiseFastStateContraction, which bundles three pieces: a measurable evolution family, a continuous-path evolution core, and an agreement statement between the two. The split is mathematically meaningful: the variation-of-constants formula in the tracking proof needs measurability, while the comparison estimates use continuity of the law trajectories.

N=1 branch in the minorization criterion. The Lean proof of the minorization criterion (the paper’s Proposition 10) exposed that the displayed minorization constants become degenerate when the state space has only one state (, so the zero-mass subspace ). The theorem therefore splits: trivial contraction on when , explicit minorization constants when . This split makes the mathematical statement more precise, not more cumbersome.

The global attractor theorem (the paper’s Theorem 2, thm:attractor) is unconditional: it is stated on the subtype phase space PhaseSpaceState data, where the semiflow is constructed outright from the generator assumptions, so its only hypotheses are the model data and ass:gen. The theorem is also exported at the paper’s literal absorbing set, with , through shortNotePhaseSpace_globalAttractor_of_exact_sharp_explicit; the attractor is proved nonempty, and the canonical semiflow is proved jointly continuous in time and state.

The tracking estimate (Theorem 8, thm:tracking) and the upper-semicontinuity corollary (Corollary 9, cor:usc) are now exported on the same subtype phase space, where the semiflow input is the one Theorem 2 constructs. The fixed-delta tracking theorem shortNote_phaseState_tracking_of_simplexBound_and_gronwallProjection takes the paper’s pathwise contraction assumption (ass:path) directly, and its Gronwall constant does not degenerate as the time-scale parameter shrinks (the earlier proof via shortNote_phaseState_tracking_of_simplexBound_and_reducedAbsorbingDiameter is retained for comparison).

The family-level delta -> 0 layer carries the paper’s “one constant, independent of delta” clause as the named theorem shortNotePhaseStateTrackingFamilyDisplayedEstimates, and Corollary 9 is discharged end to end in two ways: from the minorization criterion (Proposition 10) via shortNotePhaseStateUpperSemicontinuity_of_minorization_explicit, and from the literal family form of ass:path via shortNotePhaseStateUpperSemicontinuity_of_pathwiseFamily_explicit, with the minorization criterion proved as one way to obtain that family data. The mixing assumption (ass:mix) is likewise producible from its paper-literal matrix-exponential decay form through uniformExponentialMixing_of_matrixExponential.

Older exports on the ambient product space remain in the repository and remain conditional on ambient semiflow existence. That hypothesis cannot be obtained by simply transporting Theorem 2’s subtype semiflow: the ambient raw field keeps the actor velocity outside the parameter box, where it grows superlinearly and can escape in finite time. The Lean ambient statements are sharper than that raw-field reading, however. Their equation witnesses require the raw equations only from starts already in the phase space, so five bridge theorems ending in _of_canonical_extension reduce the whole conditional ambient group–ambient Theorem 1, ambient tracking, ambient upper semicontinuity, and the legacy reduced ambient target–to one hypothesis: a total continuous semiflow on the ambient product space that agrees with the canonical subtype semiflow on for nonnegative times.

That extension is not needed for the main statements used in the paper or in Chapters 2—7, which is why the current verified results live on the subtype . For a later book formalization, the natural next step is to construct a fully clamped ambient vector field, prove that it agrees with the exact field on , and rerun the ODE existence, uniqueness, gluing, and continuity pipeline for that field. This would provide the ambient extension by construction, but it would also add a substantial theory of off-phase-space dynamics that the main theorems do not use. The “no axioms, no stubs” guarantee applies to the ambient statements’ proofs given their stated extension hypothesis.

For the main theorem statements (statement numbers as in the paper):

1. ShortNoteTheorems.lean–Theorem 2 (global attractor)
2. FrozenInvariantLaw/Existence.lean–Proposition 5 (frozen invariant law)
3. ShortNoteReduction.lean–Theorem 8 (tracking), Corollary 9 (USC)

For supporting proof files:

4. ShortNoteSystem.lean–ODE well-posedness, semiflow construction
5. FrozenInvariantLaw/Core.lean then Resolvent.lean–frozen law construction
6. ShortNoteReduction/Minorization.lean–Proposition 10 (minorization criterion)
7. ShortNoteReduction/Tracking.lean–tracking estimates
8. ShortNoteReduction/ReducedState.lean–reduced attractor, metric bridges
9. ShortNoteReduction/PathwiseCore.lean–transport construction

Reading the formalization in the main-statements-first order reproduces the mathematical structure of the notes.