unique_on_inBall
plain-language theorem explainer
If two affine ledgers agree on the recognition function at a base point x0, their phi values coincide at every point inside a finite causal ball under the induced kinematics. Researchers deriving uniqueness for solutions of the recognition difference equation would cite this when propagating local agreement along causal paths. The proof is a direct one-line application of the general T4 uniqueness theorem by substituting the two phi maps.
Claim. Let $M$ be a recognition structure, let $δ ∈ ℤ$, and let $L, L'$ be ledgers on $M$ such that both satisfy the affine difference equation DE$_δ$ with respect to their recognition functions $ϕ_L$ and $ϕ_{L'}$. If $ϕ_L(x_0) = ϕ_{L'}(x_0)$ and $y$ lies in the causal ball of radius $n$ around $x_0$ under the kinematics Kin$(M)$, then $ϕ_L(y) = ϕ_{L'}(y)$.
background
The LedgerUniqueness module derives uniqueness for the recognition function phi on ledgers obeying the affine condition. IsAffine δ L holds precisely when the map x ↦ phi L x satisfies the difference equation DE δ supplied by the Potential module. The kinematics Kin M packages the recognition relation R of M as the step relation of a causal structure, so that inBall asserts existence of k ≤ n with ReachN holding between x0 and y. The RS-native units U fix the gauge with c = 1, τ₀ = 1 tick and ℓ₀ = 1 voxel.
proof idea
The proof is a one-line wrapper that applies Potential.T4_unique_on_inBall, instantiating p and q with the maps x ↦ phi L x and x ↦ phi L' x, supplying the two IsAffine hypotheses, the base-point agreement (via simpa), and the inBall hypothesis hin.
why it matters
The lemma shows that agreement of phi propagates along finite causal balls whenever both ledgers are affine, supplying a local uniqueness step that supports global ledger uniqueness arguments. It fills the T4 slot in the uniqueness chain for functions obeying the same δ-rule and aligns with the Recognition Composition Law by preserving the invariant difference (p − q) on each edge. No downstream uses appear yet; it leaves open the extension to infinite reachability or non-affine cases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.