Dynamic Street Complexes: Certified Kinodynamic Planning on Deforming Ribbons

We introduce the \emph{dynamic street complex} (DSC), a five-layer space--time road representation the record at time t, denoted Rₜ = (T, Gₜ, Fₜ, Lₜ, Uₜ) coupling directed topology, deforming ribbon geometry, traffic fields, rules, and uncertainty. Lanes are ribbons, users are probability or reachable-set tubes, and typed events rewrite the represented road. The traffic field enters the local causal cone, so congestion changes feasibility rather than cost alone. We separate exact semantics from computable certification. An exact finite cover factorizes safe trajectories into overlap points and local reachability witnesses. Three conservative generators then share one certificate language: star-cell arcs, sound at every resolution and locally consistent under an explicit constant condition evaluated here; chord arcs, needing only positive speed slack on flat static charts; and cubic-Hermite arcs on a velocity-augmented lattice, giving kinodynamic resolution completeness for jerk-regular robust references with pointwise speed and acceleration bounds and velocity-compatible portal transitions. The last result does not impose a global jerk limit across spline knots. We also prove monotone comparison and a critical-density severance result for the field-modulated feasible set. Evidence is of three kinds and no more. Six deterministic synthetic studies check the certificates, refinement behavior, resolution-gated apex cutting, prescribed-density severance, and a coupled experiment in which a conservative Godunov solution of the width-corrected kinematic-wave law feeds the causal cone. A same-search ablation additionally isolates scheduled width rewrites and conservative phantom tubes: deleting either layer admits plans that fail under the fully revealed scripted incident, while a no-incident control is unchanged. A controlled lane-centre comparison on eight bundled public CommonRoad scenarios gives DSC-A*, SIPP, and an unpruned time lattice one graph and one collision oracle; all three solve all cases at identical earliest arrivals with zero same-oracle replay violations, while a fixed corridor solves seven. This is a representation/search comparison, not a production-controller benchmark.A self-contained Lean~4 companion kernel-checks exact-rational star, chord, and typed Hermite certificates with the pinned Lean~4.19.0 toolchain. The scope of each claim is tabulated explicitly: geometry-to-rational transcription, continuous containment, PDE entropy theory, perception, tracking, forecast calibration, and closed-loop control remain outside the formal guarantee.