IsAffine
plain-language theorem explainer
Defines when a ledger is affine with increment δ by requiring its induced potential to obey the discrete edge increment rule. Uniqueness results for potentials on reachable sets cite this definition to propagate equality from a base point. It is realized as a direct invocation of the DE predicate on the ledger-derived potential.
Claim. Let $L$ be a ledger on the recognition structure $M$. Then $L$ is affine with increment $δ$ if the potential $ϕ$ extracted from $L$ satisfies $ϕ(b)-ϕ(a)=δ$ whenever $a$ is related to $b$ by the recognition relation.
background
The discrete edge rule requires that a potential function increases by a fixed integer δ along every edge of the underlying relation R. Here the potential is obtained from the ledger L by the phi construction in the Recognition module. The definition therefore specializes the general DE condition to ledger-induced potentials. Upstream, DE is defined as the universal quantification over related pairs, and the ledger L is the constant debit-credit ledger.
proof idea
This is a one-line wrapper that applies the discrete edge rule DE to the potential induced by the ledger.
why it matters
It provides the hypothesis used by the uniqueness lemmas unique_on_inBall, unique_on_reachN and unique_up_to_const_on_component. These lemmas establish that affine ledgers agree on potentials within balls and up to constants on connected components. The construction ties ledger data to the potential theory that underpins the forcing chain and dimension results in Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.