Foundation Ground State Dynamics Ratio Config

The ratio configuration

A ratio is a comparison of two quantities. In the Recognition Science framework, which models reality as a discrete record of recognition events, a ratio becomes a configuration: a finite list of positive entries that describe a state of the system. The declaration ratioConfig packages any positive real number r into the simplest possible configuration, one with a single entry. It is a definitional choice, a way to name a one-channel ratio so that the framework's dynamics can ask what happens to it.

The framework's dynamics are built around a ledger, a discrete record of events, and a variational update rule: each step moves to the configuration that minimizes a conserved quantity. For a one-entry configuration, the conserved quantity is the logarithm of the ratio itself. The framework proves that any equilibrium, a state stable under the update rule, coincides with the uniform minimizer of its conserved sector. In the zero-charge sector, where the logarithm of the ratio is zero, the unique equilibrium is the unity configuration, the state where every entry equals 1.

The consequence is direct. If a one-channel ratio is stable, meaning it is an equilibrium, and it lies in the neutral sector, meaning its logarithm is zero, then the ratio must equal 1. The theorem stable_zero_charge_ratio_eq_one states this: for any positive real r, if the configuration ratioConfig r is an equilibrium and its log-charge is zero, then r = 1. This is a proved result in the machine-checked library of formal theorems, derived from the variational step uniqueness and the zero-charge equilibrium theorem.

This result matters because it shows how stability alone, without any fitted parameters, forces a specific value. The framework does not claim that all ratios are 1, only that stable ratios in the neutral sector are. It also does not claim that the ratio 1 is the only possible value in other sectors, nor does it claim anything about the physical meaning of a ratio beyond the formal dynamics. The declaration is a tool for studying one-channel systems, and the theorem is a boundary condition on what stability can allow.

/-- A one-channel ratio packaged as a `Configuration 1`. -/
def ratioConfig (r : ℝ) (hr : 0 < r) : Configuration 1 where
  entries := fun _ => r
  entries_pos := fun _ => hr

/-- Any equilibrium coincides with the uniform minimizer of its conserved sector. -/
theorem equilibrium_entries_eq_uniform {N : ℕ} (hN : 0 < N)
    (c : Configuration N) (hEq : IsEquilibrium c) :
    c.entries = (uniform_config hN (log_charge c)).entries := by
  exact variational_step_unique hN c c (uniform_config hN (log_charge c))
    hEq (uniform_is_variational_successor hN c)

/-- The zero-charge equilibrium is the unity configuration. -/
theorem zero_charge_equilibrium_is_unity {N : ℕ} (hN : 0 < N)
    (c : Configuration N) (hEq : IsEquilibrium c)
    (hCharge : log_charge c = 0) :
    c.entries = (unity_config N hN).entries := by
  calc
    c.entries = (uniform_config hN (log_charge c)).entries :=
      equilibrium_entries_eq_uniform hN c hEq
    _ = (uniform_config hN 0).entries := by rw [hCharge]
    _ = (unity_config N hN).entries := by
      funext i
      simp [uniform_config, unity_config]

/-- Stable one-channel ratios in the neutral sector are forced to unity. -/
theorem stable_zero_charge_ratio_eq_one (r : ℝ) (hr : 0 < r)
    (hEq : IsEquilibrium (ratioConfig r hr))
    (hCharge : log_charge (ratioConfig r hr) = 0) :
    r = 1 := by
  have hEntries :
      (ratioConfig r hr).entries = (unity_config 1 (by norm_num)).entries :=
    zero_charge_equilibrium_is_unity (N := 1) (by norm_num) (ratioConfig r hr) hEq hCharge
  have h0 := congrFun hEntries ⟨0, by simp⟩
  simpa [ratioConfig, unity_config] using h0

What this page does not claim

The declaration does not define a physical ratio, only a formal one-entry configuration. The theorem does not claim that all stable ratios equal 1, only those in the zero-charge sector. The framework does not claim that the ratio 1 is the only possible stable value across all sectors.

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/GroundStateDynamics.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: