diff_const_on_ReachN
plain-language theorem explainer
The lemma shows that if two integer-valued potentials on a recognition structure both obey the discrete edge increment rule for the same δ, then their pointwise difference is invariant under any finite number of kinematics steps. Workers proving uniqueness results for potentials on causal graphs cite this when reducing global constancy to local edge conditions. The argument is a direct induction on the inductive definition of n-step reachability, applying the edge invariance lemma at each successor.
Claim. Let $p, q : M.U → ℤ$ satisfy the discrete edge condition DE(δ, p) and DE(δ, q) for fixed δ ∈ ℤ. Then for all n ∈ ℕ and x, y ∈ M.U such that y is reachable from x in n steps under the kinematics Kin(M), one has p(y) − q(y) = p(x) − q(x).
background
Pot denotes the type of functions from the universe of a recognition structure M to the integers. The predicate DE(δ, p) asserts that p increases by exactly δ along every edge of the recognition relation M.R. ReachN(K, n, x, y) is the inductive predicate expressing that y is obtained from x by n applications of the step relation in the kinematics K. The module assembles lightweight lemmas supporting uniqueness statements for such potentials on discrete reachability components. Upstream, ReachN is defined inductively with a zero-step base case and a successor rule that appends one kinematics step.
proof idea
Proof by induction on the ReachN hypothesis. The zero case holds by reflexivity. In the successor case, edge_diff_invariant supplies equality of the difference across the final step, which is then chained with the inductive hypothesis via transitivity.
why it matters
This result supplies the inductive step for constancy of potential differences on reach sets, directly feeding the component-wise version and the T4 uniqueness theorem on reachN. It forms part of the dependency-light T4 uniqueness lemmas in the Potential module, enabling reduction of uniqueness to basepoint agreement plus edge conditions. In the broader framework it supports discrete analogs of potential theory on causal structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.