T4_unique_on_reachN
plain-language theorem explainer
Two δ-potentials that agree at a basepoint x0 must agree at every point reachable from x0 in any finite number of steps under the kinematics. Ledger uniqueness arguments and componentwise potential comparisons cite this result. The proof invokes the companion lemma establishing constancy of the difference on the reach set, then cancels the base equality to obtain zero difference at the target.
Claim. Let $M$ be a recognition structure. Let Pot$(M)$ be the type of maps $M.U → ℤ$. Let DE$(δ, p)$ assert that $p(b) - p(a) = δ$ whenever $a$ is related to $b$ by the recognition relation of $M$. If $p$ and $q$ both satisfy DE$(δ, ·)$ and $p(x_0) = q(x_0)$, then $p(y) = q(y)$ for every $y$ such that ReachN$(Kin(M), n, x_0, y)$ holds.
background
The Potential module supplies dependency-light T4 uniqueness lemmas on discrete reach sets. Pot$(M)$ is the type of integer-valued maps on the universe $M.U$. DE$(δ, p)$ is the predicate that $p$ increases by exactly the fixed integer δ along every edge of the recognition relation $M.R$ (see the sibling definition DE). Kin packages that same relation as the step relation of a kinematics object for causality arguments. ReachN is the standard inductive definition of n-step reachability: the zero case is reflexivity and the successor case appends one kinematics step.
proof idea
The proof is a short tactic script. It introduces the reachability hypothesis, applies the sibling lemma diff_const_on_ReachN to obtain constancy of the difference $p - q$ on the reachable set, rewrites the base equality to show the constant is zero, and extracts the target equality by subtraction.
why it matters
This supplies the core uniqueness step for T4 in the Potential module. It is invoked directly by T4_unique_on_component (to handle arbitrary reachability) and by T4_unique_on_inBall (for membership in the n-ball). The ledger lemma unique_on_reachN in LedgerUniqueness reuses the identical pattern for affine ledgers. Within the Recognition framework it closes the discrete potential uniqueness required before statements about ledger phi or componentwise agreement can be lifted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.