Prediction Depth of Controlled Cellular Automata

This preprint classifies prediction depth for one-sided cellular automata whose frozen Boolean controls gate stay and hop updates over the binary field. Lean 4 verifies the classification, logspace-uniform circuit constructions, and depth lower bounds, including exact De Morgan depth for the homogeneous Pascal rule. The paper also gives exact depth formulas for transported controls and matching logarithmic depth bounds for a branching rule with additive control evolution. The English PDF is the primary edition. The Simplified Chinese, Japanese, and Esperanto PDFs are translations of the same revision. The accompanying reproducibility ZIP contains the Lean formalization, Typst sources, bibliography, pinned toolchain and dependency manifest, and build and audit scripts. Source snapshot: https://github.com/miuchan/structural-certificates-for-prediction-depth/tree/1f2c9ccb3e7fde4431b491227bbeed265eaf56bc