PhysicsLogic / Metropolis 1953

Balance Is Not Relaxation

One explicit two-state sampler separates a stationary law, a prepared distribution, and an empirical average.

Definitions and assumptions

Scope and physical limitations

Two equal-energy states have canonical weights 1/2 at beta=1. At each update the state switches with probability p and stays with probability 1-p; stochasticity holds exactly for 0 <= p <= 1. Prepared laws start at either definite state. For p=1 every trajectory alternates, every state is reachable, and detailed balance holds, but the prepared law stays distance 1/2 from equilibrium in one state probability. The empirical mean of the signed observation nevertheless converges, with error at most 1/N for each nonempty sample. For 0 < p < 1 the prepared law and signed ensemble mean converge; p=3/4 supplies an alternating, decaying mode. Steps are algorithmic updates, not physical time. Reachability permits zero steps to the initial state. The empty sample is totalized by Lean but is not used as an empirical estimate. This is an independent finite diagnostic, not either original spatial or gauge algorithm.

Other arguments
Examples and distinctions

Constructed examples of this model; each answer includes the Lean statement.

Exact root statement

(update 1).DetailedBalanceAt target ∧
  (update 1).NonvacuousFiniteStationaryUpdateAt target ∧
    (∀ (initial final : Bool), ∃ steps ≤ 1, 0 < (update 1).evolveSteps steps (prepared initial) final) ∧
      ∀ (initial : Bool),
        ¬Tendsto (fun steps => (update 1).evolveSteps steps (prepared initial) true) atTop (nhds (target true))
Compare two arguments

Compare their definitions and hypotheses. Shared declarations may be instantiated differently; differences do not establish equivalence or implication.

No comparison argument selected.

Compare an earlier extraction

Compare the displayed specifications with an earlier JSON export. This compares text, not mathematical equivalence. Files stay in this browser.

No earlier extraction selected.

Notes and questions

Note for

Unsubmitted text stays in this tab when navigating declarations, but is not saved across reloads.

Import merges local entries without overwriting them.

All declarations in the selected argument

Definitions, structures, and assumptions

Structures, classes, and inductive alternatives

  • structure
  • structure
  • structure
  • structure
  • structure

Definitions and domain choices

  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition

Checked statements: parameters, hypotheses, and interpretation

  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement

Constructors, projections, and other meaning dependencies

  • constructor
  • constructor
  • constructor
  • constructor
  • constructor

External mathematical declarations

  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary
  • external type boundary