PhysicsLogic / Metropolis 1953

Deleting Rejections Changes the Sample

Convergence does not repair bias caused by keeping only accepted events.

Definitions and assumptions

Scope and physical limitations

The independent two-state energy model has E(false)=0, E(true)=log 2 and beta=1. Fresh symmetric proposals switch with probability q; Metropolis acceptance is min(1,exp(E(before)-E(after))). Rejection repeats the old configuration, while an accepted self-proposal is a distinct event that also leaves it unchanged. Physical results retain 0<q<=1. The conditional accepted-event kernel comes from summing the actual masses for zero, one, or more preceding rejections. Its invariant law is proportional to canonical weight times acceptance rate, not to the canonical weight alone. At q=1/2 both chains converge from the specified definite preparation, but the high-energy limits are 1/3 and 2/5. Inverse acceptance-rate weighting restores the stationary canonical law. This is not the original rigid-disk simulation, a process in physical time, a jump chain that records only configuration changes, or a finite-sample accuracy guarantee.

Other arguments
Examples and distinctions

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

Exact root statement

(∀ (state : Bool),
    Tendsto (fun steps => (attempts (1 / 2)).evolveSteps steps prepared state) atTop (nhds (target state))) ∧
  (∀ (state : Bool),
      Tendsto (fun steps => (retained (1 / 2)).evolveSteps steps prepared state) atTop
        (nhds (retainedLaw (1 / 2) state))) ∧
    target true = 1 / 3 ∧ retainedLaw (1 / 2) true = 2 / 5
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

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

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

Constructors, projections, and other meaning dependencies

  • 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