T4_unique_up_to_const_on_component
plain-language theorem explainer
Two discrete potentials p and q that each increase by exactly δ along every edge of the recognition relation differ by a constant on the reachable component from any basepoint x0. Ledger uniqueness arguments cite this to show affine structures are fixed up to additive constants on connected components. The proof extracts the constant from the basepoint values and invokes the component constancy lemma followed by algebraic rearrangement.
Claim. Let $p, q : U_M → ℤ$ satisfy the discrete edge rule that $p(b) - p(a) = δ$ (and likewise for $q$) whenever $a$ is related to $b$ by the recognition relation $R$. Then there exists an integer $c$ such that $p(y) = q(y) + c$ for every $y$ reachable from $x_0$ under the kinematics induced by $R$.
background
Pot M is the type of functions from the universe U to integers. DE δ p is the predicate asserting that p increases by exactly δ along every edge of the recognition relation R. Reaches K x y holds precisely when there exists a finite n such that ReachN K n x y, i.e., y lies in the forward orbit of x under the kinematics K derived from R. The module collects dependency-light uniqueness lemmas for such potentials restricted to discrete reach sets. Upstream results include the definition of Reaches in both Causality.Basic and Causality.Reach, the step operation from CellularAutomata, the RS-native unit gauge U, and the arithmetic identities add_assoc and add_comm extracted from the logic-to-arithmetic foundation.
proof idea
The tactic proof refines the witness to the integer c := p x0 - q x0. It then applies the sibling lemma diff_const_on_component to obtain p y - q y = c for any y reachable from x0. Finally it rearranges the equality via simpa using add_comm, add_left_comm, add_assoc and sub_eq_add_neg.
why it matters
This result is invoked directly by LedgerUniqueness.unique_up_to_const_on_component to transfer uniqueness from potentials to the phi maps of affine ledgers. It belongs to the T4 family of componentwise uniqueness statements that support quantization and ledger rigidity in the Recognition framework. The lemma closes a step in the forcing chain by showing that any two solutions of the discrete edge rule are rigidly offset on each reach component, without requiring extra hypotheses on the structure M.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.