edge_diff_invariant
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.