unique_up_to_const_on_component
plain-language theorem explainer
If two ledgers L and L' both satisfy the affine condition with the same integer parameter δ, then their phi functions differ by an additive integer constant on any causally reachable component from a base point x0. Researchers establishing ledger uniqueness in Recognition Science cite this when showing that phi is fixed up to constants by the DE condition. The proof is a one-line wrapper that invokes the corresponding uniqueness theorem from the Potential module.
Claim. Let $L$ and $L'$ be ledgers on structure $M$ such that both satisfy the affine condition DE$ _δ$ applied to their respective recognition functions $φ_L$ and $φ_{L'}$. Then there exists an integer $c$ such that for every $y$ reachable from $x_0$ under the kinematics Kin$(M)$, $φ_L(y) = φ_{L'}(y) + c$.
background
IsAffine δ L holds precisely when the map x ↦ Recognition.phi L x satisfies the differential equation DE δ from the Potential module. Reaches K x y is the existential closure of ReachN, i.e., there exists a finite number of steps n such that ReachN K n x y. Kin M packages the recognition relation R of M as a Kinematics object on the universe M.U, with step function given by R. The lemma specializes the general affine uniqueness result T4 from Potential to the concrete case of recognition ledgers.
proof idea
The proof is a one-line wrapper that applies Potential.T4_unique_up_to_const_on_component to the functions p := fun x => Recognition.phi L x and q := fun x => Recognition.phi L' x, supplying the affine hypotheses hL and hL' together with the base point x0 and simplifying the resulting statement.
why it matters
This lemma supplies the ledger-specific instance of the affine uniqueness theorem T4 from Potential, thereby enabling component-wise constancy arguments inside the LedgerUniqueness module. It directly supports the broader program of showing that recognition ledgers are determined up to additive constants once the affine (DE) condition is imposed. No open scaffolding or unresolved questions are addressed by this proved result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.