edge_diff_invariant
If two integer-valued potentials p and q on a recognition structure both obey the same constant increment δ along every recognition edge, their difference is unchanged across any single edge. This invariance is cited in downstream reachability lemmas within the Potential module for building T4 uniqueness results. The proof reduces the claim by algebraic expansion of the difference of increments, substitution of the DE rules, and cancellation to zero.
claimLet $p, q : M.U → ℤ$. Suppose both satisfy the discrete edge rule with fixed integer δ, that is, $p(b) - p(a) = δ$ and $q(b) - q(a) = δ$ whenever $M.R(a, b)$. Then $p(b) - q(b) = p(a) - q(a)$ for any such edge.
background
Pot is the abbreviation for functions from the universe U of a RecognitionStructure M to the integers ℤ. DE δ p is the proposition that p increases by exactly δ along every pair related by the recognition relation R of M. The module supplies dependency-light T4 uniqueness lemmas on discrete reach sets, with this lemma supplying the single-edge case of difference invariance.
proof idea
The tactic proof expands the target difference of differences via ring, replaces each increment by δ using the two DE hypotheses, simplifies δ - δ to zero, and applies sub_eq_zero to finish.
why it matters in Recognition Science
The result feeds diff_const_on_ReachN, which lifts the invariance to n-step reachability and supports the T4 uniqueness statements on components and balls. It supplies the edge-level fact needed for the discrete potential theory that underpins the Recognition framework's treatment of constant-increment functions on reach sets.
scope and limits
- Does not apply when p and q obey different δ values.
- Does not address pairs outside the recognition relation R.
- Does not assume or produce any metric or continuity on U.
- Does not extend the statement to real-valued or non-integer increments.
formal statement (Lean)
21lemma edge_diff_invariant {δ : ℤ} {p q : Pot M}
22 (hp : DE (M:=M) δ p) (hq : DE (M:=M) δ q) {a b : M.U} (h : M.R a b) :
proof body
Tactic-mode proof.
23 (p b - q b) = (p a - q a) := by
24 have harr : (p b - q b) - (p a - q a) = (p b - p a) - (q b - q a) := by ring
25 have hδ : (p b - p a) - (q b - q a) = δ - δ := by simp [hp h, hq h]
26 have : (p b - q b) - (p a - q a) = 0 := by simp [harr, hδ]
27 exact sub_eq_zero.mp this
28
29/-- The difference (p − q) is constant along any n‑step reach. -/