Foundation Variational Dynamics

The Equation of Motion

Foundation variational dynamics is the ledger (the record of recognition events) update rule in Recognition Science. Earlier results fixed the cost function J(x) = (x + 1/x)/2 - 1, showed that the initial state has zero defect, and established that defect never increases along a tick. What was missing was the specific map from state(t) to state(t+1): the difference between knowing the energy surface and knowing the equation of motion. This module supplies that map.

The ledger evolves by constrained global J-cost minimization. The next state is the configuration that minimizes total defect among all configurations reachable from the current state in one tick, subject to a conservation law. The conserved quantity is the total log-ratio, the sum of logarithms of all entries, which follows from the symmetry J(x) = J(1/x). The update is simultaneous across all entries: the minimizer is a function of the entire current configuration, not of individual entries. Recognition is therefore a non-local process, where the optimal update of one entry depends on all others through the shared constraint.

The module proves that a successor always exists, that it is unique, that total defect is non-increasing along the evolution, and that the evolution is fully determined by the initial state. It also proves that the variational step produces a valid RecognitionStep, the previously defined ledger transition. A zero-defect trajectory is constant at unity, and the unity configuration is an equilibrium for zero-charge states. The theorems are established in Lean 4 with no RS-specific axioms.

The consequence is a deterministic dynamics for the ledger. From any initial state, the evolution is fixed, defect decreases monotonically, and the dynamics is bounded below by zero defect. This turns the static cost function into a process, the missing equation of motion for Recognition Science.

THEOREM IsVariationalSuccessor · Feasible · IndisputableMonolith/Foundation/VariationalDynamics.lean

THEOREM variational_step_exists · IndisputableMonolith/Foundation/VariationalDynamics.lean

THEOREM variational_step_unique · IndisputableMonolith/Foundation/VariationalDynamics.lean

THEOREM variational_step_reduces_defect · trajectory_defect_monotone · IndisputableMonolith/Foundation/VariationalDynamics.lean

THEOREM variational_dynamics_deterministic · IndisputableMonolith/Foundation/VariationalDynamics.lean

THEOREM variational_implies_recognition_step · IndisputableMonolith/Foundation/VariationalDynamics.lean

What this page does not claim

No claim that the variational dynamics is the only possible update rule consistent with the ledger axioms. No claim that the conservation law is derived from the cost function alone; it is a definitional choice in this module. No claim that the dynamics has been connected to any physical equation of motion beyond the ledger formalism.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/VariationalDynamics.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: