LocalUpdate
plain-language theorem explainer
LocalUpdate is the structure that encodes a one-entry modification to a ledger configuration while leaving all other entries unchanged. Researchers formalizing the non-local character of variational evolution in Recognition Science cite it when separating local perturbations from the global argmin of total J-cost. The definition consists of a direct structure declaration with an index field and a universal equality constraint on the remaining coordinates.
Claim. A local update from configuration $c$ to $c'$ (each a map from Fin $N$ to positive reals) consists of an index $k$ together with the requirement that $c'_i = c_i$ for every $i$ distinct from $k$.
background
The module VariationalDynamics supplies the missing evolution rule for the Recognition ledger: each tick replaces a configuration by the feasible successor that minimizes total defect (sum of J-costs). Configuration, imported from InitialCondition, is the type of an N-tuple of positive real entries whose log-ratios sum to zero under the conservation law. J itself is the unique function satisfying J(x) = J(1/x) with minimum at x = 1, as established in LawOfExistence. The module doc states that the update is simultaneous across all entries and therefore depends on the entire current state through the shared charge constraint.
proof idea
The declaration is a plain structure definition; it introduces the two fields changed_index and others_fixed with no further proof obligations.
why it matters
LocalUpdate supplies the precise negation target for the downstream theorem update_is_global, which asserts that for N ≥ 2 the variational successor (the global J-cost minimizer) cannot be realized by any single-entry change. This directly supports the module's claim that ledger evolution is fundamentally non-local because of the conservation law on total log-ratio. The construction therefore closes the gap between the existence of a unique minimizer (from Determinism) and the concrete statement that the dynamics cannot be decomposed into independent local rules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.