Six Birds Foundations VI: A Catalog of Dynamical Structural Laws

The Six Birds corpus through Foundations IV certifies states: each of its laws fixes a single map, quotient, package, or declared finite family and proves a static classification about it. Nothing in the corpus certifies runs: liveness, amortized or transfinite cost over unbounded time, covers that must move with their targets, obstructions that grow, react, or are manufactured by the system's own history, route defects that integrate into potentials, transport that emerges from substrate dynamics, or content that persists through repeated loss. This paper is the catalog of exactly those laws: thirteen dynamical structural laws (G1–G13) in four clusters, each stated in the six-part normal form inherited from Foundations IV and each carrying an unbounded quantifier — temporal in most laws, scale-indexed in G11, orbit-radiating in G12, asymptotic in G13 — that no static row possesses. The laws were mined from eccentric mathematical problems — Collatz, Goodstein, Egyptian fractions, reverse-and-add, Recamán, the angel problem, sandpiles, rule 184, Ducci, aperiodic tilings, Hadwiger–Nelson, Apollonian packings — treated as theorem detectors: each problem's folklore almost-proof names a promoted object, the object's lawful descended certificate fixes a boundary expression, and the residual surviving comparison against every existing law is the law seed. The contributions are separated by provenance, and every result carries its provenance line in the text. What is recovered standard is the classical mathematics anchoring the laws that have such a component (the potential method, well-founded ranking, Goodstein's theorem with the Kirby–Paris price, the angel-problem threshold, Dhar's abelian property and the Fey–Levine–Peres least-action principle, Robinson's hierarchical forcing, de Bruijn–Erdős compactness, the Apollonian density and reciprocity theorems), cited at each result and never restated as this paper's; what is recovered SBT is the corpus apparatus and each law's nearest Foundations IV cousin, cited by identifier and differently scoped in every case. What is sharpened is the layer-agnostic normal form of each law: named hypotheses, typed records, minimized falsifiers, and two scope repairs (legal-versus-legal least action; explicit devil legality). Nothing is labelled new: the two candidate schemas (G1's ghost discharge, G6's covering and hole-forming) are sharpened typed records with elementary proofs, and the mining protocol is offered as a procedure without a result label. The abstract core of every law is mechanized in Mathlib-free Lean 4 with per-declaration kernel-axiom receipts, and the appendix records clause by clause which parts of each printed statement the Lean covers; six laws are full theorem-grade rows, one splits into an unconditional theorem and a schema, three are schema-grade with named boxed hypotheses, and three are calibration-anchored schemas discharged end-to-end by solved classical instances. The paper solves no open problem and claims none: Collatz, Erdős–Straus, Lychrel, Recamán, the Langton's-ant highway, Gilbreath, and the exact chromatic number of the plane all remain open, and each law's nonclaims say so explicitly.