diff_const_on_component
plain-language theorem explainer
The lemma establishes that for two integer-valued potentials satisfying the same discrete edge increment rule δ, their pointwise difference is invariant under reachability in the induced kinematics. Researchers proving componentwise uniqueness for potentials on discrete reach sets would cite this result. The proof reduces the existential reachability witness to an n-step path via case analysis and applies the sibling ReachN constancy lemma.
Claim. Let $p, q : U_M → ℤ$ satisfy the discrete edge condition $DE(δ)$ for the same integer $δ$, so that $p(b) - p(a) = δ$ whenever $M.R(a,b)$. If $y$ is reachable from $x_0$ in the kinematics $Kin(M)$, then $p(y) - q(y) = p(x_0) - q(x_0)$.
background
Pot is the type of integer-valued functions on the universe $U$ of a recognition structure $M$. The predicate $DE(δ, p)$ asserts that along every edge of the recognition relation $R$, the potential increases by exactly $δ$. Reaches$(Kin M, x_0, y)$ is the existential closure of the $n$-step reachability relation ReachN under the kinematics $Kin M$, which packages the recognition relation as a transition system on $U$ (see Causality.Basic and Causality.Reach).
proof idea
The proof performs rcases on the Reaches hypothesis to extract the step count $n$ and the ReachN witness $h$, then directly invokes the sibling lemma diff_const_on_ReachN with those parameters.
why it matters
This lemma is invoked inside T4_unique_up_to_const_on_component to obtain the basepoint offset $c = p(x_0) - q(x_0)$ and thereby establish that two $δ$-potentials differ by a constant on each reach component. It belongs to the dependency-light T4 uniqueness collection in the Potential module, which supports discrete potential theory consistent with the recognition relation and the causality kinematics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.