edge_diff_invariant
plain-language theorem explainer
If two integer-valued potentials on a recognition structure both obey the same discrete increment rule δ along the relation R, their difference is unchanged across any single edge. Workers on T4 uniqueness for discrete reach sets cite this base invariance when lifting edge properties to path constancy. The tactic proof rearranges the target difference via ring, substitutes the two DE hypotheses to obtain δ - δ, and concludes via sub_eq_zero.
Claim. Let $M$ be a recognition structure. Let $δ ∈ ℤ$. Let $p, q : M.U → ℤ$ each satisfy $p(b) - p(a) = δ$ (respectively for $q$) whenever $M.R a b$. Then for any $a, b$ with $M.R a b$, $p(b) - q(b) = p(a) - q(a)$.
background
Pot is the type of potentials, i.e., maps from the universe $M.U$ to ℤ. DE(δ, p) is the proposition that p increases by exactly δ along every pair related by the recognition relation R. The module collects dependency-light T4 uniqueness lemmas on discrete reach sets, establishing invariance and uniqueness properties of such potentials preparatory to pathwise results.
proof idea
Tactic proof. Ring rewrites the target as (p b - p a) - (q b - q a). Simp with the two DE hypotheses replaces both increments by δ, yielding δ - δ. A second simp reduces the expression to zero. Sub_eq_zero then gives the equality.
why it matters
The edge invariance supplies the base case for the induction in the downstream lemma diff_const_on_ReachN, which lifts the property to n-step reaches. It belongs to the family of T4 uniqueness results on connected components and supports the discrete kinematics used in the Recognition framework's forcing chain (T0-T8) and phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.