LocalUpdate
plain-language theorem explainer
A structure that encodes a single-entry modification between two ledger configurations of size N, recording the changed index together with the predicate that every other entry is identical. Researchers formalizing the non-local character of variational evolution in Recognition Science cite this record when separating local perturbations from the global argmin of total defect. The definition is a direct inductive record with no computational content.
Claim. Let $c$ and $c'$ be configurations of $N$ positive real ledger entries. A local update from $c$ to $c'$ consists of an index $k$ in the finite set of size $N$ together with the assertion that $c'_i = c_i$ for every index $i$ distinct from $k$.
background
The VariationalDynamics module supplies the missing evolution rule for the Recognition Science ledger: each tick replaces the current configuration by the feasible successor that globally minimizes total defect, where defect is the sum of per-entry J-costs and feasibility respects the conserved log-charge sum. A Configuration N is the structure whose entries field maps each Fin N to a positive real; this is imported from InitialCondition and carries the positivity hypothesis used throughout the module. J itself is the function J(x) = (x + x^{-1})/2 - 1 whose unique minimum at unity was established in LawOfExistence; the present structure isolates the purely syntactic notion of a change that touches only one coordinate while leaving the conservation constraint untouched.
proof idea
The declaration is a plain structure definition that packages the changed index of type Fin N and the universal quantifier asserting that all other entries are copied verbatim. No tactics or lemmas are applied; the record is introduced directly as an inductive type whose fields are exactly the two listed components.
why it matters
LocalUpdate supplies the precise negation target for the downstream theorem update_is_global, which exhibits an explicit two-entry configuration whose variational successor alters both entries and therefore lies outside every LocalUpdate instance. The construction thereby substantiates the module's central claim that the update rule is fundamentally non-local because the shared log-charge constraint couples every entry to every other. It closes the gap left by the earlier modules (LawOfExistence, InitialCondition, TimeEmergence, Determinism) that had characterized the energy landscape but not the concrete map realizing the global minimizer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.