LocalUpdate
LocalUpdate introduces a structure capturing single-entry modifications to finite ledger configurations while preserving all other entries. Researchers studying non-locality of the variational update rule cite it when showing that global J-cost minimization cannot reduce to isolated changes. The declaration is supplied directly as a structure definition with an index field and an invariance predicate.
claimLet $c$ and $c'$ be configurations of $N$ positive real entries. A local update from $c$ to $c'$ is given by an index $k$ in the finite set of size $N$ together with the requirement that $c'_i = c_i$ for all indices $i$ distinct from $k$.
background
The Variational Dynamics module supplies the missing update rule for the Recognition Science ledger: each step selects the feasible configuration minimizing total defect subject to conservation of the sum of log-ratios. A configuration consists of $N$ positive real entries together with the positivity condition; total defect is the sum of individual J-costs where $J(x) = (x + x^{-1})/2 - 1$. The module states that the update is simultaneous and global because the minimizer depends on the entire current state through the shared conservation law.
proof idea
This declaration is a structure definition with no proof body. It directly encodes the two data required to express a single-index change: the changed index and the predicate asserting that every other entry remains fixed.
why it matters in Recognition Science
The structure is invoked by the downstream theorem update_is_global, which exhibits configurations (for $N=2$) whose variational successor alters more than one entry and therefore lies outside every LocalUpdate. This supplies the concrete witness that the ledger evolution is fundamentally non-local, consistent with the module's statement that optimal evolution of each entry depends on all others through the conservation constraint.
scope and limits
- Does not define the actual variational successor map or the feasible set.
- Does not assert existence of any update, local or global.
- Applies only to finite $N$; no statement about continuum limits.
- Does not address whether local updates preserve the conservation law.
formal statement (Lean)
413structure LocalUpdate {N : ℕ} (c c' : Configuration N) where
414 changed_index : Fin N
415 others_fixed : ∀ i, i ≠ changed_index → c'.entries i = c.entries i
416
417/-- **Theorem (Update Is Global)**:
418 The variational successor generally cannot be achieved by a local update.
419
420 Specifically: for N ≥ 2, there exist configurations where the
421 variational successor modifies more than one entry.
422
423 This makes the update rule fundamentally NON-LOCAL — the optimal
424 evolution of each entry depends on the state of all other entries
425 through the shared conservation constraint. -/