LocalUpdate
plain-language theorem explainer
LocalUpdate defines a structure for single-entry modifications between ledger configurations of dimension N. Researchers analyzing non-locality in Recognition Science variational dynamics would cite it to separate local changes from global minimizers. The definition is a direct structure declaration with an index field and a fixed-entries predicate.
Claim. Let $c$ and $c'$ be configurations of $N$ positive real entries. A local update consists of an index $k$ in the finite set of size $N$ together with the condition that $c'_i = c_i$ for every index $i$ distinct from $k$.
background
The VariationalDynamics module formalizes the ledger update rule as the argmin of total defect over feasible configurations that preserve log-charge. Configuration N is the structure of maps from Fin N to positive reals, each entry a ratio whose J-cost contributes to the global sum. The module rests on LawOfExistence (J has unique minimum at 1), InitialCondition (zero initial defect), TimeEmergence (defect non-increasing), and Determinism (convexity yields unique minimizers).
proof idea
This is a structure definition introducing two fields: the changed index of type Fin N and the predicate that all other entries remain unchanged. No lemmas or tactics are applied.
why it matters
The structure is invoked by the downstream theorem update_is_global, which exhibits configurations where the variational successor alters more than one entry. It thereby supports the module claim that the update is fundamentally non-local because each entry's optimal value depends on the full configuration through the shared conservation constraint. This fills the gap between knowing the energy landscape and specifying the discrete evolution map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.