dependency_cone
plain-language theorem explainer
The theorem establishes that in a one-dimensional cellular automaton the state at tape position i after t steps depends only on the initial interval from i-t to i+t, with the cone containing at most 2t+1 cells. Researchers bounding locality in CA-based SAT solvers or light-cone arguments would cite the result. The proof constructs the explicit closed interval Finset and verifies the cardinality and distance bounds by direct rewriting and linear arithmetic.
Claim. For any tape (a function from integers to cell states), integer position $i$, and natural number $t$, there exists a finite set of integers cone such that the cardinality of cone is at most $2t+1$ and every position $i'$ in cone satisfies $|i'-i|leq t$.
background
The module supplies cellular automata gadgets that encode SAT instances via local deterministic rules, modeled on Rule 110 universal computation and adapted for Boolean circuit evaluation. A Tape is the type of infinite sequences of cell states, with all analysis restricted to finite windows. The local theoretical setting requires each gadget to be local, deterministic, and reversible to maintain ledger compatibility under the Recognition framework.
proof idea
The tactic proof constructs the cone as the image of Finset.Icc (i-t) (i+t) under the identity. The cardinality goal rewrites via Int.card_Icc and simplifies by ring to 2t+1. The distance goal unfolds image and interval membership, applies abs_sub_le_iff, and closes both directions with linarith.
why it matters
The result supplies the explicit light-cone bound needed to establish locality of CA steps in the SAT gadget construction. It supports the module claim that CA evaluation runs in O(n^{1/3} log n) time while preserving reversibility. In the broader Recognition Science setting it aligns with finite propagation speed on the one-dimensional tape, consistent with the eight-tick octave and D=3 spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.