T4_unique_on_inBall
plain-language theorem explainer
Two potentials obeying the discrete edge rule with fixed increment δ agree at every point inside the n-ball around a basepoint where they match. Ledger uniqueness arguments cite this lemma to obtain local agreement on discrete reach sets. The proof is a one-line wrapper that extracts a reachability witness from the inBall hypothesis and delegates to the reachN uniqueness result.
Claim. Let $p, q : U(M) → ℤ$ satisfy $DE(δ, p)$ and $DE(δ, q)$. If $p(x_0) = q(x_0)$ and $y$ lies in the $n$-ball around $x_0$ under the kinematics induced by the recognition relation, then $p(y) = q(y)$.
background
Pot is the type of integer-valued functions on the universe of a RecognitionStructure. DE(δ, p) is the predicate requiring that p increases by exactly δ along every recognition edge. The inBall predicate, imported from Causality.Basic and Reach, asserts existence of k ≤ n such that y is reachable from x0 via ReachN. The module supplies dependency-light T4 uniqueness lemmas on discrete reach sets.
proof idea
The proof is a one-line wrapper. It cases on the inBall hypothesis to obtain a witness k ≤ n together with a ReachN fact, then applies T4_unique_on_reachN with those data.
why it matters
This result is invoked by unique_on_inBall in LedgerUniqueness, which transfers the agreement to affine ledgers. It fills the local uniqueness step on n-balls inside the T4 chain for potentials on discrete reach sets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.