increment_on_ReachN
plain-language theorem explainer
The lemma shows that any integer-valued potential p obeying the discrete edge rule with fixed increment δ changes by exactly nδ along an n-step reach in the kinematics. Researchers deriving quantized potentials or T4 uniqueness results on discrete graphs cite this when establishing subgroup structure for differences. The proof is by induction on the ReachN relation: the zero case is immediate, while each successor applies the edge rule once and combines via ring arithmetic.
Claim. Let $p : M.U → ℤ$ satisfy the discrete edge rule that $p(b) - p(a) = δ$ for every recognition edge $M.R(a,b)$. Then for any $n$-step reach from $x$ to $y$ under the kinematics of $M$, the potential difference satisfies $p(y) - p(x) = n δ$.
background
The Potential module contains dependency-light T4 uniqueness lemmas on discrete reach sets. Pot is the abbreviation for integer-valued functions on the universe of a recognition structure M. DE δ p is the predicate asserting that p increases by exactly δ along every edge of the recognition relation M.R. ReachN is the inductive definition of n-step reachability in a kinematics: the zero constructor connects a point to itself, and the successor constructor extends a reach by one step.
proof idea
The proof proceeds by induction on the ReachN hypothesis. The zero case simplifies directly to equality. In the successor case the DE hypothesis supplies the increment over the final edge, the inductive hypothesis supplies the difference over the preceding n steps, and ring tactics combine them to obtain the (n+1)δ result, with Nat.cast handling the successor conversion.
why it matters
This T8 quantization lemma supports discrete potential changes along paths and feeds directly into the corollary diff_in_deltaSub, which places all reach differences inside the subgroup generated by δ. It underpins the family of T4 uniqueness results on reach sets and components, consistent with the eight-tick octave and dimension forcing in the T0-T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.