Foundation Variational Dynamics Uniform Is Variational Successor

The uniform successor

A ledger is a discrete record of events, and in Recognition Science each entry is a positive number. The framework models change from one state to the next by a rule: the next state must be reachable from the current one, and among all reachable states it must have the smallest possible total defect, a measure of how far the entries are from being equal to 1. The declaration uniform_is_variational_successor proves that the state in which every entry is the same number, chosen so that the ledger's conserved charge is preserved, is always such a minimizer. In plain terms, when the ledger is allowed to change, spreading its values out evenly is never a mistake: it is always a legal and optimal next step.

The conserved charge is the sum of the logarithms of the entries, and it is invariant under the update rule. The uniform state with the same charge is therefore always feasible, meaning it is reachable in one tick. The theorem states that this uniform state is not just feasible but optimal: no other reachable state has a smaller total defect. This is a consequence of the strict convexity of the cost function J, which forces a unique minimizer. The result is one of several that together specify the ledger's equation of motion, the map from one state to the next that earlier modules had left unspecified.

The theorem does not claim that the ledger always moves to the uniform state. It claims only that the uniform state is a valid successor, and that it is the unique one with the minimum defect. Other states may also be feasible, but they cannot have a lower defect. The theorem also does not claim that the uniform state is reached in finite time, nor that the ledger's dynamics are continuous in time. It is a statement about a single step, not about the whole trajectory, although other theorems in the same module do establish that trajectories exist and are deterministic.

In Recognition Science, this result is part of a larger chain that derives physical constants and the structure of space from the cost function. The uniform successor is the simplest possible evolution, and the fact that it is always optimal is a strong constraint on the ledger's behavior. It means that the ledger, when left to its own dynamics, tends toward uniformity, and that this tendency is not a choice but a consequence of the cost function's shape.

The declaration is a theorem in the machine-checked library of formal theorems, and it is axiom-clean, meaning it relies only on the standard axioms of the underlying type theory. It is not a hypothesis or a model choice; it is a proved statement about the framework's own definitions.

/-- **Theorem (Explicit Solution)**:
    For any configuration c with log-charge σ, the uniform configuration
    with charge σ is the variational successor.

    This is the explicit "equation of motion":
      entries(t+1) = [exp(σ/N), exp(σ/N), ..., exp(σ/N)]
    where σ = ∑ᵢ log(entries(t)ᵢ).

    The uniform distribution minimizes total J-cost subject to fixed
    log-sum (by Jensen's inequality on the convex function J). -/
theorem uniform_is_variational_successor {N : ℕ} (hN : 0 < N)
    (c : Configuration N) :
    IsVariationalSuccessor c (uniform_config hN (log_charge c)) := by
  simpa [uniform_config, constant_config] using
    (show IsVariationalSuccessor c (constant_config (log_charge c / N)) from by
      constructor
      · show log_charge (constant_config (log_charge c / N) : Configuration N) = log_charge c
        rw [constant_config_log_charge]
        exact mul_div_cancel₀ _ (Nat.cast_ne_zero.mpr (Nat.pos_iff_ne_zero.mp hN))
      · intro c' hc'
        rw [constant_config_total_defect]
        have hbound := total_defect_lower_bound hN c'
        rw [hc'] at hbound
        exact hbound)

/-- **Theorem (Explicit Solution)**:
    For any configuration c with log-charge σ, the uniform configuration
    with charge σ is the variational successor.

    This is the explicit "equation of motion":
      entries(t+1) = [exp(σ/N), exp(σ/N), ..., exp(σ/N)]
    where σ = ∑ᵢ log(entries(t)ᵢ).

    The uniform distribution minimizes total J-cost subject to fixed
    log-sum (by Jensen's inequality on the convex function J). -/
theorem uniform_is_variational_successor {N : ℕ} (hN : 0 < N)
    (c : Configuration N) :
    IsVariationalSuccessor c (uniform_config hN (log_charge c)) := by
  simpa [uniform_config, constant_config] using
    (show IsVariationalSuccessor c (constant_config (log_charge c / N)) from by
      constructor
      · show log_charge (constant_config (log_charge c / N) : Configuration N) = log_charge c
        rw [constant_config_log_charge]
        exact mul_div_cancel₀ _ (Nat.cast_ne_zero.mpr (Nat.pos_iff_ne_zero.mp hN))
      · intro c' hc'
        rw [constant_config_total_defect]
        have hbound := total_defect_lower_bound hN c'
        rw [hc'] at hbound
        exact hbound)

/-- **Theorem (Variational Step Existence)**:
    A total-defect minimizer always exists in the feasible set.

    The proof constructs the minimizer explicitly: it is the configuration
    where every entry equals exp(log_charge(c) / N), distributing the
    conserved charge equally. This is the AM-GM-optimal configuration. -/
theorem variational_step_exists {N : ℕ} (hN : 0 < N)
    (c : Configuration N) :
    ∃ next : Configuration N, IsVariationalSuccessor c next := by
  let μ := log_charge c / N
  use (constant_config μ : Configuration N)
  constructor
  · show log_charge (constant_config μ : Configuration N) = log_charge c
    rw [constant_config_log_charge]
    unfold μ
    exact mul_div_cancel₀ _ (Nat.cast_ne_zero.mpr (Nat.pos_iff_ne_zero.mp hN))
  · intro c' _hc'
    rw [constant_config_total_defect]
    have hbound := total_defect_lower_bound hN c'
    rw [_hc'] at hbound
    unfold μ
    exact hbound

What this page does not claim

The ledger always moves to the uniform state in one step. The uniform state is reached in finite time. The theorem applies to configurations with zero entries or negative entries.

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: