PhysicsLogic · Paper-first editionLean-extracted article 115

Formal reconstruction · rapid-falloff minimum-image finite periodic cell, canonical configuration target, rejection of naive weighted sampling, positive-width periodic local proposals, successive finite-probability move attempts, energy-based acceptance, rejected-state counting, detailed balance, accessibility, asymptotic equilibration, rigid-sphere overlap rejection, exact virial/contact-density equations (7)-(10), finite MANIAC evidence, and convergence/finite-size scope

Equation of State Calculations by Fast Computing Machines

The modified Monte Carlo argument from canonical target to finite rigid-sphere evidence—without turning asymptotic sampling into molecular dynamics or a thermodynamic-limit theorem

Original work encoded in Lean: N. Metropolis, A. W. Rosenbluth, M. N. Rosenbluth, A. H. Teller, and E. Teller Edition: human-readable logical reconstruction
Formal objectPhysicsLogic.Papers.Metropolis1953
Physical resultA finite periodic classical particle cell with spherical two-body interactions and rapidly falling potential uses the minimum periodic image contribution, represents the selected one-phase substance, and reduces surface effects. For velocity-independent forces, the canonical average reduces to a Boltzmann-weighted configuration integral. Uniform configuration sampling followed by weighting is impractical in dense systems, motivating a positive-width symmetric one-particle displacement update with periodic wraparound, successive particle attempts, finite-probability allowed moves, and an explicit selected-update/proposal link: the disjoint conditions DeltaE < 0 and 0 < DeltaE trigger downhill acceptance and uphill acceptance with probability exp(-DeltaE/kT), rejected moves retain the old configuration, and every attempt counts as a sample. The supplied forward/reverse flux calculation establishes detailed balance, while a separate repeated-local-move argument consumes the finite periodic model and complete move protocol to supply configuration accessibility. Together with an equilibration calculation and ensemble interpretation, these yield asymptotic canonical sampling. For rigid spheres the rule becomes acceptance of nonoverlapping moves and rejection of overlaps. The pressure route retains the selected real-valued Clausius virial, mean-contact-force, internal-virial, and pressure equations (7)-(10), rather than only a named virial bridge; finite runs with discarded transients, radial-distribution extrapolation, model comparisons, and roughly three-percent statistical error provide qualified equation-of-state evidence. No finite convergence rate, physical-dynamics interpretation, exact thermodynamic-limit equation of state, or finite-size systematic control is established.
Argument architecture8 routes · 30 semantic claims · 30 sourced steps · 1 finite-periodic root · 1 canonical-reduction route · 1 algorithm-construction route · 1 asymptotic-equilibration route · 1 rigid-sphere specialization · 1 virial route with retained source formulas · 1 finite numerical-evidence route · 1 scope route · 1 grounded shared equilibrium-sampling model · 20 formal countermodels · 5 dependency audits · 6 status audits

Definitions, structures, and assumptions

Structures, classes, and inductive alternatives

  • structureThe selected asymptotic algorithmic-sampling phenomenon. Its type is distinct from the structural constraint so a declared output cannot explain itself.
  • structure
  • structureProof-free selected physical data and their indexed source relations.
  • inductiveDistinct source arguments that can yield the same normalized energy law.
  • structure
  • structure
  • inductiveA state-list sum and a configuration-space integral are different data.
  • inductiveThe shared semantic claims carried by the equilibrium-sampling route. These claims deliberately stop short of certifying a selected finite run. Metropolis et al. and Creutz both use an asymptotic convergence route, while finite-run convergence remains an independent paper-local obligation.
  • structure
  • structure
  • structurePaper-local interpretation of an asymptotic equilibrium-sampling model. The shared convergence route does not determine which physical theory uses the update, which sampling process it represents, or what equilibrium production means in that theory and world.
  • structureProof-free data and relation families selected by one equilibrium-sampling route. No field supplies a proof of validity, target selection, balance, accessibility, equilibration, or equilibrium production. The selected finite-run predicate remains outside this model because neither shared route establishes it.
  • structureThe four selected indices constrained by one complete equilibrium-sampling route. This type contains no validity, balance, accessibility, convergence, or equilibrium-production proof.
  • structureA paper-local theory object paired with the selected sampling model.
  • structureA paper-local physical sampling process paired with the selected model.
  • structure
  • structure
  • structure
  • structure
  • inductive
  • inductive
  • inductive
  • structure
  • inductive
  • structure
  • structureA selected claim must depend on exactly these source-map steps.
  • structureA selected claim must retain exactly these epistemic statuses.
  • structureA selected route must name exactly these immediate predecessor routes.
  • structure
  • structure
  • inductive
  • inductiveEquation (2) follows from the selected canonical ensemble and momentum separation before the paper introduces its separate sampling algorithm.
  • inductiveTyped name for the original modified-Monte-Carlo sampling route.
  • structureThe physical sampling process represented by the selected asymptotic Metropolis model. Its regime remains explicit because the 1953 argument does not establish convergence for an arbitrary finite run.
  • structure
  • structure
  • structure
  • structure
  • structure
  • structureSource-shaped two-state population readout for the original pp. 1088-1089 acceptance and directional-flow argument.
  • structureThe bias is computed from the actual finite accept/reject chain. The count 64 selects a diagnostic duration, not a reconstruction of the disk data.
  • structure
  • structure
  • structure
  • structure
  • structureBoth update rules sample the same energy model; their dynamics is not assigned.
  • structure
  • inductive
  • structureSelected real-valued content of the rigid-sphere virial calculation in Metropolis et al. Section III.A. The readout keeps journal pp. 1089-1090 equations (7)-(10) paper-local: the Clausius virial identity, averaged contact force, internal-force virial, and pressure equation of state are retained before the named pressure-curve output is used.
  • structureProof-free relation families for one computational inference problem.
  • structureMathematical certification is a separate contract layered over computational support. It is used only by papers that explicitly compare a numerical claim with proof status.
  • structure
  • structure
  • structure
  • structureThe exact scope shared by target-production and viability questions.
  • structureA mechanism produces targets within a declared scope.
  • structure

Definitions and domain choices

  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionValidity, physical selections, the exact normalization branch, and a genuinely inhabited selected domain.
  • definitionThe partition function is the selected normalization of the actual exponential energy weight and cannot be zero or negative.
  • definitionThe selected probability or probability density is normalized by its own physical sum or measure integral.
  • 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
  • definition
  • definition
  • definition
  • definition
  • definitionA source-sensitive explanation of the selected sampling phenomenon.
  • definitionThe complete selected algorithmic route structurally explains its asymptotic equilibrium-sampling phenomenon in the declared regime.
  • definitionThe selected model is exactly context-induced at its four physical indices. This equality retains every route-used relation family while excluding the paper-local finite-run predicate.
  • definitionThe exact pre-convergence sampling setup used for theory/model/world grounding. It fixes the context-selected model and requires validity, equilibrium targeting, detailed balance, and target-space accessibility, but assumes neither convergence nor equilibrium production.
  • definition
  • definition
  • definitionPaper-independent semantics of every claim retained by the shared route. The model supplies the selected physical indices and exact relation families.
  • definition
  • definition
  • definitionThe exact proof-free sampling model induced by this context.
  • definition
  • definition
  • definition
  • definition
  • definitionThe unique four-index equilibrium-sampling model selected by the context.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionIdentify the selected update model with a theory and represented process without presupposing convergence or equilibrium production. Those remain model conclusions transferred by the grounding bridges.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe paper-local convergence calculation. Detailed balance and target-space accessibility are inputs to this calculation, not replacements for it.
  • definitionThe physical interpretation that the limiting update process produces the selected equilibrium ensemble.
  • definitionThe complete inhabited asymptotic equilibrium-sampling route, stated directly at one model. Every setup relation, repeated-update convergence claim, and equilibrium-production interpretation holds at the same selected description, regime, update, and ensemble. This proposition remains asymptotic: it does not assert that any selected finite run has already converged.
  • definition
  • definitionDirect terminal outputs of the selected asymptotic sampling route.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe exact asymptotic ensemble-sampling phenomenon selected by the model.
  • definitionThe selected sampling constraint with one paper-local derivation.
  • definitionThe complete typed constraint selected by one sampling model.
  • definition
  • definitionThe selected update produces only its selected equilibrium target, after the actual validity, target, balance, accessibility, and asymptotic-convergence conditions hold. No finite-run convergence or physical-time evolution follows.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionOne update of the retained state only, with no additional hidden state.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionA constructed larger-state dynamics, not a microscopic model of either paper.
  • definitionStates here are normalized laws, not individual configurations.
  • definition
  • definition
  • definition
  • definitionFirst apply the left kernel, then the right kernel.
  • definitionA correlation between consecutive update indices, not a supplied physical clock.
  • definition
  • definition
  • definitionOne algorithmic update; Unit is not a physical clock.
  • definitionThe actual probability of consecutive retained configurations.
  • definition
  • definition
  • definitionPush forward the same initial joint law along the observed first coordinate.
  • definition
  • definition
  • definition
  • definitionImmediate predecessor routes. Claims established by their transitive predecessors are inherited by the dependency closure.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionTemporary reductio-introduction steps discharged by this inference. Discharge removes only those exact origins from the conclusion's epistemic basis; it does not assert the temporary hypotheses globally.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionA source-mapped claim holds when its declared formula evaluates under the given paper-local semantic interpretation.
  • definition
  • definition
  • definition
  • definition
  • definitionEvery claim in the supplied identifier list holds.
  • definitionA source-mapped step is semantically sound when the interpreted premises imply the interpreted conclusion. Physical principles and imported calculations therefore remain explicit hypotheses of paper-specific certificates rather than acquiring truth from their source-map labels. A reductio hypothesis is different: it introduces a temporary assumption into a subargument and therefore is not required to hold globally. Its later uses remain ordinary premise-sensitive steps, and discharging it into a negated conclusion remains an ordinary semantic obligation.
  • definitionEvery step in the supplied identifier list is semantically sound.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe formula declared for a claim identifier, when that claim is present.
  • definition
  • definitionEvery source-mapped step whose justification contributes to the claim through declared premise-to-conclusion steps.
  • definitionAll justification statuses contributed by the exact source-mapped origins of a claim. This records epistemic provenance; it does not assert any paper claim or discharge any physical assumption.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe declared argument step with the requested identifier, when present.
  • definition
  • definitionThe premise list and conclusion attached to a declared step identifier.
  • definition
  • definition
  • definition
  • definition
  • definitionThe complete Lean-side fidelity certificate. The first conjunct is computed from source-map data; the second is supplied by checked route semantics; the third requires each declared independence boundary to have a countermodel.
  • definition
  • definition
  • definition
  • definition
  • definitionA typed countermodel matrix avoids string-keyed audit rows. Each index selects one proposition-valued separation obligation.
  • definition
  • definitionEvery route actually declared in the source map has a semantic certificate under the paper-local interpretation.
  • definition
  • definition
  • definitionOne countermodel row retains a weaker proposition while rejecting a stronger upgrade. This is a proposition, not a structure carrying proof fields.
  • definition
  • definition
  • definitionIndependent dependency and epistemic ledgers must review the same actual source claims, including every public conclusion and the selected paper conclusion. Empty, duplicated, nonexistent, or one-sided entries are invalid.
  • definitionEvery actually declared source route must have exactly one independently reviewed predecessor row. Correct rows for a selected subset are insufficient.
  • definitionThe declared main conclusion must be exposed by at least one public route output, rather than existing only as an unexported source-map claim.
  • definition
  • definition
  • definitionTwo finite lists describe the same dependency set. Duplicate expected entries are rejected so a ledger cannot pass by repeating a label.
  • definitionEvery paper-level, claim-level, and step-level source reference is present and has a nonempty work and locator. PaperArgument.auditable separately checks that every claim and step carries at least one source.
  • definitionA source reference is usable for review only when both the work and its locator are nonempty.
  • definitionStatic fidelity checks that can be evaluated from a paper's source map alone. They do not assert the truth of any physical premise.
  • definitionEvery declared output of a named source route holds under the semantic interpretation. This is the proof obligation discharged by paper-specific Lean theorems.
  • definition
  • definitionA route is fully certified only when both its individual steps and its declared outputs are semantically checked.
  • definitionEvery source-mapped inference step in a named route is semantically sound.
  • definitionEvery route named in the supplied identifier list is semantically certified.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe source-mapped route with the requested identifier, when present.
  • definition
  • definitionThe public semantic interface inherited from predecessor routes. Descendants receive only declared route outputs, not every internal intermediate claim. Outputs still carrying a temporary reductio origin are excluded.
  • definitionAll direct and inherited route dependencies. The route-order check separately ensures that the declared graph is acyclic and topologically ordered.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionA finite energy model of the source accept/reject rule, not the rigid-disk run.
  • 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
  • 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
  • definitionThe p. 1089 pairwise equilibrium claim is quantified over admissible states connected by an actual positive symmetric proposal; its conclusion is the positive, value-level equality of the two directional population fluxes.
  • 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
  • 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
  • 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
  • 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
  • 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
  • definitionA two-state update that remains in its current component with certainty and never crosses between components.
  • 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
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe source's actual Eq. (2) observable is the Boltzmann-weighted configuration integral divided by its partition denominator.
  • definitionThe named canonical target retains all numerical content of its printed configuration-space normalization and average.
  • definitionEquation (2) has a positive physical thermal scale and an actual positive configuration-space partition denominator.
  • definitionThe selected configuration distribution is the normalized Boltzmann density on its actual admissible domain.
  • definition
  • definition
  • definition
  • definition
  • definitionSource p. 1089: a finite sequence of actual positive-probability update steps reaches the second configuration from the first.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionSource equations (5)-(6) compare actual positive directional ensemble fluxes, not a free proposition named for detailed balance.
  • definitionThe two states in the original pp. 1088-1089 population-flow argument belong to the canonical configuration space, and their allowed one-particle proposal has the same strictly positive probability in either direction.
  • definitionOne actual algorithmic step has strictly positive transition probability.
  • definition
  • definition
  • definition
  • definition
  • definitionThe selected rigid-sphere pressure, area, contact density, kinetic energy, and virial values retain Metropolis et al.'s equations (7)-(10).
  • definition
  • definitionThe directional population counts use the uphill proposal multiplied by its Boltzmann acceptance, while the reverse downhill proposal is accepted without suppression. Rejected uphill attempts are therefore not silently removed by renormalizing accepted moves.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionMetropolis ergodicity is connectivity of the admissible configuration space under finite positive-probability update paths, not a named label.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe two source branches are conditional rules, not simultaneous facts about one selected proposal.
  • definition
  • definition
  • definitionJournal p. 1088: `ΔE` is the energy of the proposed configuration minus the energy of the old configuration for the selected energy observable.
  • definition
  • definition
  • definitionThe configuration-space Boltzmann factor in journal p. 1088, Eq. (2).
  • definitionThe exact proof-free shared model selected by the Metropolis route.
  • 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
  • definitionThe source's `kT` denominator must be positive on the selected branch.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe lower-energy branch of the paper's Eq. (3) rule is `ΔE < 0`.
  • definitionThe higher-energy branch of the paper's Eq. (3) rule is `0 < ΔE`.
  • 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
  • definitionMetropolis's shared canonical state retains the actual configuration integral and positive `kT`; its source is not Jaynes's entropy optimization.
  • definitionThe finite rigid-sphere computation has a selected validation scope. Its finite-size systematic and exact thermodynamic-limit status remain separate from the reported statistical error and model comparisons.
  • definition
  • definition
  • definitionPaper-local theory and world meanings of every shared equilibrium-sampling claim. The represented process includes accessibility in addition to the claim's shared semantic content.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionSource pp. 1088-1089: detailed balance is the actual equality of canonical population fluxes for every pair of admissible configurations.
  • definition
  • definition
  • definitionJournal p. 1088, Eq. (3): on the uphill branch the selected update uses the explicit Boltzmann acceptance probability `exp (-ΔE / kT)`.
  • definitionThe uphill acceptance claim is not a free label: it retains the positive energy branch, positive `kT`, and the source's exponential probability.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionJournal p. 1090, equation (8): isotropic Maxwellian collisions give the average contact force `m vbar^2 pi d_0 nbar`.
  • definitionJournal p. 1090, equation (9): the internal-force contribution to the Clausius virial is the negative contact-density term.
  • definitionJournal p. 1089, equation (7): the total Clausius virial equals the boundary pressure term plus the internal-force virial and also equals twice the total kinetic energy. The displayed `E_kin = N m vbar^2 / 2` relation is retained with the same selected values.
  • definitionJournal p. 1090, equation (10): substituting the internal virial into the Clausius identity gives the rigid-sphere equation of state in both the kinetic-energy and `NkT__ forms.
  • definitionPositive physical domain for the selected rigid-sphere equation of state. The signed virial terms remain unrestricted because equation (9) makes the internal contribution negative.
  • definitionThe source-level virial calculation retains the complete equation (7)-(10) chain rather than only a pressure-curve label.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionScoped computational evidence with a relevant check still unpassed.
  • definitionA model-scoped run was executed, produced the selected result, passed a nonempty selected validation family, and supports the selected claim.
  • definitionA selected validation family is nonempty and every selected check matters.
  • definitionEvery check in the selected nonempty family passes.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionMathematical proof is an additional relation, not a validation synonym.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionAt least one forward continuation exists for the selected time and state.
  • definitionExistence and uniqueness for every selected time and initial state. No topology, continuous dependence, error bound, or effective solver is asserted.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionNonvacuous success at one selected admissible initial condition.
  • definition
  • definition
  • definitionA model-to-world interpretation law. It does not assert that the model has produced a conclusion; use `GroundedModelConclusionAt` for that.
  • definitionA model-to-theory interpretation law. It does not assert that the model has produced a conclusion; use `GroundedModelConclusionAt` for that.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionBuild the epistemic dependency basis in paper order. A conclusion inherits the justification origin of its own step and every origin already attached to its premises.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionExpand a set of route identifiers by one dependency edge, iterated with enough fuel to traverse any acyclic graph on the declared routes.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition

Selected instances and coercions

  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance
  • instance

Source mappings and interpretation choices

  • checked statement
  • inductive
  • definition
  • instance
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • recursor
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • inductive
  • definition
  • instance
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • recursor
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • inductive
  • definition
  • instance
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • recursor
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • checked statement
  • checked statement
  • checked statement
  • definition
  • checked statement
  • definition
  • definition
  • instance
  • checked statement
  • checked statement
  • instance
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • checked statement
  • checked statement
  • definition
  • definition
  • inductive
  • definition
  • instance
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • definition
  • checked statement
  • recursor
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • constructor
  • definition
  • checked statement
  • inductive
  • definition
  • instance
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • checked statement
  • recursor
  • definition
  • definition
  • structure
  • definition
  • instance
  • checked statementRaw paper-local inputs construct every Metropolis route in source order.
  • checked statement
  • checked statement
  • definition
  • definition
  • checked statement
  • checked statement
  • definition
  • definition
  • definition
  • definition
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • checked statement
  • definition
  • checked statement
  • checked statement
  • definition
  • definition
  • checked statement
  • recursor
  • definition
  • checked statement
  • checked statementNo completed route certificate is needed to cover a route identifier.
  • checked statement
  • checked statement
  • checked statement
  • inductive
  • definition
  • instance
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • checked statement
  • recursor
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • checked statement
  • checked statement
  • checked statement
  • definition
  • checked statement
  • definition
  • definition
  • instance
  • checked statement
  • checked statement
  • instance
  • checked statement
  • checked statement
  • instance
  • checked statement
  • checked statement
  • instance
  • checked statement
  • checked statement
  • instance
  • checked statement
  • checked statement
  • instance
  • definition
  • definition
  • instance
  • definition
  • definition
  • instance
  • definition
  • definition
  • instance
  • definition
  • definition
  • instance
  • definition
  • definition
  • checked statement
  • definition
  • checked statement
  • definition
  • definition
  • checked statement
  • checked statement
  • checked statement
  • definition
  • checked statement
  • definition
  • definition
  • checked statement
  • definition
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement

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
  • 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
  • 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
  • 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 statementThe exact Metropolis acceptance and symmetric proposal do not balance directional populations when the candidate weights are not the canonical Boltzmann ratio.
  • checked statement
  • checked statement
  • checked statementCounting only accepted moves renormalizes the uphill transition to one, destroying the source population balance even with canonical state weights, positive probabilities, symmetric proposals, and correct downhill moves.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementDetailed balance can hold for every pair while no finite sequence of positive-probability updates connects the two admissible components.
  • 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
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementThe printed canonical density and the two accepted-transition formulas derive the original directional population equality.
  • checked statementA normalized target retains the printed observable average while leaving physical molecular dynamics, finite convergence, and the thermodynamic limit outside the source's demonstrated conclusions.
  • checked statementCompleted canonical sampling keeps finite positive update paths without claiming that any selected finite numerical run has already converged.
  • checked statementThe final asymptotic-sampling result retains the actual source population equation instead of reducing it back to a named detailed-balance predicate.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementThe independently supplied accessibility calculation yields actual finite positive-transition paths between every admissible configuration pair.
  • checked statementGlobal detailed balance retains the actual directional population equality even for disconnected admissible state pairs.
  • checked statementThe completed source-local balance result exposes the original positive population-flow equality independently of the retained global balance label.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementFinite update paths compose, so connectivity really permits several successive moves rather than demanding direct one-step access.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementThe paper-local target, balance/accessibility result, asymptotic calculation, and interpretation directly realize the shared structural explanation without using the established or nonvacuous shared endpoint.
  • checked statementThe paper's canonical target, validity, balance, and accessibility inputs ground the selected model independently of the convergence calculation.
  • checked statement
  • checked statementOriginal paper pp. 1088-1089: the canonical target, symmetric local update, pairwise balance, finite-probability accessibility, asymptotic approach to the canonical distribution, and its equilibrium interpretation exhibit one direct shared equilibrium-sampling model. The paper explicitly leaves the convergence rate open, so this theorem asserts no selected finite-run convergence.
  • checked statementThe selected update solves its canonical-target problem asymptotically.
  • checked statement
  • checked statementThe complete Metropolis route transfers every shared equilibrium-sampling claim to both the modified Monte Carlo theory and the represented accessible sampling process.
  • checked statementThe raw source contracts construct the complete shared sampling route.
  • checked statementMetropolis's source-ordered finite-periodic, canonical-target, local-update, pairwise-balance, accessibility, iteration, and interpretation inputs realize the structural endpoint. The theorem reconstructs every packaged intermediate result internally and asserts neither a mixing rate nor finite-run convergence. Primary-source anchor: pp. 1088-1089, especially the symmetric proposal, Boltzmann acceptance rule, reachability argument, pairwise population flow, and stated asymptotic approach to the canonical distribution.
  • checked statementThe selected modified update retains the source's normalized canonical target instead of forgetting the actual candidate ensemble before the population-flow argument begins.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementA single genuinely positive update probability supplies a finite path.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementA positive rigid-sphere domain and the kinetic/thermal normalization can coexist with a wrong Clausius boundary term; the partial pressure readout does not supply equations (7)-(10).
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement

Axioms and trust boundaries

  • axiom / trust boundary
  • axiom / trust boundary
  • axiom / trust boundary
  • axiom / trust boundary
  • axiom / trust boundary
  • axiom / trust boundary
  • axiom / trust boundary
  • axiom / trust boundary

Constructors, projections, and other meaning dependencies

  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • constructor
  • recursor
  • recursor
  • constructor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • constructor
  • recursor
  • constructor
  • constructor
  • constructor
  • constructor
  • recursor
  • constructor
  • recursor
  • constructor
  • constructor
  • constructor
  • 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
  • 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
  • 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

Every statement below comes only from Metropolis1953.lean, SourceMap.lean, and Coverage.lean. Multidimensional integrals, the naive close-packing argument, balance fluxes, finite-cell accessibility, convergence, contact extrapolation, and numerical runs remain named proposition-valued inputs. Their implication-valued calculation and interpretation contracts are supplied independently, then result steps apply them to the selected setups and certified predecessor outputs. The virial branch is more explicit: RigidSphereVirialFormulaReadout stores selected real values and SourceFormulaAt conjoins the physical domain with equations (7)-(10). Dependent routes recover the finite-model, canonical-target, update, sampling, rigid-sphere, virial-formula, virial-result, and finite-evidence propositions from certified predecessor outputs before using them. The accept/reject step likewise computes the proposed real-valued energy difference, keeps downhill and uphill as conditional branches, and uses uphillBoltzmannProbabilityFormulaAt to equate the uphill acceptance probability with exp(-DeltaE/kT).

01

The algorithmic proof and the rigid-sphere equation-of-state calculation branch after the update

The route graph begins with the finite periodic model and canonical target, then constructs the modified update. The naive close-packing argument is a separate calculation whose output is the impracticality assessment. One branch proves asymptotic canonical sampling from balance, accessibility, equilibration, and interpretation. Another specializes the certified update to rigid spheres and imports a virial pressure calculation. The finite numerical route consumes both certified branches. A final independent scope assessment is conjoined with the extracted sampling and numerical-evidence outputs.

Finite periodic one-phase modelclassical particles · spherical two-body forces · rapid falloff · minimum periodic image · periodic replicas · reduced surface effects
Configuration-space targetmomentum integrals separate · Boltzmann-weighted canonical average
Positive-window periodic local updatesuccessive finite-probability attempts · selected update implements proposal · DeltaE-sign branches · exp(-DeltaE/kT) uphill probability · rejected state retained
Canonical equilibrationdetailed balance + accessibility + asymptotic convergence + ensemble interpretation
Rigid-sphere pressureoverlap rejection · contact density · equations (7)-(10) retained
Finite equation-of-state evidence and scopefinite cycles · contact extrapolation · statistical error · no finite-rate or thermodynamic-limit upgrade
Figure 1. Eight routes. The declared main conclusion is the qualified conjunction of canonical sampling, finite numerical evidence, and four negative scope statements.
Epistemic ledger
TransitionStatusRetained boundary
Finite periodic cell to substanceone-phase idealizationMinimum-image reduction requires rapid potential falloff; the cell does not represent a two-phase system.
Canonical average to configuration integralcanonical reductionVelocity-independent forces are explicit.
Symmetric proposal to canonical balanceacceptance-flux calculationSymmetry alone is insufficient.
Balance to equilibrium samplingbalance plus accessibility and convergenceAccessibility separately consumes the finite periodic model and complete move protocol.
Asymptotic sampling to finite runrate unspecifiedNo finite convergence rate or selected-run convergence is established.
Contact density to pressurevirial calculation with source formulasThe imported physical calculation now retains equations (7)-(10) as selected real-valued propositions.
Finite pressure curve to equation of statecontrolled finite evidenceNo exact thermodynamic limit or finite-size control follows.
02

A periodic finite cell represents one phase and reduces the canonical target to configurations

The selected description assumes classical statistics, finitely many particles, spherical two-body interactions, and a potential that falls off rapidly with distance. Periodic replicas reduce surface effects and model a selected one-phase substance; the rapid falloff separately licenses keeping only the minimum periodic image contribution.

finite classical particle cell + spherical two-body interactions + rapidly falling potential + periodic replicas
⇒ reduced surface effects, minimum-image sufficiency, and representation of the selected one-phase substance. FinitePeriodicModelResult; journal p. 1087 (1)

Periodic replication alone does not perform that energy reduction: periodic_replica_construction_does_not_supply_minimum_image_reduction gives a direct countermodel. The checked retention theorem finite_periodic_model_retains_minimum_image_scope keeps the minimum-image conclusion in the finite model consumed by downstream routes.

For velocity-independent forces, the momentum variables separate from the canonical average. The desired observable is therefore represented by a Boltzmann-weighted configuration-space integral.

canonical equilibrium target + velocity-independent forces
⇒ momentum integrals separate and the observable average reduces to configuration space. CanonicalTargetResult; Eq. (2) (2)

Uniformly choosing configurations and applying Boltzmann weights afterward is assessed separately. Near close packing, most uniformly drawn configurations have negligible weight, making the naive scheme impractical.

03

The modified update samples locally and counts rejected states

A selected particle is displaced by a positive-width symmetric local proposal with periodic wraparound. The selected update implements that proposal, attempts particles successively, and gives each allowed local move finite probability. The acceptance calculation computes the proposed energy difference and keeps the lowering and raising cases as disjoint conditional branches; the counting rule preserves the old configuration after rejection.

DeltaE < 0: accept;
0 < DeltaE: accept with probability exp(-DeltaE/kT), with kT > 0;
rejection: retain the old configuration;   every attempted move counts as the next sample. MetropolisUpdateResult; Eqs. (3)–(4) (3)

The two energy branches are not simultaneous facts about one proposal. downhill_and_uphill_energy_branches_are_disjoint proves their incompatibility, while uphill_boltzmann_formula_gives_probability_strictly_between_zero_and_one derives the expected probability range from positive DeltaE and positive kT. The proposal protocol and the last two clauses are part of the mathematical update, not bookkeeping trivia: rejected configurations contribute the required residence time in high-probability regions.

04

Pairwise balance and configuration accessibility are independent premises

Equations (5)–(6) compare actual positive forward and reverse ensemble fluxes. For admissible configurations connected by equal proposal probabilities, the normalized equation-(2) canonical weights combine with T_rs = P_rs exp(-ΔE/kT) and T_sr = P_sr to give p_r T_rs = p_s T_sr. A separate calculation argues that repeated finite-probability local displacements, using the positive window, periodic wraparound, and successive attempts inside the certified finite periodic cell, can reach every configuration.

p_r > 0, p_s > 0, P_rs = P_sr > 0,
T_rs = P_rs exp(-DeltaE/kT), T_sr = P_sr,
⇒ p_r T_rs = p_s T_sr,
finite-periodic repeated local moves ⇒ configuration-space accessibility. PairwiseBalanceResult; journal p. 1089 (4)

canonical_equation_two_and_transition_formulas_balance_population_flux derives this equation from the actual Boltzmann factors, while established_metropolis_balance_retains_population_flux_equation and canonical_sampling_retains_population_flux_equation preserve it through the complete route. Neither balance nor accessibility contains the other. The formal countermodels show that proposal symmetry need not imply detailed balance, that discarding rejected attempts or using noncanonical populations destroys the directional equality, that detailed balance need not imply accessibility, and that a bare local proposal does not supply positive width, periodic wraparound, finite move probability, or successive particle attempts.

An additional equilibration calculation turns balance plus accessibility into approach to the canonical distribution. The ensemble interpretation then says that this limiting distribution is canonical equilibrium sampling.

canonical target + detailed balance + accessibility + asymptotic equilibration + ensemble interpretation
⇒ repeated updates produce the canonical ensemble while retaining p_r T_rs = p_s T_sr. CanonicalSamplingResult; journal p. 1089 (5)

This is an asymptotic sampling result. It supplies neither a finite rate nor physical molecular dynamics.

FiniteMetropolisRun replaces assigned bias values with an actual finite accept/reject process. Energies 0 and log(3) at kT=1 have canonical probabilities 3/4 and 1/4. The symmetric proposal q gives uphill transition q/3, downhill transition q, and a diagonal term that counts rejected attempts. actual_metropolis_branches_retain_rejected_attempts and target_is_the_actual_boltzmann_distribution check these relations.

mun(i) = pi(i) + (1-4q/3)n[mu0(i)-pi(i)],   mun(i) → pi(i). The actual finite-state kernel; positive q at most 3/4.

the_actual_sampling_distribution_converges proves the limit, while no_fixed_run_length_uniformly_removes_the_actual_bias chooses q=3/[8(n+1)] and proves bias at least 1/8 at the prescribed length n. Every transition remains positive. The 64-attempt fidelity boundary therefore fails tolerance 1/100 using the computed distribution, not independently assigned errors. This is a finite mechanism diagnostic for the report's pp. 7-8 argument, not the historical rigid-disk run.

05

Hard-core energy turns the general rule into overlap rejection

For rigid spheres, a proposed energy change is zero or infinite. The acceptance game therefore simplifies completely.

nonoverlapping rigid-sphere proposal ⇒ accept,
overlapping rigid-sphere proposal ⇒ reject. RigidSphereUpdateResult; journal p. 1089 (6)

The pressure route then applies the virial theorem and estimates the surface contact density. The imported physical step is not represented merely by the words “virial pressure”: its selected values retain the displayed Clausius, contact-force, internal-virial, and pressure equations.

sum_i X_i^(tot) dot r_i = 2 P A + sum_i X_i^(int) dot r_i = 2 E_kin,
E_kin = N m vbar^2 / 2,
Fbar_i = m vbar^2 pi d_0 nbar,
sum_i X_i^(int) dot r_i = -(N m vbar^2 / 2) pi d_0^2 nbar,
P A = E_kin (1 + pi d_0^2 nbar / 2) = N k T (1 + pi d_0^2 nbar / 2). RigidSphereVirialSourceFormulaAt; journal pp. 1089-1090, Eqs. (7)-(10) (7)

RigidSphereVirialFormulaReadout.SourceFormulaAt conjoins the positive physical domain with all four displayed equations, and virial_pressure_calculation_retains_source_formula makes that conjunction an explicit route output. Under positive particle count, thermal energy, diameter, and contact density, equation_ten_makes_pressure_area_exceed_ideal_gas_term checks the nonzero hard-sphere correction N k T < P A. The countermodel named_virial_pressure_calculation_does_not_supply_source_formulas blocks a bare calculation label from manufacturing these equations.

06

Finite MANIAC cycles provide a pressure curve with statistical, not finite-size, control

The numerical setup uses the canonical sampler and virial pressure relation, discards an initial transient, and accumulates finitely many cycles at each density. The radial distribution is extrapolated to contact and compared with free-volume and virial-expansion curves.

discarded transient + finite sampled cycles + contact extrapolation + comparison with two equation-of-state models
⇒ finite rigid-sphere pressure evidence with roughly 3% statistical error. FiniteEquationOfStateEvidence; journal p. 1091 (8)

The statistical-error assessment does not control finite-size systematics, and finite evidence does not establish the exact thermodynamic-limit equation of state. Both non-implications are formalized.

Open computational-evidence theoremselected checks + finite-size obligation

The finite cycles realize scoped support under the selected transient, statistical, and comparison checks, while finite-size systematic control remains a relevant unpassed check and the thermodynamic-limit claim is not mathematically certified.

finite_cycles_realize_open_scoped_computational_evidence_without_thermodynamic_proof · journal pp. 1091–1092
07

The qualified conclusion keeps four limitations inside the theorem statement

The final route conjoins the canonical sampling result, finite equation-of-state evidence, and a scope assessment. It does not merely append caveats in prose.

asymptotic canonical sampling + finite equation-of-state evidence,
but no established finite convergence rate, no identification with physical molecular dynamics, no exact thermodynamic-limit equation of state, and no controlled finite-size systematic. QualifiedConclusion; formal main conclusion (9)

The periodic model also retains one-phase scope: reduced surface effects do not make it a representation of phase coexistence.

08

The canonical branch realizes equilibrium sampling while the finite branch retains open evidence

The shared adapter selects the finite periodic description, finite-model regime, modified update, and canonical ensemble. Its setup requires validity, the equilibrium target, detailed balance, and accessibility. The paper's equilibration calculation and interpretation bridge then establish equilibrium sampling.

valid equilibrium target + detailed balance + accessible target space + equilibration calculation + equilibrium interpretation
⇒ established shared equilibrium sampling. shared EquilibriumSampling route (10)
Source-sensitive Metropolis explanationpp. 1088-1089 derivation preserved

The typed provenance route begins before the packaged canonical and balance results. It reconstructs the finite-periodic and canonical reductions, symmetric positive-width proposal, disjoint conditional DeltaE branches, explicit exp(-DeltaE/kT) uphill acceptance, repeated rejected configurations, reachability, pairwise population flow, asymptotic equilibration, and canonical interpretation. The common equilibrium-sampling endpoint therefore cannot turn this accept/reject derivation into Creutz's conditional heat bath.

metropolisEquilibriumSamplingDerivationObtains · metropolis_source_inputs_make_shared_equilibrium_sampling_route_applicable · symmetric_proposal_acceptance_and_population_flow_realize_source_structural_equilibrium_sampling_explanation · original report pp. 6-8 / journal pp. 1088-1089

The established shared endpoint is output-led: exact selection is conjoined directly with validity, target, balance, accessibility, convergence, and equilibrium production, rather than storing the calculation or route proof. The latter can be reconstructed from those inhabited relations. This is exhibited by metropolis_route_exhibits_nonvacuous_shared_equilibrium_sampling. Grounding is earlier and narrower: it requires the exact selected model and the valid target, balance, and accessibility setup, but neither convergence nor equilibrium production. The model is thereby grounded in the modified-Monte-Carlo framework and an accessible sampling process, and every shared claim transfers to both only after the independently completed route is combined with that grounding. The adapter remains asymptotic: it stores a distinct finite-run-convergence predicate but the 1953 route does not establish it.

A

Concept guide

Finite periodic one-phase model

A classical finite cell with periodic replicas used to reduce surface effects for one selected phase.

FinitePeriodicModelResult

Canonical configuration target

The Boltzmann-weighted configuration integral left after velocity-independent momentum variables separate.

CanonicalTargetResult

Modified Metropolis update

A positive-width periodic symmetric local proposal, implemented by the selected update and attempted successively with finite move probability, together with energy-based acceptance, rejection residence, and one sample per attempt.

MetropolisUpdateResult

Balance plus accessibility

The separate canonical flux and finite-periodic reachability inputs needed before equilibration is invoked.

PairwiseBalanceResult

Asymptotic canonical sampling

Approach to and interpretation as the canonical ensemble, without a finite convergence rate.

CanonicalSamplingResult

Rigid-sphere specialization

The zero-or-infinite energy case in which only overlaps are rejected.

RigidSphereUpdateResult

Virial contact-density pressure

The selected Clausius, contact-force, internal-virial, and pressure equations that turn a surface contact-density estimate into the pressure curve.

RigidSphereVirialSourceFormulaAt · VirialPressureResult

Finite numerical scope

Statistical evidence without finite-rate, physical-dynamics, thermodynamic-limit, or finite-size-systematic conclusions.

ScopeAssessment

Shared equilibrium-sampling model

The reusable setup, equilibration, interpretation, grounding, and theory/world transfer semantics.

equilibriumSamplingModel
B

Complete route inventory, blocked shortcuts, and provenance

The source map declares eight routes, thirty claims, and thirty sourced steps. Coverage interprets every atom, certifies every route, and proves exhaustive semantic realization. The qualified conjunction is the declared main conclusion. The finite-cell, target, naive-method, update, rigid-sphere, virial, numerical, and scope setups are independent local premises; certified predecessor outputs appear only at the result steps that use them. Implication-valued calculation and interpretation contracts are likewise independent inputs applied only at those result steps. The virial route has a separate source-formula output, so the pressure result cannot silently erase equations (7)-(10).

Complete route inventory
RouteDirect dependenciesDeclared outputProfile
Finite periodic model—Selected one-phase finite modelindependent idealization root
Canonical configuration targetFinite modelConfiguration-space canonical averagecanonical reduction
Modified importance updateCanonical targetNaive-method assessment and modified updatealgorithm construction
Canonical equilibrationModified update; inherited finite modelAsymptotic canonical samplingbalance/accessibility proof
Rigid-sphere specializationModified updateOverlap-rejection updatehard-core specialization
Virial pressureRigid spheresEquations (7)-(10) and contact-density pressure equationimported virial calculation with retained formulas
Numerical equation of stateEquilibration; virial pressureFinite pressure evidencecontrolled numerical route
ScopeNumerical equation of stateQualified conclusionconvergence and finite-size limit
Finite model · finite_periodic_model_route_is_semantically_realized
Certifies the classical finite-cell setup, periodic construction, reduced surface effects, and one-phase representation.
Canonical target · canonical_configuration_target_route_is_semantically_realized
Consumes the finite model and certifies the target, momentum separation, and configuration integral.
Modified update · modified_importance_update_route_is_semantically_realized
Consumes the target and certifies both the naive-method rejection and the complete proposal, acceptance, rejection, and counting protocol.
Equilibration · canonical_equilibration_route_is_semantically_realized
Consumes the update plus the inherited finite model and certifies balance, accessibility, convergence, interpretation, and canonical sampling.
Rigid spheres · rigid_sphere_specialization_route_is_semantically_realized
Consumes the update and certifies zero/infinite energy specialization and overlap rejection.
Virial pressure · virial_pressure_route_is_semantically_realized
Consumes the rigid update and adds the virial theorem, contact estimate, the retained equations (7)-(10), and the pressure result. virial_pressure_route_recovers_source_formula separately exposes the source-formula atom.
Finite evidence · numerical_equation_of_state_route_is_semantically_realized
Consumes equilibrium sampling and virial pressure before certifying transient removal, finite cycles, extrapolation, error assessment, comparisons, and evidence.
Scope · scope_route_is_semantically_realized
Consumes numerical evidence and retains all four negative scope statements in the main conclusion.

All thirty source-mapped claims

Claim groupSource anchorStatus
Finite setup, calculation, resultp. 1087Physical model and paper derivation
Canonical setup, reduction, targetp. 1088, Eq. (2)Physical principle and paper derivation
Naive setup/calculation/assessment; update setup/calculation/resultp. 1088, Eqs. (3)–(4)Paper derivation, interpretive assessment, and algorithm derivation
Balance, accessibility, balance result, equilibration, interpretation, samplingp. 1089, Eqs. (5)–(6)Calculation, physical reachability, interpretation, derivation
Rigid setup, calculation, resultp. 1089Physical specialization and derivation
Virial setup, calculation, source formula, resultpp. 1089-1090, Eqs. (7)-(10)Physical setup, imported calculation, exact formula retention, derivation
Numerical setup, calculation, evidencep. 1091Finite controlled approximation
Scope assessment and qualified conclusionpp. 1087–1092Open obligation

Three dynamical levels

The actual finite sampler now consumes the existing dynamics paradigm on normalized probability laws and, separately, on retained configurations. Stochastic rows give well-posed law evolution and actual retained successors. Positive branching at a configuration with positive canonical mass excludes retained-state uniqueness. actual_canonical_update_separates_distribution_and_state_levels derives this nonvacuous distinction from the kernel.

A constructed two-coordinate swap is deterministic on its larger state space and starts from the sampler's actual joint law. Its observed one-step statistics match exactly. After two swaps it returns to the initial observed state, whereas the q=3/8 Markov kernel gives joint mass 9/64 for (false,true). one_step_realization_does_not_supply_the_next_canonical_joint_law retains canonical sampling and convergence while rejecting that stronger history claim. This is not molecular dynamics, the historical random-number implementation, or a denial of other deterministic realizations of a Markov history.

Equilibrium marginals and actual adjacent-update laws

FiniteMetropolisRun now compares proposals 3/8 and 3/4 for the same canonical target (3/4,1/4). Both kernels satisfy detailed balance, have normalized consecutive-configuration laws with both marginals equal to the target, and genuinely converge. The centered occupation has variance 3/16 but adjacent-update correlations 3/32 and 0. identical_canonical_marginals_do_not_determine_the_actual_joint_law therefore separates an equilibrium distribution from its history law.

The old assigned clock and energy residual have been removed. the_actual_sampler_is_not_deterministic_on_configuration_states instead uses two positive-probability destinations to reject a single deterministic update map on the retained states alone. It does not exclude hidden momenta or bath variables, nor assert that stochastic open-system dynamics is unphysical. These update-index correlations are not calibrated molecular-time correlations or reconstructed rigid-disk data.

Representative formally blocked shortcuts

Available factConclusion not suppliedLean witness
Periodic replica constructionMinimum-image energy reduction without rapid falloffperiodic_replica_construction_does_not_supply_minimum_image_reduction
Canonical target and naive setupNaive-method impracticalitycanonical_target_and_naive_setup_do_not_supply_impracticality
Positive uphill energy and positive kTUnit acceptance probability in place of exp(-DeltaE/kT)positive_uphill_energy_does_not_supply_unit_acceptance_probability
Named virial-pressure calculationThe Clausius, force, internal-virial, and pressure source formulasnamed_virial_pressure_calculation_does_not_supply_source_formulas
Symmetric proposalDetailed balancesymmetric_proposal_does_not_supply_detailed_balance
Normalized canonical populations, symmetric proposals, and a correct downhill transitionPopulation-flux balance when rejected uphill attempts are discardeddiscarding_rejected_attempts_destroys_canonical_population_balance
Symmetric proposals and the correct acceptance-weighted uphill/downhill transitionsPopulation-flux balance with non-Boltzmann state populationscorrect_acceptance_without_canonical_population_does_not_balance_flux
Pairwise balanceConfiguration accessibilitypairwise_balance_does_not_supply_configuration_accessibility
Bare local proposalPositive width, periodic wraparound, finite move probability, and successive attemptslocal_proposal_alone_does_not_supply_metropolis_accessibility_inputs
Asymptotic convergenceA finite convergence rateasymptotic_convergence_does_not_determine_a_finite_rate
Same canonical marginals and convergent samplingUnique adjacent-update correlationcanonical_sampling_does_not_determine_adjacent_step_correlations
Valid canonical sampler, unique law evolution, and a deterministic larger-state realizationUnique evolution of the retained configuration statescanonical_branching_has_a_deterministic_larger_state_realization
Valid canonical sampler and matching deterministic one-step realizationThe same two-step Markov joint lawone_step_realization_does_not_supply_the_next_canonical_joint_law
Finite equation-of-state evidenceExact thermodynamic-limit equation of statefinite_equation_of_state_evidence_does_not_establish_thermodynamic_limit
Statistical-error assessmentControl of finite-size systematicsstatistical_error_assessment_does_not_control_finite_size_systematics
One-phase periodic representationRepresentation of a two-phase substanceone_phase_periodic_representation_does_not_cover_two_phase_systems

The countermodels are value-level witnesses. They retain positive thermal and pressure domains, Boltzmann weight and kinetic normalization, symmetric proposal rates with unequal target-weighted flows, normalized canonical populations (2/3, 1/3) with discarded rejected attempts, correct uphill acceptance with noncanonical populations (1/2, 1/2), pairwise balance with zero cross-component reach probability, local displacement with missing width/wrap/move/attempt inputs, sixty-four-cycle finite bias, the reported three-percent statistical error with a larger finite-size shift, and explicit interface and other-image contributions. The failed conclusions are precisely directional population balance, accessibility, finite rate, identification of adjacent-update correlations and deterministic retained-state evolution, thermodynamic or finite-size control, two-phase coverage, and minimum-image sufficiency.

Five source-dependency audits and six status audits

routes_have_exact_predecessor_graph fixes the eight direct route dependencies. local_setups_are_independent_hypotheses prevents fresh physical setups from masquerading as consequences of earlier route outputs. calculation_and_interpretation_contracts_are_independent_hypotheses prevents implication-valued contracts from masquerading as derived outputs. result_steps_apply_selected_inputs_and_contracts checks every application site, and dependent_routes_consume_certified_predecessor_outputs checks the inherited route chain.

sampling_result_retains_paper_derivation preserves the paper calculation behind canonical sampling, while sampling_result_depends_on_target_and_update_routes checks that the sampling claim really inherits both the canonical target and modified update. numerical_evidence_retains_controlled_status preserves the finite approximation. qualified_conclusion_retains_open_convergence_obligation preserves the unspecified finite rate, qualified_conclusion_retains_numerical_input preserves dependence on the controlled run, and qualified_conclusion_depends_on_sampling_and_numerical_evidence checks that the final conjunction inherits both substantive branches.

Machine-checked audit boundary

argument_wellFormed, argument_auditable, and routes_wellFormed certify source structure. The five dependency guards additionally certify exact predecessor routes, independent local setups, independent contracts, result-step applications, and certified predecessor-output use. every_source_claim_has_semantics covers all thirty claims, and route_semantic_realization_is_exhaustive covers all eight routes. Coverage extracts every direct inherited route output instead of accepting a fresh copy of the result as a theorem parameter, including the separate virial-source-formula output. The canonical branch separately establishes, grounds, and transfers every claim of the shared equilibrium-sampling model.

Lean-encoded bibliographic record

N. Metropolis, A. W. Rosenbluth, M. N. Rosenbluth, A. H. Teller, and E. Teller, Equation of State Calculations by Fast Computing Machines, Journal of Chemical Physics 21 (1953) 1087–1092.

TraceComplete Lean semantic identifier ledger

Reading note. The article above is the human exposition. This collapsed cross-reference records every public theorem and every constructor of the five paper-local source-map vocabularies. It introduces no additional claim; its purpose is to make semantic omissions mechanically detectable.

Primary semantic theorems (86)

equation_ten_makes_pressure_area_exceed_ideal_gas_termnamed_virial_pressure_calculation_does_not_supply_source_formulastarget_is_the_actual_boltzmann_distributiontarget_and_initial_are_normalizedactual_metropolis_branches_retain_rejected_attemptsthe_accept_reject_kernel_is_a_computed_refreshactual_sampling_kernel_is_nonvacuousthe_sampling_kernel_obeys_actual_detailed_balancea_small_positive_proposal_has_positive_transitionsactual_run_law_is_normalizedthe_actual_finite_run_retains_its_relaxation_factorthe_actual_sampling_distribution_convergesslow_proposal_has_a_positive_physical_domainno_fixed_run_length_uniformly_removes_the_actual_biascanonical_occupation_has_zero_mean_and_positive_variancethe_actual_occupation_is_a_relaxation_modethe_actual_adjacent_occupation_correlationthe_actual_canonical_sampler_has_stationary_joint_lawsthe_actual_sampler_is_not_deterministic_on_configuration_statestwo_canonical_samplers_have_different_actual_adjacent_correlationsidentical_canonical_marginals_do_not_determine_the_actual_joint_lawactual_canonical_update_separates_distribution_and_state_levelscanonical_branching_has_a_deterministic_larger_state_realizationthe_actual_second_step_has_nonzero_canonical_transition_massone_step_realization_does_not_supply_the_next_canonical_joint_lawpositive_update_step_realizes_finite_reachabilityfinite_positive_update_paths_composedownhill_and_uphill_energy_branches_are_disjointuphill_boltzmann_formula_gives_probability_strictly_between_zero_and_onefinite_periodic_cell_represents_the_selected_one_phase_systemfinite_periodic_model_retains_minimum_image_scopevelocity_independence_reduces_the_canonical_average_to_configuration_spacecanonical_target_retains_printed_equation_two_configuration_formulacanonical_equation_two_and_transition_formulas_balance_population_fluxshared_canonical_weight_is_the_printed_metropolis_boltzmann_factorfinite_periodic_canonical_target_realizes_nonvacuous_gibbs_normalizationperiodic_canonical_inputs_realize_source_gibbs_explanationshared_source_metropolis_gibbs_route_retains_original_derivationdense_configuration_weight_concentration_rejects_naive_samplingsymmetric_proposal_and_acceptance_rule_define_the_modified_updatemetropolis_update_retains_canonical_equation_twoacceptance_ratio_and_reachability_supply_balance_and_accessibilityestablished_metropolis_balance_retains_population_flux_equationestablished_metropolis_balance_equates_every_admissible_population_fluxestablished_metropolis_balance_connects_every_admissible_configurationbalance_accessibility_and_iteration_yield_canonical_samplingcanonical_sampling_retains_population_flux_equationcanonical_sampling_connects_every_admissible_configurationequilibrium_sampling_model_retains_paper_semanticspaper_calculation_realizes_shared_equilibrationpaper_interpretation_realizes_shared_equilibrium_bridgemetropolis_inputs_make_shared_equilibrium_sampling_route_applicablemetropolis_inputs_realize_structural_equilibrium_sampling_explanationmetropolis_source_inputs_make_shared_equilibrium_sampling_route_applicablemetropolis_source_inputs_realize_structural_equilibrium_sampling_explanationsymmetric_proposal_acceptance_and_population_flow_realize_source_structural_equilibrium_sampling_explanationmetropolis_route_realizes_shared_equilibrium_samplingmetropolis_route_exhibits_nonvacuous_shared_equilibrium_samplingmetropolis_route_realizes_scoped_asymptotic_sampling_solutionmetropolis_model_inputs_establish_theory_model_groundingmetropolis_route_establishes_theory_model_grounded_equilibrium_samplingmetropolis_route_transfers_every_shared_equilibrium_sampling_claimhard_core_energy_specializes_the_update_to_overlap_rejectioncontact_density_and_virial_bridge_determine_the_pressure_curvevirial_pressure_calculation_retains_source_formulafinite_cycles_supply_qualified_equation_of_state_evidencecanonical_gibbs_realization_preserves_metropolis_average_and_open_scopealgorithmic_and_numerical_conclusions_retain_paper_scopefinite_cycles_realize_open_scoped_computational_evidence_without_thermodynamic_proofnamed_canonical_target_does_not_supply_printed_equation_two_normalizationpositive_uphill_energy_does_not_supply_unit_acceptance_probabilitycanonical_target_and_naive_setup_do_not_supply_impracticalitysymmetric_proposal_does_not_supply_detailed_balancediscarding_rejected_attempts_destroys_canonical_population_balancecorrect_acceptance_without_canonical_population_does_not_balance_fluxpairwise_balance_does_not_supply_configuration_accessibilitydisconnected_two_state_positive_step_preserves_componentdisconnected_two_state_finite_positive_path_preserves_componentglobal_detailed_balance_does_not_connect_disconnected_markov_componentslocal_proposal_alone_does_not_supply_metropolis_accessibility_inputsasymptotic_convergence_does_not_determine_a_finite_ratecanonical_sampling_does_not_determine_adjacent_step_correlationsfinite_equation_of_state_evidence_does_not_establish_thermodynamic_limitstatistical_error_assessment_does_not_control_finite_size_systematicsone_phase_periodic_representation_does_not_cover_two_phase_systemsperiodic_replica_construction_does_not_supply_minimum_image_reduction

Coverage theorems (12)

every_source_claim_has_semanticsfinite_periodic_model_route_is_semantically_realizedcanonical_configuration_target_route_is_semantically_realizedmodified_importance_update_route_is_semantically_realizedcanonical_equilibration_route_is_semantically_realizedrigid_sphere_specialization_route_is_semantically_realizedvirial_pressure_route_is_semantically_realizedvirial_pressure_route_recovers_source_formulanumerical_equation_of_state_route_is_semantically_realizedscope_route_is_semantically_realizedall_routes_are_semantically_realizableroute_semantic_realization_is_exhaustive

Source-map audit theorems (15)

argument_wellFormedargument_auditableroutes_wellFormedroutes_have_exact_predecessor_graphlocal_setups_are_independent_hypothesescalculation_and_interpretation_contracts_are_independent_hypothesesresult_steps_apply_selected_inputs_and_contractsvirial_route_exposes_source_formuladependent_routes_consume_certified_predecessor_outputssampling_result_retains_paper_derivationsampling_result_depends_on_target_and_update_routesnumerical_evidence_retains_controlled_statusqualified_conclusion_retains_open_convergence_obligationqualified_conclusion_retains_numerical_inputqualified_conclusion_depends_on_sampling_and_numerical_evidence

Semantic atoms (30)

finitePeriodicSetupfinitePeriodicCalculationfinitePeriodicResultcanonicalTargetSetupcanonicalReductionCalculationcanonicalTargetResultnaiveSamplingSetupnaiveSamplingCalculationnaiveSamplingAssessmentupdateSetupacceptanceCalculationupdateResultbalanceCalculationaccessibilityCalculationbalanceResultequilibrationCalculationensembleInterpretationcanonicalSamplingResultrigidSphereSetuprigidSphereCalculationrigidSphereResultvirialSetupvirialCalculationvirialSourceFormulavirialResultnumericalSetupnumericalCalculationfiniteEquationOfStateEvidencescopeAssessmentqualifiedConclusion

Claim identifiers (30)

finiteSetupfiniteCalculationfiniteResulttargetSetuptargetCalculationtargetResultnaiveSetupnaiveCalculationnaiveAssessmentupdateSetupacceptanceCalculationupdateResultbalanceCalculationaccessibilityCalculationbalanceResultequilibrationCalculationensembleInterpretationsamplingResultrigidSetuprigidCalculationrigidResultvirialSetupvirialCalculationvirialFormulavirialResultnumericalSetupnumericalCalculationnumericalEvidencescopeAssessmentqualifiedConclusion

Step identifiers (30)

stateFiniteSetupsupplyFiniteCalculationderiveFiniteResultstateTargetSetupsupplyTargetCalculationderiveTargetResultstateNaiveSetupsupplyNaiveCalculationassessNaiveMethodstateUpdateSetupsupplyAcceptanceCalculationderiveUpdateResultsupplyBalanceCalculationsupplyAccessibilityCalculationderiveBalanceResultsupplyEquilibrationCalculationsupplyEnsembleInterpretationderiveSamplingResultstateRigidSetupsupplyRigidCalculationderiveRigidResultstateVirialSetupsupplyVirialCalculationretainVirialSourceFormuladeriveVirialResultstateNumericalSetupsupplyNumericalCalculationderiveNumericalEvidencestateScopeAssessmentretainQualifiedConclusion

Route identifiers (8)

finitePeriodicModelcanonicalConfigurationTargetmodifiedImportanceUpdatecanonicalEquilibrationrigidSphereSpecializationvirialPressurenumericalEquationOfStatescope

Route kinds (8)

finitePeriodicIdealizationcanonicalReductionalgorithmConstructionasymptoticEquilibriumProofhardCoreSpecializationimportedVirialCalculationfiniteNumericalEvidenceconvergenceAndFiniteSizeLimitation

R

Checked source-route details

This ledger is generated from the elaborated Lean route records. It lists direct predecessors, ordered inference steps, and exported claims. The independent fidelity audit checks every field; this ledger does not replace the physical semantics or certify every explanatory diagram.

finitePeriodicModel

Logical kind: finitePeriodicIdealization.

Required predecessor routes: none.

Ordered inference steps: stateFiniteSetup, supplyFiniteCalculation, deriveFiniteResult.

Exported conclusions: finiteResult.

canonicalConfigurationTarget

Logical kind: canonicalReduction.

Required predecessor routes: finitePeriodicModel.

Ordered inference steps: stateTargetSetup, supplyTargetCalculation, deriveTargetResult.

Exported conclusions: targetResult.

modifiedImportanceUpdate

Logical kind: algorithmConstruction.

Required predecessor routes: canonicalConfigurationTarget.

Ordered inference steps: stateNaiveSetup, supplyNaiveCalculation, assessNaiveMethod, stateUpdateSetup, supplyAcceptanceCalculation, deriveUpdateResult.

Exported conclusions: naiveAssessment, updateResult.

canonicalEquilibration

Logical kind: asymptoticEquilibriumProof.

Required predecessor routes: modifiedImportanceUpdate.

Ordered inference steps: supplyBalanceCalculation, supplyAccessibilityCalculation, deriveBalanceResult, supplyEquilibrationCalculation, supplyEnsembleInterpretation, deriveSamplingResult.

Exported conclusions: samplingResult.

rigidSphereSpecialization

Logical kind: hardCoreSpecialization.

Required predecessor routes: modifiedImportanceUpdate.

Ordered inference steps: stateRigidSetup, supplyRigidCalculation, deriveRigidResult.

Exported conclusions: rigidResult.

virialPressure

Logical kind: importedVirialCalculation.

Required predecessor routes: rigidSphereSpecialization.

Ordered inference steps: stateVirialSetup, supplyVirialCalculation, retainVirialSourceFormula, deriveVirialResult.

Exported conclusions: virialFormula, virialResult.

numericalEquationOfState

Logical kind: finiteNumericalEvidence.

Required predecessor routes: canonicalEquilibration, virialPressure.

Ordered inference steps: stateNumericalSetup, supplyNumericalCalculation, deriveNumericalEvidence.

Exported conclusions: numericalEvidence.

scope

Logical kind: convergenceAndFiniteSizeLimitation.

Required predecessor routes: numericalEquationOfState.

Ordered inference steps: stateScopeAssessment, retainQualifiedConclusion.

Exported conclusions: qualifiedConclusion.