T4_unique_on_component
plain-language theorem explainer
Two integer-valued potentials satisfying the same constant-increment rule along recognition edges agree at every point reachable from a common base point. Discrete-potential work in Recognition Science cites this for componentwise uniqueness on the recognition graph. The proof unpacks the existential in the reachability hypothesis and invokes the n-step uniqueness lemma.
Claim. Let $p,q:U(M)→ℤ$ satisfy $p(b)-p(a)=δ$ whenever $R(a,b)$ holds. If $p(x_0)=q(x_0)$ and $y$ is reachable from $x_0$ under the kinematics whose step relation is $R$, then $p(y)=q(y)$.
background
The Potential module supplies dependency-light uniqueness lemmas for discrete potentials on recognition structures. Pot is the type of integer-valued functions on the universe U. DE requires that the difference along every recognition edge equals the fixed integer δ. Kin packages the recognition relation R as the step relation of a Causality.Kinematics object. Reaches asserts the existence of a finite chain of steps connecting two points.
proof idea
The proof performs case analysis on the Reaches hypothesis to extract the step count n together with a ReachN witness, then applies the sibling lemma T4_unique_on_reachN.
why it matters
The result extends n-step uniqueness to the full transitive closure, showing that δ-potentials are determined on each connected component of the recognition graph. It belongs to the T4 uniqueness package that supports later invariants and difference lemmas in the Potential module. No downstream citations are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.