diff_in_deltaSub
plain-language theorem explainer
If a discrete potential satisfies the edge increment condition with fixed step δ, then differences along any finite reachability path belong to the subgroup generated by δ. Researchers proving T4-style uniqueness on connected components in Recognition Science cite this to control potential variation on reach sets. The proof is a direct one-line wrapper around the n-step increment lemma that refines the exact multiple n·δ into an existential statement.
Claim. Let $p$ be a function from the universe of a recognition structure $M$ to the integers that satisfies the discrete edge rule: $p(b)-p(a)=δ$ whenever $M$ recognizes an edge from $a$ to $b$. Then for any $n$-step reachability relation from $x$ to $y$ in the kinematics induced by $M$, there exists an integer $k$ such that $p(y)-p(x)=kδ$.
background
Pot M abbreviates the type of discrete potentials $M.U→ℤ$. DE δ p is the predicate asserting that every recognition edge increases the potential by exactly δ. ReachN K n x y is the inductive n-step reachability relation generated by the step relation of a kinematics K; its constructors are the zero-step identity and the successor that appends one step. The upstream lemma increment_on_ReachN states that under DE, the exact difference along any ReachN path of length n is n·δ (T8 quantization). The module supplies dependency-light uniqueness results on discrete reach sets.
proof idea
One-line wrapper that applies increment_on_ReachN to obtain the concrete equality p y - p x = n·δ and then refines the existential quantifier to witness k = n.
why it matters
The lemma closes the gap between the exact n-step increment and the subgroup statement needed for T4 uniqueness on reach sets and components. It directly supports the parent results T4_unique_on_reachN and T4_unique_on_component by guaranteeing that all potential differences lie in δℤ. In the broader framework it instantiates the quantization step of the forcing chain (T8) on finite discrete paths.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.