unique_on_reachN
plain-language theorem explainer
If two affine ledgers agree on the value of phi at a base point, their phi functions coincide at every point reachable in finitely many kinematics steps. Researchers establishing uniqueness of solutions to the recognition differential equation on discrete spaces would cite this result. The proof is a direct one-line wrapper that instantiates the general uniqueness theorem T4_unique_on_reachN on the phi maps of the two ledgers.
Claim. Let $L$ and $L'$ be ledgers on $M$ such that both satisfy the affine condition for the same integer parameter, meaning their maps $xmapsto phi_L(x)$ and $xmapsto phi_{L'}(x)$ obey the same equation DE$ _delta$. If $phi_L(x_0)=phi_{L'}(x_0)$ at a base point $x_0$, then $phi_L(y)=phi_{L'}(y)$ whenever $y$ is reachable from $x_0$ in $n$ steps under the kinematics Kin$(M)$.
background
The module LedgerUniqueness develops uniqueness statements for phi functions attached to ledgers. Its central definition IsAffine asserts that the map $x mapsto phi L x$ satisfies the differential equation DE from the Potential module with fixed integer parameter delta. ReachN is the inductive reachability predicate: it holds at zero steps when the points coincide and closes under a single kinematics step via K.step, where K is instantiated as Potential.Kin M.
proof idea
The proof introduces the reachability hypothesis and then applies the upstream lemma Potential.T4_unique_on_reachN to the concrete functions p = phi L and q = phi L', supplying the two IsAffine hypotheses together with the base-point equality. A final simpa closes the resulting equality.
why it matters
This lemma supplies component-wise uniqueness for affine ledgers, a prerequisite for showing that ledger states are determined by their values on a generating set. It directly instantiates the general T4 uniqueness result from Potential and supports the ledger-equivalence claims needed higher in the Recognition framework, including the forcing chain steps that fix J-uniqueness and the eight-tick octave. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.