logicalDepth
plain-language theorem explainer
The logicalDepth function returns the ceiling of log base 2 of n plus one, quantifying logical propagation depth as the number of implication layers across a system of size n. Analysts of cellular-automaton embeddings in SAT solvers cite it when bounding simulation cost under locality. The definition is a direct one-line computation that applies the standard ceiling and base-2 logarithm operations.
Claim. The logical propagation depth for parameter $n$ is defined by $d(n) = 2^{n+1}$ ceiling of the base-2 logarithm of $n+1$.
background
The module supplies abstract runtime parameters for cellular-automaton embeddings of SAT instances. Logical propagation depth counts the successive implication layers required for a signal to cross distance n. The upstream CirclePhaseLift.and result supplies an explicit log-derivative bound M that converts to an angular Lipschitz constant on the circle, providing the analytic control needed for phase-lift arguments that later feed runtime estimates.
proof idea
One-line definition that applies Nat.ceil to Real.logb 2 (n + 1).
why it matters
The definition supplies the O(log n) logical-depth factor inside caTimeBound, which asserts an O(n^{1/3} log n) target for CA time under locality. It therefore closes the logical-depth slot in the CA-to-TM simulation cost analysis and connects the Recognition Science complexity module to the eight-tick octave and phi-ladder scaling already fixed in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.