Encyclopedia Foundation Foundation Variational Dynamics Eq Constant Config Of Defect Eq

ARTICLE 3 claims 3 theorems

Foundation Variational Dynamics Eq Constant Config Of Defect Eq

A machine-checked theorem pins down when a ledger's total defect equals a simple average, forcing every entry to the same value.

Verify this page

The equality condition

A ledger in Recognition Science is a discrete record of positive numbers, one per entry, that evolves by minimizing a cost function called total defect. The cost function J(x) = (x + 1/x)/2 - 1 measures how far an entry sits from 1, the value of perfect balance. A configuration is a snapshot of all entries at one tick, and the ledger's charge is the sum of the logarithms of those entries, a quantity the update rule conserves.

The theorem eq_constant_config_of_defect_eq states a precise equality condition. If a configuration's total defect equals N times J applied to the average log-charge per entry, where N is the number of entries, then every entry must equal exp(average log-charge). In plainer terms: when the total cost hits the lower bound set by the average, the only way to get there is for all entries to be identical. The proof uses strict convexity of J, which rules out any spread around the mean as strictly more costly.

This result is a lemma inside a larger machine-checked library of formal theorems. It supports the framework's claim that the ledger's evolution is deterministic: from a given state, the next state is unique. It also feeds the theorem that a zero-defect trajectory is constant, meaning once the ledger reaches perfect balance, it stays there. The declaration itself is private, an internal step, not a standalone law of motion.

What the declaration does not claim is broader. It does not assert that every configuration reaches this constant state, only that if the defect equals the bound, the configuration is constant. It does not specify how fast the ledger approaches balance, nor does it say the constant state is the only equilibrium for nonzero charge. The theorem is conditional: the equality of defect to the bound is the hypothesis, and the conclusion is uniformity of entries.

THEOREM eq_constant_config_of_defect_eq · IndisputableMonolith/Foundation/VariationalDynamics.lean
eq_constant_config_of_defect_eq · IndisputableMonolith/Foundation/VariationalDynamics.lean:189 
/-- Equality in the Jensen bound forces the configuration to be uniform. -/
private theorem eq_constant_config_of_defect_eq {N : ℕ} (hN : 0 < N) (c : Configuration N)
    (hEq : total_defect c = (N : ℝ) * Jlog (log_charge c / N)) :
    c.entries = (constant_config (log_charge c / N) : Configuration N).entries := by
  have hN_pos : (0 : ℝ) < N := Nat.cast_pos.mpr hN
  have hw_pos : ∀ i ∈ (Finset.univ : Finset (Fin N)), 0 < (1 / (N : ℝ)) := by
    intro _ _
    exact one_div_pos.mpr hN_pos
  have hw_sum : ∑ i ∈ (Finset.univ : Finset (Fin N)), (1 / (N : ℝ)) = 1 := by
    rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
    field_simp [hN_pos.ne']
  have hmem : ∀ i ∈ (Finset.univ : Finset (Fin N)), Real.log (c.entries i) ∈ (Set.univ : Set ℝ) := by
    intro _ _
    simp
  have hEq' : Jlog (log_charge c / N) = (1 / (N : ℝ)) * total_defect c := by
    have hN_ne : (N : ℝ) ≠ 0 := hN_pos.ne'
    calc
      Jlog (log_charge c / N)
          = (1 / (N : ℝ)) * ((N : ℝ) * Jlog (log_charge c / N)) := by
              field_simp [hN_ne]
      _ = (1 / (N : ℝ)) * total_defect c := by rw [← hEq]
  have hMapEq :
      Jlog (∑ i ∈ (Finset.univ : Finset (Fin N)), (1 / (N : ℝ)) • Real.log (c.entries i)) =
        ∑ i ∈ (Finset.univ : Finset (Fin N)), (1 / (N : ℝ)) • Jlog (Real.log (c.entries i)) := by
    have hMapEq0 :
        Jlog (∑ i : Fin N, (1 / (N : ℝ)) * Real.log (c.entries i)) =
          ∑ i : Fin N, (1 / (N : ℝ)) * Jlog (Real.log (c.entries i)) := by
      rw [weighted_log_average hN c, weighted_Jlog_average c]
      exact hEq'
    simpa [smul_eq_mul] using hMapEq0
  have hall :=
    (Jlog_strictConvexOn.map_sum_eq_iff
      (t := (Finset.univ : Finset (Fin N)))
      (w := fun _ : Fin N => (1 / (N : ℝ)))
      (p := fun i : Fin N => Real.log (c.entries i))
      hw_pos hw_sum hmem).mp hMapEq
  funext i
  have hlog : Real.log (c.entries i) = log_charge c / N := by
    have hlog0 : Real.log (c.entries i) = ∑ i : Fin N, (1 / (N : ℝ)) * Real.log (c.entries i) := by
      simpa [smul_eq_mul] using hall i (by simp)
    rw [weighted_log_average hN c] at hlog0
    exact hlog0
  have hexp := congrArg Real.exp hlog
  simpa [constant_config, Real.exp_log (c.entries_pos i)] using hexp
THEOREM total_defect_lower_bound · IndisputableMonolith/Foundation/VariationalDynamics.lean
total_defect_lower_bound · IndisputableMonolith/Foundation/VariationalDynamics.lean:159 
/-- Jensen lower bound: fixed log-charge implies a defect lower bound. -/
private theorem total_defect_lower_bound {N : ℕ} (hN : 0 < N) (c : Configuration N) :
    (N : ℝ) * Jlog (log_charge c / N) ≤ total_defect c := by
  have hN_pos : (0 : ℝ) < N := Nat.cast_pos.mpr hN
  have hw_nonneg : ∀ i ∈ (Finset.univ : Finset (Fin N)), 0 ≤ (1 / (N : ℝ)) := by
    intro _ _
    positivity
  have hw_sum : ∑ i ∈ (Finset.univ : Finset (Fin N)), (1 / (N : ℝ)) = 1 := by
    rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
    field_simp [hN_pos.ne']
  have hmem : ∀ i ∈ (Finset.univ : Finset (Fin N)), Real.log (c.entries i) ∈ (Set.univ : Set ℝ) := by
    intro _ _
    simp
  have hJensen :=
    Jlog_strictConvexOn.convexOn.map_sum_le
      (t := (Finset.univ : Finset (Fin N)))
      (w := fun _ : Fin N => (1 / (N : ℝ)))
      (p := fun i : Fin N => Real.log (c.entries i))
      hw_nonneg hw_sum hmem
  have hJensen' :
      Jlog (log_charge c / N) ≤ (1 / (N : ℝ)) * total_defect c := by
    have hJensen0 :
        Jlog (∑ i : Fin N, (1 / (N : ℝ)) * Real.log (c.entries i)) ≤
          ∑ i : Fin N, (1 / (N : ℝ)) * Jlog (Real.log (c.entries i)) := by
      simpa [smul_eq_mul] using hJensen
    rw [weighted_log_average hN c, weighted_Jlog_average c] at hJensen0
    exact hJensen0
  have hmul := mul_le_mul_of_nonneg_left hJensen' hN_pos.le
  simpa [div_eq_mul_inv, hN_pos.ne', mul_comm, mul_left_comm, mul_assoc] using hmul
THEOREM eq_constant_config_of_defect_eq · IndisputableMonolith/Foundation/VariationalDynamics.lean
eq_constant_config_of_defect_eq · IndisputableMonolith/Foundation/VariationalDynamics.lean:189 
/-- Equality in the Jensen bound forces the configuration to be uniform. -/
private theorem eq_constant_config_of_defect_eq {N : ℕ} (hN : 0 < N) (c : Configuration N)
    (hEq : total_defect c = (N : ℝ) * Jlog (log_charge c / N)) :
    c.entries = (constant_config (log_charge c / N) : Configuration N).entries := by
  have hN_pos : (0 : ℝ) < N := Nat.cast_pos.mpr hN
  have hw_pos : ∀ i ∈ (Finset.univ : Finset (Fin N)), 0 < (1 / (N : ℝ)) := by
    intro _ _
    exact one_div_pos.mpr hN_pos
  have hw_sum : ∑ i ∈ (Finset.univ : Finset (Fin N)), (1 / (N : ℝ)) = 1 := by
    rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
    field_simp [hN_pos.ne']
  have hmem : ∀ i ∈ (Finset.univ : Finset (Fin N)), Real.log (c.entries i) ∈ (Set.univ : Set ℝ) := by
    intro _ _
    simp
  have hEq' : Jlog (log_charge c / N) = (1 / (N : ℝ)) * total_defect c := by
    have hN_ne : (N : ℝ) ≠ 0 := hN_pos.ne'
    calc
      Jlog (log_charge c / N)
          = (1 / (N : ℝ)) * ((N : ℝ) * Jlog (log_charge c / N)) := by
              field_simp [hN_ne]
      _ = (1 / (N : ℝ)) * total_defect c := by rw [← hEq]
  have hMapEq :
      Jlog (∑ i ∈ (Finset.univ : Finset (Fin N)), (1 / (N : ℝ)) • Real.log (c.entries i)) =
        ∑ i ∈ (Finset.univ : Finset (Fin N)), (1 / (N : ℝ)) • Jlog (Real.log (c.entries i)) := by
    have hMapEq0 :
        Jlog (∑ i : Fin N, (1 / (N : ℝ)) * Real.log (c.entries i)) =
          ∑ i : Fin N, (1 / (N : ℝ)) * Jlog (Real.log (c.entries i)) := by
      rw [weighted_log_average hN c, weighted_Jlog_average c]
      exact hEq'
    simpa [smul_eq_mul] using hMapEq0
  have hall :=
    (Jlog_strictConvexOn.map_sum_eq_iff
      (t := (Finset.univ : Finset (Fin N)))
      (w := fun _ : Fin N => (1 / (N : ℝ)))
      (p := fun i : Fin N => Real.log (c.entries i))
      hw_pos hw_sum hmem).mp hMapEq
  funext i
  have hlog : Real.log (c.entries i) = log_charge c / N := by
    have hlog0 : Real.log (c.entries i) = ∑ i : Fin N, (1 / (N : ℝ)) * Real.log (c.entries i) := by
      simpa [smul_eq_mul] using hall i (by simp)
    rw [weighted_log_average hN c] at hlog0
    exact hlog0
  have hexp := congrArg Real.exp hlog
  simpa [constant_config, Real.exp_log (c.entries_pos i)] using hexp

What this page does not claim

The theorem does not claim every configuration evolves to the constant state. It does not specify the speed of convergence toward equilibrium. It does not assert the constant state is the only equilibrium for nonzero charge.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND