Formal reconstruction · Nonequilibrium work, endpoint partition ratios, ensemble convexity, alternative dynamics, and sampling scope
A Nonequilibrium Equality for Free Energy Differences
The isolated Hamiltonian derivation, two weak-reservoir routes, path/rate invariance, quasistatic and sudden limits, mean-work and Gaussian consequences, thermostat extensions, and the rare-event obstacle to practical estimation
Definitions, structures, and assumptions
Structures, classes, and inductive alternatives
- structureThe proof-free average-work description reached after the convexity step.
- structureThe measurable realization space and its actual statistical measure. Normalization and existence of moments are separate physical/mathematical premises.
- structure
- structure
- structure
- structureThe proof-free exact-ensemble side of the shared work route. The structure retains the selected process, thermal parameter, work assignment, ensemble measure, and endpoint free-energy difference, but no identity proof.
- structureProof-free data selected for one nonequilibrium-work calculation. The model retains six selected data components and all five setup relation families used by the shared route. It stores no proof of preparation, applicability, the exponential identity, the mean-work definition, or the convexity step.
- inductiveExactly the claims established by the repeated work-identity route.
- structureProof-free provenance source for one paper-local nonequilibrium-work derivation. It stores the exact selected work model and a typed derivation token, but no proof that the token obtains and no identity or bound output.
- structureSource-sensitive structural-explanation constraint for one selected nonequilibrium-work route. It keeps the proof-free exact-ensemble source description, one typed paper derivation, and its proposition-valued realization relation, but no identity or mean-work-bound output.
- structureNeutral context containing exactly the repeated identity-and-bound route.
- structurePaper-local meanings for theory use, physical representation, and transferred claims. These relations do not supply the technical calculation.
- structureThe containing theory is distinct from the selected calculation.
- structureThe represented physical process is distinct from model and theory.
- structureThe selected process-level free-energy/mean-work inequality, kept distinct from both the exact ensemble description and the average-work description.
- 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
- structureScalar source data separating a canonical formula from its probability domain.
- structureEndpoint densities do not determine the inverse Hamiltonian trajectory.
- structure
- structureInteraction strength, reservoir size, and canonical sampling are separate.
- inductive
- structureA repeated-trial law and declared accuracy, confidence, and resource budget. The original manuscript pp. 7 and 9 distinguish these from the exact ensemble identity.
- structure
- structure
- inductiveTyped name for Jarzynski's Hamiltonian average-work derivation.
- structure
- structurePaper-local data for a family of switching experiments. Proposition-valued fields classify preparations, dynamics, regimes, and practical behavior; they do not supply proofs of any conclusion.
- inductive
- inductive
- structure
- structureValue-level readout of the trajectory-work definition in the original manuscript equation (3). The time integral is an actual Mathlib interval integral; the selected duration, constant rate, parameter path, trajectory, Hamiltonian derivative, and work value remain visible as one proposition.
- structure
- structureExact identity and average-bound outputs for one process family.
- structure
- structureThe minimal semantics of typicality. `propertyTypicalFor` can mean measure one, overwhelming measure, or another paper-specified small-exception notion; the bridge states how that notion licenses a claim about a typical state.
- structure
Definitions and domain choices
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionUse an actual discrete probability law without replacing its expectation by an unconstrained averaging function.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe finite canonical weights define a genuine probability mass function, not an independent law supplied by a physical assumption.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA reversed physical schedule reverses the order of control changes and heat updates. Keeping the same combined quench-then-update convention is not enough.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThis finite specialization has time-even states. Momentum and magnetic-field reversal in Crooks's general source model are not replaced by this operation.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe imported convexity calculation. The exact identity is an input to this bridge, not a hidden structure field or a consequence of the setup alone.
- definition
- definition
- definitionThe paper-local Hamiltonian, reservoir, or forward-reverse calculation whose exact output is the shared exponential-work identity.
- definition
- definition
- definition
- definitionThe complete inhabited nonequilibrium-work route, stated directly at one model rather than through implication-valued calculation contracts. The proposition retains the positive-temperature finite-classical setup, the exact exponential-work identity, the selected mean-work definition, and the derived mean-work bound at the same process. It intentionally does not assert how a paper obtained the identity or convexity step; Jarzynski's Hamiltonian transport and Crooks's forward/reverse path calculation remain paper-local.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe selected average-work data, without a bound proof.
- definitionThe selected exact-ensemble work data, without an identity proof.
- definitionExact selected work model and typed paper-local derivation.
- definitionSource-sensitive structural constraint selected by this work model.
- definitionThe exact process and values compared by the selected mean-work bound.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA finite but mass-two measure can mimic the scalar work identity by changing the assigned free energy. It is not a probability ensemble.
- definitionOne actual exact-ensemble/average-work pair, its derivation bridge, direct source support, and the resulting average-work inequality.
- definitionSource-sensitive reduction from one work derivation to the mean bound.
- definitionSource-sensitive structural explanation of one selected work route.
- definitionOrdinary structural explanation of one selected work-identity route.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe selected model is exactly the context-induced model at the process owned by that context. This equality retains all six data components and all five route-used proposition families.
- definitionThe exactly selected process model together with the positive-temperature, finite-classical, canonically prepared work setup, before either calculation output is used.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe unique process model selected for one paper-local deduction.
- definition
- definition
- definition
- definitionSource-sensitive structural semantics for one selected nonequilibrium-work route. The source constraint adds a typed paper-local derivation and raw realization relation without storing an established endpoint, ordinary explanation, or derivational-reduction result.
- definitionOrdinary structural semantics for one selected nonequilibrium-work route. Satisfaction retains the proof-free exact-ensemble description and complete raw bound route; the explained phenomenon is the actual scoped free-energy/mean-work bound at the same process. This is distinct from the derivational-reduction relation below.
- definitionTheory use and physical representation identify the selected process model; they do not presuppose either the exponential identity or its convexity consequence.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- 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
- 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
- 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
- definitionOne realization performs work below `Delta F = 0`, while the other performs work above it. Their exponential average nevertheless satisfies Jarzynski's identity exactly.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA normalized two-point average with weights `1/3` and `2/3`.
- 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
- definitionEquation (6): rewrite the ensemble average as a final-time phase integral.
- definitionJensen's exponential inequality specialized to the work ensemble.
- definitionThe original p. 9 convergence claim is a mathematical input about actual repeated-trial laws. Independence with a finite exponential second moment is one sufficient realization, not an extra assumption on every exact identity.
- definition
- definitionThe final Boltzmann integral is the endpoint partition function.
- definition
- definition
- definition
- definitionProtocols with the same complete endpoint Hamiltonians integrate the corresponding endpoint Boltzmann factors over the same full phase space.
- definition
- definition
- definitionThe reservoir argument has its own full phase volume and trajectory map. It is not identified with reduced-system volume preservation.
- definition
- definitionFull-space Liouville transport uses the selected combined trajectory.
- definition
- definitionThe combined endpoint partition ratio depends only on the full initial and final system-reservoir Hamiltonians and the temperature, not on the path or switching time between them.
- definition
- definition
- definition
- definitionFull-space work-energy balance uses that same combined trajectory.
- definitionExact mathematical output of truncating the work cumulant expansion for a Gaussian distribution. The physical identification with `Delta F` remains a separate use of Jarzynski's equality.
- definitionThe selected experiment is the pushforward of its normalized initial phase density by the same invertible, phase-volume-preserving evolution.
- definitionEvery protocol in the weak-reservoir regime has a quasistatic comparison at the same complete endpoint setup whose exponential work average is already the endpoint free-energy exponential. This is the source-ordered bridge between the quasistatic calculation and the later all-path law.
- definitionEvery admissible finite-time switching protocol has a quasistatic comparison that remains in the weak-reservoir regime and has the same system endpoints and complete system-reservoir endpoint Hamiltonians. The comparison work is the thermodynamic-integration value, and the established equilibrium identity identifies that value with the endpoint free-energy difference.
- definitionEquation (2a), stated for one switching protocol.
- definitionRaw paper-local inputs constituting Jarzynski's Hamiltonian derivation of the exponential-work identity and average-work bound. The token stores neither a shared applicable route nor an established or nonvacuous endpoint.
- definitionEquation (2b), the logarithmic free-energy extraction form.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionLiouville transport is evaluated along the selected deterministic trajectory from a final phase point back to its initial point, not at one unchanged phase-space coordinate.
- definition
- definitionThe ordinary mean is a finite expectation of trajectory work.
- definitionExact output of the paper's discrete Metropolis extension.
- definitionThe repeated, canonically prepared work experiment has a normalized realization measure and a finite exponential work moment.
- definitionExact output of the Nosé-Hoover extended-phase-space calculation in the paper. No weak-coupling or chaos premise occurs in this implication.
- definition
- definitionExtensionality of the actual phase-space integral, derived below.
- definitionScalar-linearity used in equation (8), derived for the actual integral below.
- definitionThe pointwise density-work cancellation immediately preceding equation (8).
- definitionWork is the same thermodynamic-integration value on every slow run.
- definitionThe practical warning needs a quantitative sampling-risk assessment for the selected budget. It does not deny all finite counts or asymptotic consistency.
- definition
- definitionCalibrate the paper data to the system-controlled work of one full history. The decomposition and Hamilton equations remain separate physical obligations.
- definitionData calibration to one actual Hamiltonian history. No energy-balance conclusion or proof of the work identity is stored in this proposition.
- definitionThe protocols have the same system configurations and the same complete system-reservoir endpoint Hamiltonians. This makes the fixed reservoir and interaction content of Jarzynski's comparison explicit.
- definition
- definitionTwo protocols use the same full system-reservoir Hamiltonians at both endpoints. The temperature is already fixed by the ambient framework.
- definitionEquation (3) is selected for the same protocol and work observable used by the switching framework. The representation bridge prevents an unrelated scalar integral from being relabeled as the physical trajectory work.
- definitionIn the sudden limit, work is the endpoint Hamiltonian difference.
- definitionThe paper's `Z₁ / Z₀` interpretation of the system partition ratio.
- definitionThe system partition-function ratio encodes the endpoint free energy.
- definitionThe weak-coupling equilibrium input used to replace the combined system-reservoir partition ratio by the system ratio.
- definition
- definitionThe paper's central result, scoped to its declared physical regime.
- definitionWork-energy balance uses the same selected final-to-initial trajectory.
- definitionThe source's sigma squared is the variance of the same actual work law.
- 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 full control-family decomposition with calibrated system and combined endpoint energies. Bath and interaction energies have no control argument.
- definition
- definitionThe shared technical context retains the work, averaging, free-energy, and mean-work assignments together with the route-used setup predicates, while leaving Jarzynski's Hamiltonian phase-space derivation paper-local.
- definition
- definition
- definition
- definition
- definitionThe paper's work observable is not an opaque label: it is the selected equation-(3) trajectory 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
- definitionOriginal manuscript p. 3, equation (3), together with the preceding constant switching-rate convention lambda(t) = t / t_s on 0 ≤ t ≤ t_s.
- definitionThe printed switching interval has positive duration.
- definitionThe positive-duration work-definition domain used by the countermodel.
- definitionTimes for which the source specifies the finite switching protocol.
- 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 bridge principle derives a macro behavior from any realizing microdescription that supports it.
- definition
- definition
- definition
- definition
- definition
- definitionTypicality is nonvacuous only when the selected measure has a typical state.
- definition
- 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
- 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
Source mappings and interpretation choices
- inductive
- definition
- instance
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- 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
- 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
- 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
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- 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
- 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
- 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
- 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
- definition
- constructor
- definition
- checked statement
- 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
- 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
- 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
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- definition
- definition
- checked statement
- definition
- definition
- definition
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- definition
- inductive
- definition
- instance
- definition
- definition
- definition
- definition
- 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
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- inductive
- definition
- instance
- 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
- definition
- definition
- definition
- checked statement
- recursor
- definition
- definition
- constructor
- definition
- checked statement
- structure
- definition
- instance
- checked statement
- checked statementEvery route certificate is built from the paper's raw physical, mathematical, approximation, and interpretive hypotheses in source dependency order.
- definition
- definition
- definition
- definition
- definition
- checked statementThe paper's later direct weak-coupling reduction is a second route to the central law, distinct from the quasistatic-transfer derivation above.
- checked statementThe ensemble-consequence route derives eq. (1), nonnegative dissipated work, and the conditional Gaussian fluctuation-dissipation relation.
- checked statement
- checked statementThe p. 9 estimator limit uses the numerical-thermostat identity and a separate repeated-sampling convergence input, with no rare-event premise.
- definition
- checked statementThe combined system-reservoir canonical ensemble is normalized.
- checked statementEvery full-reservoir canonical density has a positive physical `Y0`.
- checked statementEquation (9)'s exact full-reservoir work average is positive at each protocol.
- checked statementEvery source-resolved full-space ratio is an actual positive `Y1/Y0`.
- checked statementThe exact full-reservoir calculation realizes equation (9).
- checked statementDerive the full-space route's work and averaging inputs from coupled Hamiltonian histories and actual Liouville transport.
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- definition
- checked statementThe source canonical density integrates to one once its integral rules apply.
- checked statementThe isolated canonical-density atom retains a positive physical partition.
- checked statementThe isolated Hamiltonian route realizes equations (6)-(8) and eq. (2).
- checked statementEquation (8)'s certified work average is positive for the selected ensemble.
- checked statementThe isolated source route now derives both its work definition and work-energy balance from one actual Hamiltonian history.
- checked statementThe source route is constructed using actual pushforward transport; equation (6) and integral congruence/scaling are derived, not separately supplied.
- definition
- constructor
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- checked statement
- definition
- checked statementThe weak-reservoir central-law route consumes the exact equation-(9) route, then adds endpoint comparison and quasistatic weak-coupling transfer.
- definition
- definition
- checked statementThe practical-scope route separates exact validity from reliable finite sampling when rare low-work realizations dominate the exponential average.
- definition
- checked statementThe slow-switching route recovers thermodynamic integration, eq. (4).
- recursor
- definition
- checked statementThe raw constructor covers every Jarzynski route identifier.
- definition
- definition
- checked statementThe instantaneous-switching route recovers eq. (5).
- checked statementThe source's system ratio is an actual positive `Z1/Z0`.
- checked statementThe Nosé-Hoover and Metropolis calculations remain separate extensions.
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- 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
- 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
- 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
- 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
- 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
- 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
- checked statement
- checked statement
- definition
- definition
- checked statement
- definition
- checked statement
- definition
- checked statement
- definition
- checked statement
- 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
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- definition
- checked statement
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- checked statement
- definition
- definition
- checked statement
- definition
- definition
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- checked statement
- definition
- 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 statementCanonical density and Liouville transport alone do not produce the paper's pointwise cancellation when trajectory work fails to equal the energy change.
- checked statement
- checked statement
- checked statementEven an exact equation-(9) identity with an endpoint-invariant full partition ratio does not identify that common value with the free-energy exponential. The quasistatic comparison equality is a substantive bridge, not bookkeeping.
- checked statementJarzynski's identity and Jensen's inequality for the actual work ensemble do not constrain a separate number merely called `meanWork`. Equation (1) therefore requires the explicit identification of that number with the ensemble average of trajectory work.
- 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 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 final ensemble is the actual pushforward. Phase-volume conservation turns its density into the initial density evaluated at the inverse trajectory.
- 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 full-space result precedes any weak-coupling reduction to the reduced system partition function or any quasistatic comparison.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementExact combined partition ratio from system-controlled work and actual full Hamilton equations. Neither a large reservoir nor weak coupling is assumed.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementEquation (3) and work-energy balance come from the same actual history; the existing Liouville and partition deductions then give the work identity.
- checked statementNo separately assigned averaging equation or integral axioms are needed: the finite-time Liouville realization supplies equation (6).
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe source's initial system phase density is a normalized probability density.
- checked statementA canonical system density is strictly positive at every finite-energy state.
- 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 statementCanonical preparation on the combined phase space is also normalized.
- checked statementThe full system-reservoir canonical density is strictly positive.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe full equation-(9) work average is positive before free-energy transfer.
- checked statementEquation (9) transports the already-established quasistatic comparison average to every protocol with the same complete endpoint Hamiltonians.
- checked statement
- checked statement
- checked statementThe source's exact system-reservoir ratio `Y1/Y0` is positive.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementFor positive inverse temperature, the exponential identity in equation (2a) really yields the equivalent logarithmic equation (2b).
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementJarzynski's raw Hamiltonian route structurally explains the selected free-energy/mean-work bound without consuming an established work result or derivational-reduction endpoint.
- checked statement
- checked statementJarzynski's original author TeX states the exponential-work identity in iden1.tex lines 78-90, derives it from isolated Hamiltonian transport in lines 201-269, and obtains the mean-work inequality by exponential convexity in lines 370-379. The completed paper-local route therefore exhibits one direct shared process where the positive-temperature setup, exact identity, mean-work definition, and bound all hold together.
- checked statementJarzynski's canonical-density, Liouville-transport, work-energy, phase-space, partition-ratio, mean-definition, and Jensen route directly realizes the shared derivational reduction from the exact ensemble identity to the average-work bound. Primary-source anchors: original author TeX lines 201-269 for the Hamiltonian identity calculation and lines 370-379 for the convexity inference.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementJarzynski's typed Hamiltonian derivation reconstructs the raw shared bound route without storing an established endpoint or ordinary explanation.
- checked statementJarzynski's raw Hamiltonian inputs realize a source-sensitive average-work derivational reduction without identifying this calculation with Crooks's forward/reverse path-weight route. Primary-source anchors: original author TeX lines 201-269 for canonical density, Liouville transport, work-energy change, and the partition ratio; lines 370-379 for the convexity inference.
- checked statementJarzynski's typed Hamiltonian derivation realizes the source-sensitive work explanation while remaining distinct from Crooks's forward/reverse route.
- 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 quasistatic comparison is established before the all-path law: slow work is constant on the comparison ensemble, and thermodynamic integration fixes that constant to the endpoint free-energy difference.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe isolated equation-(8) work average cannot collapse to zero.
- checked statementThe system's source ratio `Z1/Z0` is genuinely positive.
- 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 constant-rate convention in equation (3) really connects the selected time interval to the endpoint parameter values.
- checked statement
- checked statement
- checked statement
- checked statementA named trajectory-work output can hold at a positive duration while the printed equation (3) fails. The label cannot replace the value-level formula.
- 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
Axioms and trust boundaries
- 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
- constructor
- constructor
- recursor
- 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
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- recursor
- constructor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- 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
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
This edition reads Jarzynski1997.lean, SourceMap.lean, Coverage.lean, the fidelity certificate, and their imported shared formal definitions. The finite discrete-work specialization computes its canonical weights, path law, and work averages. The general Hamiltonian, reservoir, thermostat, and Gaussian routes retain their explicitly declared physical and mathematical inputs. No later quantum or strong-coupling equality is imported. The IID sampling diagnostic separately derives sufficient moment-based convergence.
Three independent roots and seven dependent routes preserve distinct physical mechanisms
The isolated Hamiltonian route, exact full-reservoir partition-ratio route, and thermostat-extension route begin independently. The physical-reservoir central-law route consumes the exact ratio and endpoint invariance; the direct weak-coupling reduction also consumes only that exact route. The quasistatic limit, sudden limit, ensemble consequences, and practical sampling routes then depend on the central-law certificate. The estimator-consistency route depends separately on the thermostat extension. The source map names the central weak-reservoir law as its main conclusion but does not manufacture an all-routes theorem.
| Transition | Status | Retained boundary |
|---|---|---|
| Isolated Hamiltonian transport | actual measure derivation + explicit Liouville realization | Initial density and energy are evaluated at the same inverse trajectory point; the final ensemble is the actual pushforward. Probability normalization alone does not imply phase-volume preservation. |
| Full reservoir ratio and endpoint invariance | exact full-space derivation | The full-space correspondence is retained; same system endpoints alone are insufficient because complete endpoint Hamiltonians must match. |
| Central weak-reservoir law | large-reservoir sampling + controlled weak-coupling regime + quasistatic reference | Weak coupling alone does not supply the large-reservoir scope; the direct partition-reduction proof is separate. |
| Quasistatic and sudden identities | controlled limiting regimes | The sudden route explicitly excludes the hard-wall exception. |
| Mean and Gaussian consequences | imported convexity/cumulants + deferred Gaussian calculation | The mean and variance labels must equal the actual ensemble moments; the Gaussian formula also requires Jarzynski’s equality. |
| Nosé–Hoover and Metropolis | deferred alternative-dynamics calculations | Neither route uses the weak-coupling reduction step. |
| Finite sampling | author expectation + budget-specific risk | Exact ensemble validity does not guarantee practical estimator reliability. |
The equality connects an exponential work average to an endpoint free-energy difference
For protocol Λ, let A and B be its initial and final configurations, W[Λ,ω] the work in realization ω, β the inverse-temperature parameter, and the overbar or angle brackets the protocol’s ensemble average. The primary Lean file defines
⟨e−βW⟩Λ = e−βΔFΛ. Jarzynski equality for one protocol; route-specific hypotheses determine when it holds (1)
At the source-mapped positive inverse temperature, the same equality permits direct free-energy extraction:
Lean takes the logarithm of the exact ensemble identity and solves for the endpoint free-energy difference under the source-retained positive β premise.
jarzynski_equality_and_positive_beta_yield_log_form · free_energy_from_exponential_work_average · original manuscript pp. 2–3Canonical density, Liouville transport, and work–energy balance cancel pointwise
The isolated route fixes a finite classical switching setup, retains positive β, defines trajectory work by the value-level generalized-force integral, prepares the initial phase space canonically, and evolves it under the time-dependent Hamiltonian. For each final phase point z, it selects the initial point z0(z,t) on the unique trajectory through z. Work equals the final Hamiltonian at z minus the initial Hamiltonian at that selected z0, while Liouville transport carries the density along the same correspondence.
W[Λ,ω] = ∫0ts dt λ̇ (∂Hλ/∂λ)(zω(t)). selected equation (3): the readout is tied to the same protocol, trajectory, and work map used downstream (3a)
f1(z)e−βW(z) = Z0−1e−βH1(z). pointwise Boltzmann cancellation along one selected final-to-initial trajectory correspondence (3b)
Congruence and scalar-linearity of the actual Mathlib phase-space integral turn the pointwise identity into ⟨e−βW⟩ = Z1/Z0. The endpoint partition evaluations and equilibrium relation Z1/Z0 = e−βΔF remain explicit inputs. Equation (6) is derived from the actual pushforward, normalized initial density, and phase-volume-preserving measurable equivalence.
Equation (3) is now an actual interval integral with an explicit integrability condition. In the finite-dimensional history constructor, the same Hamiltonian differential supplies both control power and the velocity (dH/dp,-dH/dq). Hamilton equations and the constant-rate clock give the actual energy derivative; integration and the selected inverse trajectory endpoints derive work-energy balance. The paper readout, work, endpoint Hamiltonians, and inverse map are calibrated to this history. The final ensemble is the actual pushforward of the normalized initial density. Liouville preservation then supplies equation (6), and the cancellation and partition inputs give the exponential identity and its positive-beta logarithmic form. General existence and phase-volume preservation remain separate obligations.
hamilton_equations_give_actual_energy_derivative · actual_trajectory_work_equals_endpoint_energy_change · actual_history_supplies_equation_three · actual_hamiltonian_history_yields_jarzynski · isolated_route_from_actual_hamiltonian_history · actual_liouville_transport_derives_equation_six · jarzynski_equality_and_positive_beta_yield_log_form · original manuscript pp. 2–5Continuous independent validation
On position-momentum space with Lebesgue phase volume, a separate Lean client uses H(q,p) = (q2 + p2)/2, the actual canonical density exp(-H)/(2 pi), and the free-flight shear (q,p) to (q+p,p). Its endpoint work uses the same inverse trajectory. The public transport API derives the exponential-work average 1 and a finite exponential moment, while work takes both signs and the final density is not canonical for H. This validates the finite-time transport mechanism, not a complete time-dependent equation-(3) switching protocol. A separate unequal-volume example preserves normalized probability under an invertible map but violates Liouville preservation. These are constructed tests, not examples attributed to the original paper.
Complete constructed switching experiment
A second independent client uses Hlambda = (1+lambda)(q2+p2)/2, duration 4 pi/3, and actual rotation angle t+t2/(2 duration). Lean checks its Hamiltonian differential, equations of motion, and integrable work. The orbit has a nontrivial intermediate phase point and returns to its initial point at the selected final time. Canonical Gaussian preparation and actual endpoint partition integrals give Z0 = 2 pi, Z1 = pi. The history API derives W = (q2+p2)/2; the transport API derives its finite exponential average 1/2 and free-energy change log 2 at unit inverse temperature. The actual final probability law differs from final equilibrium: exp(-W) has averages 1/2 and 2/3, respectively. This is a checked difference of measures through an observable, not only of density representatives at one point. The example is constructed validation, not an attribution to the original article.
The full reservoir derivation separates endpoint invariance from two routes to the weak-coupling law
For the combined system–reservoir Hamiltonian G, the same selected final-to-initial trajectory correspondence and cancellation give a full partition ratio Y1/Y0. Initial and final full Boltzmann integrals, their endpoint congruence, and the ratio definition prove that this ratio depends only on the complete endpoint Hamiltonians and temperature.
SystemReservoirCoupling represents Gλ(z,z′) = Hλ(z) + Hbath(z′) + Hint(z,z′) for the entire control family. Bath and interaction energies have no control argument. From the actual full Hamiltonian differential, Lean derives ∂λG = ∂λH and hence equality of the system and full control powers on the same trajectory. Integrating Hamilton's equations gives W = ΔG = ΔHsystem + ΔHbath + ΔHint. The embedding and total-work predicates are now explicit energy equations, not free labels. This work derivation feeds the exact full partition-ratio theorem before any weak-coupling or large-reservoir premise.
actual_system_control_derivative · controlled_work_resolves_all_three_energy_changes · actual_coupled_history_yields_full_partition_ratio · full_reservoir_route_from_actual_coupled_histories · original author TeX before equation (9)An independent constructed coupled-oscillator test checks a canonical subsystem split and a quarter-period Hamiltonian trajectory. Its work is 1, system energy change 2, bath change 1, and interaction change −2. Thus work is not reduced-system energy change, and omitting interaction energy breaks the balance. Its full canonical density is now normalized by actual Gaussian integrals, and the same quarter-turn is proved volume-preserving. The computed partitions are Y0 = (2π)² and Y1 = e−1(2π)². The public Hamiltonian-work and Liouville APIs derive the finite actual work average e−1. This finite interacting example is not a large thermal reservoir. A separate inhabited countermodel preserves the initial-energy match and actual full derivatives while rejecting the full control-family decomposition. Neither example is attributed to the original paper.
The subsystem law is the actual marginal of the full canonical probability measure. A separately normalized canonical reference uses the bare system Hamiltonian. The bounded positive observable e−qs²/2 has squared averages 1/2 and 2/3 under these two measures, proving that they are unequal. In this additive-control example the full and bare partition ratios nevertheless coincide, so scalar ratio agreement alone does not establish bare-system canonical sampling. This checks the logical distinction between the exact full-space step and the later reduced-equilibrium assumptions; it does not derive a weak-coupling or reservoir-size limit.
Constructed validation: independent coupled-oscillator client · source distinction: original author TeX before equation (9)→ ⟨e−βW⟩Λ = Y1,Λ/Y0,Λ,
same full initial and final Hamiltonians → Y1,Λ/Y0,Λ is protocol invariant. system endpoints and full Hamiltonian endpoints are separate requirements (4)
This full-ratio identity supports three distinct deductions:
| Use | Additional bridge | Conclusion |
|---|---|---|
| Path/rate comparison | Same system configurations and same full endpoint Hamiltonians | Equal exponential work averages, independently of the central equality. |
| Central physical-reservoir route | For every protocol with a large-enough reservoir and sufficiently weak interaction, first establish a quasistatic comparison that stays in that regime, has the same full endpoint setup, and has work equal to the thermodynamic-integration value | The comparison average equals e−βΔF; only then does endpoint invariance transport that equality to the finite-time protocol. |
| Direct reduction route | Sufficiently weak coupling gives Y1/Y0 = Z1/Z0, and the system ratio encodes ΔF | The weak-reservoir law without a quasistatic-reference dependency. |
or
full ratio + weak-coupling partition reduction + endpoint free-energy relation → direct weak-coupling Jarzynski law. two proof routes to the same equality; only the first depends on the quasistatic reference (5)
The formalization retains the full-space selected initial point before separately proving full-ratio endpoint invariance and path/rate independence. It next derives the quasistatic comparison equality from constant slow work and thermodynamic integration, then feeds that equality into the all-path central law; the central law is not allowed to justify its own comparison premise. weak_reservoir_conditions_retain_large_reservoir_sampling_scope exposes the large-reservoir premise instead of hiding it inside weak coupling.
full_liouville_transport_retains_selected_initial_point_on_unique_trajectory · endpoint_boltzmann_integrals_yield_partition_ratio_invariance · full_partition_ratio_identity_yields_path_rate_independence · quasistatic_references_yield_comparison_equality · full_partition_ratio_and_quasistatic_comparison_yield_jarzynski_law · weakly_coupled_reservoir_law_from_full_partition_ratio · original manuscript pp. 5–6The slow and sudden limits recover two familiar equilibrium identities
In the quasistatic regime, every realization has the same work, equal to the thermodynamic-integration value. Ensemble congruence and averaging of constants reduce the exponential average to one exponential; injectivity then identifies that value with ΔF.
→ ΔF = WTI. thermodynamic integration, equation (4) (6)
In the instantaneous regime, work is the sudden endpoint Hamiltonian difference. With the moving-perfectly-hard-wall exception explicitly excluded, substitution into the logarithmic formula gives free-energy perturbation.
→ ΔF = −β−1 log ⟨e−βΔH⟩. free-energy perturbation identity, equation (5) (7)
The two dependent routes specialize an already established equality; neither limit is used to prove the other.
quasistatic_limit_recovers_thermodynamic_integration · sudden_limit_recovers_free_energy_perturbation · original manuscript pp. 3–4Convexity bounds the ensemble mean, not every realization
The mean-work result requires an explicit definition equating the stored mean work with the ensemble average of trajectory work. Exponential Jensen convexity then combines with Jarzynski’s equality at β > 0.
→ ΔF ≤ ⟨W⟩, Wdiss ≡ ⟨W⟩ − ΔF ≥ 0. ensemble statement; no pathwise lower bound follows (8)
If the work distribution is Gaussian and the cumulant expansion is valid, a deferred calculation expresses the exponential average through its first two cumulants. Only after equating that output to Jarzynski’s free-energy exponential does the fluctuation–dissipation relation follow.
plus Jarzynski equality → Wdiss = βσ²/2. conditional Gaussian relation, equation (12) (9)
Lean checks the convexity transfer, nonnegative dissipated work, and the algebra identifying the Gaussian cumulant expression with ΔF.
jarzynski_and_jensen_imply_mean_work_bound · mean_work_bound_gives_nonnegative_dissipated_work · jarzynski_and_gaussian_cumulants_give_fluctuation_dissipation_relation · original manuscript pp. 6–7Nosé–Hoover and Metropolis dynamics provide independent equality routes
The Nosé–Hoover route supplies the extended dynamics, canonical initial density, density-evolution equation, accumulated-work equation, and a deferred phase-space calculation. The Metropolis route instead supplies discrete dynamics, canonical preparation, a discrete work sum, and its own deferred calculation.
Metropolis dynamics + canonical preparation + discrete work sum + Metropolis calculation → Jarzynski equality. two independent alternative-dynamics outputs (10)
The source-map audit proves that neither equality depends on the weak-coupling partition-reduction step.
nose_hoover_switching_yields_jarzynski_without_weak_coupling · metropolis_switching_yields_jarzynski · thermostat_equalities_are_independent_of_weak_coupling_step · original manuscript pp. 8–9Finite discrete-work specialization
A finite realization now derives the discrete calculation from energy functions and actual transition matrices. It computes the partition sums and trajectory law before evaluating work. Gibbs-preserving updates suffice; this does not classify every such update as the Metropolis algorithm.
pi_i(x) = exp(-beta E_i(x)) / Z_i.
P_F(h) = pi_0(x_0) product_i K_i(x_i,x_{i+1}).
K_i(x,y) >= 0; sum_y K_i(x,y) = 1.
sum_x pi_{i+1}(x) K_i(x,y) = pi_{i+1}(y).
finite nonempty state space; any finite protocol length
Q(h) = sum_i [E_{i+1}(x_{i+1}) - E_{i+1}(x_i)].
W(h) + Q(h) = E_N(x_N) - E_0(x_0).
controlled work and stochastic heat are computed from the same history
F_i = -log(Z_i)/beta; DeltaF = F_N - F_0; beta > 0.
DeltaF <= sum_h P_F(h) W(h).
No assumption of actual final equilibration or detailed balance is needed for this forward identity.
finite Gibbs-preserving stochastic updates, not a general reservoir derivation
The finite path PMF supplies genuine normalization and integrability. Canonical reweighting composes over every step, and the shared Jensen theorem gives the mean bound. A pure heat update can change the internal energy with zero controlled work; a pure quench can satisfy the identity without ending in equilibrium.
finite_canonical_updates_derive_the_paper_work_identity_and_mean_bound · finite_work_readouts_define_a_genuine_ensemble_mean · actual_finite_updates_supply_the_discrete_metropolis_calculation · original author TeX, discrete Metropolis paragraph, lines 552-562
Finite-sample difficulty is relative to accuracy, confidence, and budget
The practical route retains the exact weak-reservoir equality as one output. A separate assessment concerns the actual sampling law, estimator, relative tolerance, failure allowance, and maximum affordable count. The author's warning about rare low-work events does not establish failure at every finite count.
The independent work-sampling review also tests the tempting converse: small ordinary work variance need not make the exponential estimator reliable within a fixed budget. A canonically prepared two-state quench has variance below 1/1000 in thermal units and satisfies the exact identity, while an event of probability one millionth dominates its exponential mean. The product sampling law, actual error events, and logarithmic free-energy readout are explicit. These numerical values are diagnostic, not results attributed to the paper, and do not imply impossibility for all estimators or all finite counts. Human semantic review remains pending.
q_N = P(|Y_N-mu| > epsilon*mu).
Reliable(N): N > 0 and q_N <= delta.
0 < epsilon < 1; 0 < delta < 1; affordable budget B > 0.
q_N > delta for every 1 <= N <= B excludes only affordable reliable counts. The budget-risk conclusion does not require the exact work identity. (11)
Rare-event dominance concerns the same work law: a measurable event with positive but small probability lies below the mean by a specified multiple of the actual standard deviation and supplies a specified majority of the exponential mean. Large work variance does not itself establish this tail geometry. The large-fluctuation-to-tail bridge and the budget-risk assessment preserve their author-expectation status.
Independent repetitions give a missed-event probability equal to the complement probability to the Nth power. When every missed-event sample falls outside the accuracy interval, that is an actual lower bound on estimator failure, not a prohibition of every finite experiment.
an_independent_missed_tail_bound_controls_every_affordable_count · rare_event_risk_bounds_obstruct_only_sampling_within_the_declared_budget · original manuscript p. 7Consistency and selected-data accuracy are different claims
The original computational discussion on p. 9 proposes averaging exponential work, then taking the negative logarithm. A separate route combines the Metropolis equality with an explicit convergence input. It does not depend on the practical obstruction or weak-coupling reduction.
IID repetitions + E[exp(-2 beta W)] < infinity give Var(Y_N) = Var(exp(-beta W))/N.
P(|Y_N-mu| > a) <= Var(exp(-beta W))/(N*a^2), for N > 0 and a > 0.
Y_N converges in probability to mu; mu = exp(-beta DeltaF) > 0.
Continuity of the logarithm gives convergence in probability of Fhat_N to DeltaF. Finite exponential second moment is a sufficient verified realization, not a necessary condition stated by the author.
Finite work variance is not finite exponential second moment. Canonical single-trial marginals do not establish independence of repetitions. Budget-limited failure can coexist with eventual convergence. Statistical confidence does not make every positive-probability dataset accurate.
DeltaF-log(1+epsilon)/beta <= Fhat_N <= DeltaF-log(1-epsilon)/beta. The shared typicality bridge requires membership of the selected sample in the accuracy event.
The Gaussian variance label is identified with the actual ensemble variance using normalization and square integrability. Gaussianity and the cumulant calculation remain separate assumptions; neither follows from a small variance or a reliable experiment.
finite_second_moment_and_independent_repetition_supply_consistency · statistical_reliability_transfers_the_error_bound_only_to_a_selected_sample · gaussian_fluctuation_dissipation_uses_the_actual_work_variance · original manuscript pp. 7, 9; reconstructed quantitative scope
Actual Hamiltonian quenches test stronger conclusions
These are constructed Lean diagnostic models, not examples attributed to Jarzynski. Probabilities, work, variances, and estimators are calculated from Hamiltonians using the shared canonical library.
H_1(false)=0; H_1(true)=log(99)-100.
P(false)=99/100; P(true)=1/100; W(false)=0; W(true)=-100.
E[W]=-1; Var(W)=99; mu=(99+exp(100))/100.
B=10; epsilon=1/2; delta=1/100.
P(no rare draw in N independent trials)=(99/100)^N. The exact identity, rare-tail dominance, finite-budget obstruction, and eventual consistency hold together.
A 100-trial dataset with one rare draw returns the exact free energy, yet the 100-trial experiment is not reliable at the declared confidence. At a reliable finite count the all-common dataset still has positive probability and fails the test. Repeating one canonical draw forever preserves every marginal but prevents consistency. Raising the rare energy level retains work variance 99 while excluding any tail more than one standard deviation below the mean.
An independent three-state consumer uses different energies and probabilities. It computes a one-trial failure mass of 1/5, passes a selected five-trial dataset with the exact free-energy readout, and uses the public probability-role bridge without importing this paper or its diagnostic models.
the_quench_obstructs_the_budget_without_obstructing_consistency · canonical_marginals_and_the_exact_identity_do_not_supply_estimator_consistency · large_work_variance_does_not_force_a_rare_low_work_tail · eight independently registered fidelity boundaries
Concept guide
Jarzynski equality
The exact ensemble identity between exponential trajectory work and the endpoint free-energy difference for a protocol satisfying a declared route.
JarzynskiEqualityIsolated Hamiltonian derivation
Selected equation-(3) trajectory work, positive inverse temperature, canonical preparation, Liouville transport, work–energy balance, pointwise Boltzmann cancellation, the system partition ratio, and both equation-(2a)/(2b) outputs.
selected_work_definition_retains_equation_three_formula · isolated_hamiltonian_switching_yields_jarzynskiFull partition ratio
The combined system–reservoir ratio Y1/Y0 obtained from full phase-space transport.
FullPartitionRatioDefinitionSame full endpoint setup
Equality of system configurations together with equality of complete initial and final system–reservoir Hamiltonians.
SameEndpointSetupWeak-reservoir law
The all-protocol equality scoped to positive β, finite classical dynamics, canonical preparation, work and Hamiltonian conditions, Liouville conservation, a reservoir large enough for canonical system sampling, and sufficiently weak coupling.
WeakReservoirJarzynskiLawQuasistatic reference
A same-full-endpoint comparison protocol whose trajectory-independent work equals thermodynamic integration and the free-energy difference.
HasQuasistaticReferenceDirect partition reduction
The alternative bridge Y1/Y0 = Z1/Z0 under sufficiently weak coupling, independent of the quasistatic reference.
WeakCouplingPartitionReductionPath/rate independence
Equality of exponential work averages for protocols with the same full endpoint setup, derived from full-ratio invariance rather than the central law.
FullPartitionRatioEndpointInvariantMean-work bound
The ensemble inequality ΔF ≤ ⟨W⟩ obtained from the exact identity, an explicit mean definition, and Jensen convexity.
MeanWorkBoundGaussian cumulant relation
The conditional identification Wdiss = βσ²/2 obtained only by combining a Gaussian cumulant output with Jarzynski’s equality.
GaussianCumulantCalculationAlternative dynamics
Independent Nosé–Hoover extended-phase-space and discrete Metropolis calculations establishing the equality.
NoseHooverPhaseSpaceCalculation · MetropolisCalculationRare-event sampling obstruction
A measured rare low-work event can dominate the exponential mean. A separate quantitative risk assessment excludes reliable estimation within a declared sample budget.
FiniteWorkSamplingPlan.RareLowWorkDominanceShared nonequilibrium-work semantics
The reusable selected-work model with direct exact identity and ensemble mean bound. A source-sensitive projection separately retains the typed Jarzynski Hamiltonian derivation. Calculation contracts are recoverable from the outputs; derivation provenance is not, and grounding requires the setup independently.
toNonequilibriumWorkIdentityContext · JarzynskiHamiltonianAverageWorkDerivationComplete route inventory, formal separations, and provenance
The source map declares ten routes, ninety-one claims, and ninety-one steps. Coverage gives every equation-level atom paper-local semantics, certifies each route from its exact dependency closure, and proves semantic realization exhaustive.
| Route | Direct dependency | Outputs | Profile |
|---|---|---|---|
| Isolated Hamiltonian | — | Isolated Jarzynski equality | exact Hamiltonian derivation |
| Exact full-reservoir ratio | — | Full ratio and endpoint invariance | exact full-space derivation |
| Physical reservoir | Exact full-reservoir ratio | Central weak law, selected equality, path/rate independence | quasistatic weak-coupling bridge |
| Direct weak-coupling reduction | Exact full-reservoir ratio | Alternative all-protocol law | direct partition reduction |
| Quasistatic limit | Physical reservoir | Thermodynamic-integration identity | equilibrium limit |
| Sudden limit | Physical reservoir | Free-energy perturbation identity | instantaneous limit |
| Ensemble consequences | Physical reservoir | Mean bound, nonnegative dissipation, Gaussian relation | convexity and cumulants |
| Thermostat extensions | — | Nosé–Hoover and Metropolis equalities | alternative dynamics |
| Practical scope | Physical reservoir | Exact equality and budget-limited sampling obstruction | applicability qualification |
| Finite-sampling consistency | Thermostat extensions | Convergence in probability of the logarithmic free-energy estimator | explicit convergence input and exact mean |
Isolated Hamiltonian · isolated_hamiltonian_route_is_semantically_realized
Exact full-reservoir ratio · full_reservoir_partition_ratio_route_is_semantically_realized
Physical reservoir · physical_reservoir_route_is_semantically_realized
Direct reduction · direct_weak_coupling_reduction_route_is_semantically_realized
Quasistatic limit · quasistatic_limit_route_is_semantically_realized
Sudden limit · sudden_limit_route_is_semantically_realized
Ensemble consequences · ensemble_consequences_route_is_semantically_realized
Thermostat extensions · thermostat_extensions_route_is_semantically_realized
Practical scope · practical_scope_route_is_semantically_realized
Finite-sampling consistency · finite_sampling_consistency_route_is_semantically_realized
Selected formal countermodels
| Available fact | Conclusion not supplied | Lean witness |
|---|---|---|
| Named trajectory-work label and positive duration | The printed equation-(3) bounded work integral | named_trajectory_work_definition_does_not_supply_equation_three |
| Same system configurations | Same full endpoint Hamiltonians or partition ratio | same_system_endpoints_do_not_determine_full_endpoint_data |
| Exponential average equals each protocol’s full ratio | Path/rate independence | full_partition_ratio_identity_alone_does_not_give_path_rate_independence |
| Exact full partition-ratio identity | Weak-reservoir free-energy law without a transfer bridge | full_partition_ratio_identity_does_not_supply_weak_reservoir_law |
| Exact full ratio plus endpoint invariance | Weak-reservoir free-energy law without the quasistatic comparison equality | endpoint_invariant_full_partition_ratio_does_not_supply_weak_reservoir_law_without_quasistatic_comparison |
| Exact ensemble exponential identity | Reversible work on every trajectory | exact_ensemble_identity_does_not_imply_pathwise_reversible_work |
| Canonical density and Liouville transport | Pointwise cancellation without work–energy balance | canonical_density_and_liouville_need_work_energy_balance |
| Endpoint density equality | A selected final-to-initial trajectory back-map | endpoint_density_equality_does_not_supply_trajectory_back_map |
| Invertible evolution and normalized probability pushforward | Liouville phase-volume preservation | invertible_probability_transport_does_not_supply_liouville_density_conservation |
| Actual Hamiltonian gradients, matching endpoints, finite work and correct endpoint energy change | Hamilton equations for the selected trajectory | correct_endpoint_work_does_not_establish_hamilton_equations |
| Weak system-reservoir interaction | A reservoir large enough for canonical system sampling | weak_coupling_does_not_supply_large_reservoir_sampling_scope |
| Gaussian cumulant output | Identification with free energy without Jarzynski’s equality | gaussian_cumulant_output_does_not_identify_free_energy_without_jarzynski |
| Exact identity and Jensen for the actual ensemble | A bound on an unrelated value merely labeled mean work | ensemble_jensen_does_not_bound_an_unrelated_mean_work_label |
Value-level countermodel boundary
The named work witness retains positive switching duration and the stated constant-rate parameter convention, but its nonzero work value disagrees with the zero Hamiltonian-derivative integral. The work-definition domain is therefore substantive even when the printed bounded integral fails.
Machine-checked audit boundary
argument_wellFormed, argument_auditable, and routes_wellFormed certify graph structure. every_source_claim_has_semantics covers all ninety-one claims, and route_semantic_realization_is_exhaustive covers all ten routes. Dedicated audits retain the premise-free equation-(3) work formula, the exact equation-(2a)-to-(2b) premise map, large-reservoir and weak-coupling scope, full-endpoint dependence, exact-ratio independence from quasistatic transfer, the source-ordered quasistatic-comparison dependency, the quasistatic-reference/direct-reduction distinction, absence of deferred calculations from both Hamiltonian laws, independence of thermostat equalities from weak coupling, author-expectation status in sampling, and the exact equality and actual mean/variance dependencies of the Gaussian and Jensen consequences, plus the independent sampling-convergence route.
Lean-encoded bibliographic record
C. Jarzynski, A nonequilibrium equality for free energy differences (1997), complete original arXiv v1 manuscript.
TraceComplete Lean semantic identifier ledger
This source-derived inventory records all current semantic theorems, source claims, steps, and routes. It is an index, not a substitute for their physical content or proofs.
Checked paper-local theorems: a_nonempty_sample_has_a_strictly_positive_exponential_mean, budget_failure_bounds_exclude_only_affordable_reliable_counts, independent_repetitions_have_normalized_sample_laws, independent_repetitions_compute_the_probability_of_missing_the_rare_event, missing_all_low_work_events_can_force_the_actual_estimator_to_fail, missing_event_probability_is_a_lower_bound_on_estimator_failure, an_independent_missed_tail_bound_controls_every_affordable_count, the_exact_positive_reference_has_the_correct_free_energy_readout, relative_exponential_accuracy_controls_the_free_energy_error, consistency_of_the_exponential_mean_transfers_through_the_logarithm, a_normalized_integrable_work_ensemble_has_a_positive_exponential_reference, independent_finite_exponential_means_are_square_integrable, independent_finite_exponential_means_are_unbiased, independent_finite_exponential_means_retain_the_inverse_sample_count_variance, independent_finite_exponential_means_have_a_computed_chebyshev_bound, finite_second_moment_and_independent_repetition_supply_consistency, a_reliable_count_has_an_actual_accurate_sample, the_accuracy_selection_bridge_uses_the_logarithmic_error_bound, reliable_sampling_exhibits_a_nonvacuous_accuracy_property, statistical_reliability_transfers_the_error_bound_only_to_a_selected_sample, consistency_supplies_reliable_finite_counts_beyond_any_fixed_budget, equation_three_retains_zero_and_unit_parameter_endpoints, named_trajectory_work_definition_does_not_supply_equation_three, selected_work_definition_retains_equation_three_formula, jarzynski_equality_and_positive_beta_yield_log_form, canonical_initial_density_is_strictly_positive, canonical_initial_density_integrates_to_one, system_partition_ratio_is_strictly_positive, system_partition_identity_gives_positive_exponential_average, full_canonical_initial_density_is_strictly_positive, full_canonical_initial_density_integrates_to_one, full_partition_ratio_is_strictly_positive, full_partition_identity_gives_positive_exponential_average, weak_reservoir_conditions_retain_large_reservoir_sampling_scope, normalized_work_ensemble_derives_exponential_jensen, exponential_jensen_realizes_generic_convexity_transfer, canonical_liouville_and_work_energy_give_pointwise_cancellation, liouville_transport_retains_selected_initial_point_on_unique_trajectory, pointwise_cancellation_integrates_to_partition_ratio, full_canonical_liouville_and_work_energy_give_pointwise_cancellation, full_liouville_transport_retains_selected_initial_point_on_unique_trajectory, full_pointwise_cancellation_integrates_to_partition_ratio, endpoint_boltzmann_integrals_yield_partition_ratio_invariance, full_partition_ratio_identity_yields_path_rate_independence, quasistatic_reference_yields_endpoint_exponential_average, quasistatic_references_yield_comparison_equality, full_partition_ratio_and_quasistatic_comparison_yield_jarzynski_law, full_partition_ratio_and_quasistatic_references_yield_jarzynski_law, isolated_hamiltonian_switching_yields_jarzynski, weakly_coupled_reservoir_yields_jarzynski, weakly_coupled_reservoir_law_from_full_partition_ratio, weakly_coupled_reservoir_law, exponential_work_average_is_endpoint_independent, free_energy_from_exponential_work_average, quasistatic_limit_recovers_thermodynamic_integration, sudden_limit_recovers_free_energy_perturbation, jarzynski_and_jensen_imply_mean_work_bound, mean_work_bound_gives_nonnegative_dissipated_work, jarzynski_and_gaussian_cumulants_give_fluctuation_dissipation_relation, gaussian_fluctuation_dissipation_uses_the_actual_work_variance, nose_hoover_switching_yields_jarzynski_without_weak_coupling, metropolis_switching_yields_jarzynski, rare_event_risk_bounds_obstruct_only_sampling_within_the_declared_budget, actual_work_sampling_consistency_gives_free_energy_consistency, realizes_generic_nonequilibrium_work_semantics, nonequilibrium_work_model_retains_paper_semantics, jarzynski_inputs_realize_shared_nonequilibrium_work_setup, hamiltonian_transport_realizes_shared_work_identity_calculation, exponential_jensen_realizes_shared_work_convexity_bridge, jarzynski_inputs_make_shared_nonequilibrium_work_route_applicable, jarzynski_hamiltonian_route_realizes_shared_average_work_derivational_reduction, jarzynski_hamiltonian_inputs_realize_structural_nonequilibrium_work_explanation, jarzynski_source_derivation_makes_shared_work_route_applicable, jarzynski_source_inputs_realize_source_structural_nonequilibrium_work_explanation, jarzynski_source_inputs_realize_source_average_work_derivational_reduction, jarzynski_hamiltonian_route_realizes_shared_nonequilibrium_work_result, jarzynski_hamiltonian_route_exhibits_nonvacuous_shared_nonequilibrium_work_identity_and_bound, jarzynski_model_inputs_establish_theory_model_grounding, jarzynski_hamiltonian_route_establishes_grounded_shared_result, grounded_jarzynski_work_result_transfers_every_shared_claim, finite_canonical_updates_derive_the_paper_work_identity_and_mean_bound, finite_work_readouts_define_a_genuine_ensemble_mean, actual_finite_updates_supply_the_discrete_metropolis_calculation, normalized_physical_canonical_density_is_nonvacuously_realized, formal_canonical_density_does_not_supply_positive_partition, formal_canonical_density_does_not_supply_normalized_ensemble, formal_canonical_density_does_not_supply_positive_density, formal_partition_integral_does_not_supply_positive_partition, positive_partition_and_density_formula_do_not_supply_normalization, formal_partition_ratio_does_not_supply_positive_initial_partition, formal_partition_ratio_does_not_supply_positive_final_partition, formal_partition_ratio_does_not_supply_positive_ratio, positive_initial_partition_does_not_supply_positive_final_partition, same_system_endpoints_do_not_determine_full_endpoint_data, full_partition_ratio_identity_alone_does_not_give_path_rate_independence, full_partition_ratio_identity_does_not_supply_weak_reservoir_law, endpoint_invariant_full_partition_ratio_does_not_supply_weak_reservoir_law_without_quasistatic_comparison, fluctuating_work_satisfies_exact_exponential_identity, exact_ensemble_identity_does_not_imply_pathwise_reversible_work, canonical_density_and_liouville_need_work_energy_balance, endpoint_density_equality_does_not_supply_trajectory_back_map, weak_coupling_does_not_supply_large_reservoir_sampling_scope, large_reservoir_size_does_not_supply_canonical_system_sampling, gaussian_cumulant_output_does_not_identify_free_energy_without_jarzynski, ensemble_jensen_does_not_bound_an_unrelated_mean_work_label, work_is_the_actual_controlled_energy_change, the_rare_initial_state_has_its_computed_canonical_probability, actual_initial_probability_weights, the_canonical_law_computes_every_observable_mean, the_mean_work_is_minus_one, every_two_state_observable_has_a_finite_second_moment, the_actual_work_variance_is_ninety_nine, the_exponential_mean_is_computed_from_the_same_law, the_exponential_second_moment_has_its_actual_variance, the_energy_quench_has_the_actual_jarzynski_identity, the_low_work_boltzmann_weight_is_large, the_sampling_domain_is_physically_inhabited, the_repeated_trials_are_independent, the_selected_work_fluctuations_exceed_the_declared_thermal_scale, the_actual_rare_low_work_event_dominates_the_exponential_mean, the_independent_quench_estimator_is_consistent, the_quench_free_energy_estimator_is_consistent, rare_low_work_dominance_does_not_preclude_reliable_finite_sampling, missing_the_rare_state_leaves_only_unit_exponential_weight, unit_weight_is_outside_the_declared_relative_accuracy, the_probability_of_missing_the_rare_state_exceeds_the_budget_allowance, the_quench_has_computed_failure_bounds_at_every_affordable_count, the_quench_obstructs_the_budget_without_obstructing_consistency, an_all_common_sample_has_unit_exponential_mean, every_finite_all_common_sample_has_positive_probability, every_nonempty_all_common_sample_fails_the_actual_accuracy_test, reliable_finite_sampling_does_not_make_every_dataset_accurate, a_selected_finite_dataset_has_the_exact_exponential_mean, a_selected_finite_dataset_returns_the_exact_free_energy, a_correct_completed_dataset_does_not_supply_statistical_reliability, an_empty_sample_is_not_a_reliable_experiment, raising_the_rare_level_computes_positive_work_and_the_same_large_variance, large_work_variance_does_not_force_a_rare_low_work_tail, repeating_one_canonical_draw_preserves_every_single_trial_marginal, correlated_repetitions_still_have_normalized_sample_laws, correlated_all_common_data_keep_the_original_probability, canonical_marginals_and_the_exact_identity_do_not_supply_estimator_consistency.
Checked route-realization theorems: normalized_ensembles_realize_reference_average_rules, actual_work_moments_realize_source_jensen, isolated_canonical_density_atom_retains_positive_partition_and_density, isolated_canonical_density_atom_is_normalized, system_partition_ratio_atom_is_strictly_positive, isolated_partition_identity_atom_retains_positive_exponential_average, full_canonical_density_atom_retains_positive_partition_and_density, full_canonical_density_atom_is_normalized, full_partition_ratio_atom_is_strictly_positive, full_partition_identity_atom_retains_positive_exponential_average, every_source_claim_has_semantics, isolated_hamiltonian_route_is_semantically_realized, full_reservoir_partition_ratio_route_is_semantically_realized, physical_reservoir_route_is_semantically_realized, direct_weak_coupling_reduction_route_is_semantically_realized, quasistatic_limit_route_is_semantically_realized, sudden_limit_route_is_semantically_realized, ensemble_consequences_route_is_semantically_realized, thermostat_extensions_route_is_semantically_realized, practical_scope_route_is_semantically_realized, finite_sampling_consistency_route_is_semantically_realized, all_routes_are_semantically_realizable, route_semantic_realization_is_exhaustive.
Checked source-map theorems: argument_wellFormed, argument_auditable, routes_wellFormed, routes_have_exact_predecessor_graph, isolated_source_contract_steps_are_independent_hypotheses, limit_and_extension_source_contract_steps_are_independent_hypotheses, result_steps_apply_exact_semantic_inputs, limit_and_practical_result_steps_apply_exact_semantic_inputs, central_law_retains_weak_coupling_qualification, path_rate_independence_depends_on_full_ratio_endpoint_invariance, path_rate_independence_depends_on_full_endpoint_setup, central_law_depends_on_quasistatic_reference, central_law_consumes_source_ordered_quasistatic_comparison, direct_reduction_law_is_independent_of_quasistatic_reference, exact_reservoir_ratio_is_independent_of_quasistatic_reference, isolated_equality_is_independent_of_deferred_calculation, physical_reservoir_law_is_independent_of_deferred_calculation, thermostat_equalities_are_independent_of_weak_coupling_step, practical_sampling_conclusion_retains_author_expectation, gaussian_relation_depends_on_jarzynski_equality, mean_work_bound_depends_on_ensemble_mean_definition, finite_sampling_consistency_is_independent_of_the_practical_obstruction, the_budget_risk_claim_does_not_require_the_exact_work_identity.
Semantic atoms: finiteClassicalSwitchingSetup, positiveInverseTemperature, workIsGeneralizedForceIntegralEq3, isolatedCanonicalPreparation, isolatedCanonicalDensityEquation, isolatedHamiltonianDynamics, isolatedWorkEnergyEquation, isolatedLiouvilleTransportEquation, isolatedExponentialAveragePhaseIntegralEq6, isolatedPointwiseBoltzmannCancellation, phaseSpaceIntegralCongruence, phaseSpaceIntegralScaling, finalBoltzmannIntegralEqualsPartitionFunction, systemPartitionRatioDefinition, isolatedExponentialAverageEqualsPartitionRatioEq8, systemPartitionRatioEncodesFreeEnergy, isolatedJarzynskiEquality, isolatedJarzynskiLogEqualityEq2b, fullCanonicalDensityEquation, fullWorkEnergyEquation, fullLiouvilleTransportEquation, fullExponentialAveragePhaseIntegral, fullPointwiseBoltzmannCancellation, fullPhaseSpaceIntegralCongruence, fullPhaseSpaceIntegralScaling, fullInitialBoltzmannIntegralEqualsPartitionFunction, fullFinalBoltzmannIntegralEqualsPartitionFunction, fullEndpointBoltzmannIntegralCongruence, fullPartitionRatioDefinition, fullExponentialAverageEqualsPartitionRatioEq9, fullPartitionRatioEndpointInvariant, quasistaticReferenceForEveryProtocol, allProtocolAverageCongruence, allProtocolAverageConstant, weakCouplingPartitionReductionRule, endpointPartitionRelationRule, weakReservoirJarzynskiLaw, directWeakCouplingJarzynskiLaw, selectedWeakReservoirConditions, selectedReservoirJarzynskiEquality, quasistaticComparisonEquality, selectedProtocolsHaveSameFullEndpointSetup, exponentialWorkAverageIndependentOfPathAndRate, quasistaticWeakReservoirConditions, quasistaticJarzynskiEquality, quasistaticSwitching, quasistaticWorkFormula, averageRespectsPointwiseEquality, averageOfConstant, thermodynamicIntegrationIdentityEq4, suddenWeakReservoirConditions, suddenJarzynskiEquality, instantaneousSwitching, hardWallExceptionExcluded, suddenWorkFormula, suddenAverageRespectsPointwiseEquality, freeEnergyPerturbationIdentityEq5, consequenceWeakReservoirConditions, consequenceJarzynskiEquality, meanWorkIsEnsembleAverage, workVarianceIsEnsembleVariance, exponentialJensenBound, meanWorkBoundEq1, dissipatedWorkNonnegative, gaussianWorkDistribution, cumulantExpansionValid, gaussianCumulantCalculation, gaussianFluctuationDissipationRelationEq12, noseHooverDynamics, noseHooverCanonicalInitialDensityEq15, noseHooverDensityEvolutionEq16, noseHooverAccumulatedWorkEq17, noseHooverPhaseSpaceCalculation, noseHooverJarzynskiEqualityWithoutWeakCoupling, metropolisDynamics, metropolisCanonicalPreparation, metropolisDiscreteWorkSum, metropolisCalculation, metropolisJarzynskiEquality, practicalWeakReservoirConditions, practicalJarzynskiEquality, practicalSamplingDomain, largeFluctuationsComparedWithThermalScale, largeFluctuationsProduceRareEventDominance, rareEventDominance, rareEventBudgetRiskAssessment, budgetLimitedSampling, computationalSamplingDomain, exponentialSamplingConsistencyCalculation, exponentialSampleMeanConsistent, freeEnergyEstimatorConsistent.
Source claims: switchingSetup, inverseTemperature, workDefinition, isolatedPreparation, isolatedCanonicalDensity, isolatedDynamics, isolatedWorkEnergy, isolatedLiouville, isolatedAverageIntegral, isolatedPointwiseCancellation, integralCongruence, integralScaling, finalBoltzmannIntegral, partitionRatioDefinition, isolatedPartitionRatio, isolatedFreeEnergyRelation, isolatedEquality, isolatedLogEquality, reservoirCanonicalDensity, reservoirWorkEnergy, reservoirLiouville, reservoirAverageIntegral, reservoirPointwiseCancellation, reservoirIntegralCongruence, reservoirIntegralScaling, reservoirInitialIntegral, reservoirFinalIntegral, reservoirEndpointIntegralCongruence, reservoirRatioDefinition, reservoirPartitionRatio, reservoirEndpointInvariant, quasistaticReferences, referenceAverageCongruence, referenceAverageConstant, weakCouplingReduction, endpointPartitionRelation, centralWeakReservoirLaw, directReductionLaw, selectedReservoirConditions, selectedReservoirEquality, quasistaticComparisonEquality, sameFullEndpointSetup, pathRateIndependence, slowConditions, slowEquality, slowRegime, slowWorkFormula, slowAverageCongruence, slowAverageConstant, thermodynamicIntegrationIdentity, suddenConditions, suddenEquality, suddenRegime, hardWallScope, suddenWorkFormula, suddenAverageCongruence, freeEnergyPerturbationIdentity, consequenceConditions, consequenceEquality, meanWorkDefinition, workVarianceDefinition, jensenBound, meanWorkBound, nonnegativeDissipation, gaussianDistribution, cumulantExpansion, gaussianCalculation, fluctuationDissipationRelation, noseHooverEquations, noseHooverPreparation, noseHooverDensityEquation, noseHooverWorkEquation, noseHooverCalculation, noseHooverEquality, metropolisEquations, metropolisPreparation, metropolisWorkDefinition, metropolisCalculationOutput, metropolisEquality, practicalConditions, practicalEquality, practicalSamplingDomain, largeFluctuationCondition, largeFluctuationBridge, rareEventDominance, samplingRiskAssessment, budgetLimitedSampling, computationalSamplingDomain, samplingConsistencyCalculation, exponentialSampleMeanConsistency, freeEnergySamplingConsistency.
Source-ordered inference steps: specifySwitchingSetup, statePositiveInverseTemperature, defineTrajectoryWork, prepareIsolatedCanonicalEnsemble, stateIsolatedCanonicalDensityEquation, imposeIsolatedHamiltonianDynamics, identifyIsolatedWorkWithEnergyChange, invokeLiouvilleConservation, stateExponentialAveragePhaseIntegral, derivePointwiseBoltzmannCancellation, statePhaseSpaceIntegralCongruence, statePhaseSpaceIntegralScaling, identifyFinalBoltzmannIntegral, defineSystemPartitionRatio, deriveIsolatedPartitionRatio, stateIsolatedFreeEnergyRelation, concludeIsolatedEquality, deriveIsolatedLogEquality, stateReservoirCanonicalDensityEquation, stateReservoirWorkEnergyEquation, stateReservoirLiouvilleTransportEquation, stateReservoirExponentialAveragePhaseIntegral, deriveReservoirPointwiseBoltzmannCancellation, stateReservoirIntegralCongruence, stateReservoirIntegralScaling, identifyReservoirInitialBoltzmannIntegral, identifyReservoirFinalBoltzmannIntegral, stateFullEndpointBoltzmannIntegralCongruence, defineFullPartitionRatio, deriveFullPartitionRatio, deriveFullPartitionRatioEndpointInvariant, stateQuasistaticReferences, stateReferenceAverageCongruence, stateReferenceAverageConstant, stateWeakCouplingReduction, stateEndpointPartitionRelation, deriveCentralWeakReservoirLaw, deriveDirectReductionLaw, instantiateSelectedReservoirConditions, deriveSelectedReservoirEquality, deriveQuasistaticComparisonEquality, identifySameFullEndpointSetup, derivePathRateIndependence, instantiateSlowConditions, deriveSlowEquality, takeQuasistaticLimit, stateQuasistaticWorkFormula, stateSlowAverageCongruence, stateSlowAverageConstant, deriveThermodynamicIntegrationIdentity, instantiateSuddenConditions, deriveSuddenEquality, takeInstantaneousLimit, excludeHardWallException, stateSuddenWorkFormula, stateSuddenAverageCongruence, deriveFreeEnergyPerturbationIdentity, instantiateConsequenceConditions, deriveConsequenceEquality, defineMeanWork, defineWorkVariance, invokeExponentialJensenBound, deriveMeanWorkBound, deriveNonnegativeDissipation, assumeGaussianDistribution, invokeCumulantExpansion, stateGaussianCalculation, deriveFluctuationDissipationRelation, stateNoseHooverDynamics, prepareNoseHooverEnsemble, deriveNoseHooverDensityEvolution, deriveNoseHooverWorkEquation, stateNoseHooverCalculation, concludeNoseHooverEquality, stateMetropolisDynamics, prepareMetropolisEnsemble, defineMetropolisWorkSum, stateMetropolisCalculation, concludeMetropolisEquality, instantiatePracticalConditions, derivePracticalEquality, specifyPracticalSamplingDomain, stateLargeFluctuationCondition, stateLargeFluctuationBridge, inferRareEventDominance, stateSamplingRiskAssessment, concludeBudgetLimitedSampling, specifyComputationalSamplingDomain, stateSamplingConsistencyCalculation, deriveExponentialSampleMeanConsistency, deriveFreeEnergySamplingConsistency.
Independent argument routes: isolatedHamiltonian, fullReservoirPartitionRatio, physicalReservoir, directWeakCouplingReduction, quasistaticLimit, suddenLimit, ensembleConsequences, thermostatExtensions, practicalScope, finiteSamplingConsistency.
Argument-route classifications: exactHamiltonianDerivation, exactReservoirDerivation, weakCouplingDerivation, directPartitionReduction, equilibriumLimit, ensembleConsequence, alternativeDynamics, applicabilityQualification.
Current checked semantic identifiers
These complete lists follow current Lean declaration order. Historical and selected explanatory lists elsewhere retain their separate scope.
Primary semantic theorems (164)
a_nonempty_sample_has_a_strictly_positive_exponential_mean, budget_failure_bounds_exclude_only_affordable_reliable_counts, independent_repetitions_have_normalized_sample_laws, independent_repetitions_compute_the_probability_of_missing_the_rare_event, missing_all_low_work_events_can_force_the_actual_estimator_to_fail, missing_event_probability_is_a_lower_bound_on_estimator_failure, an_independent_missed_tail_bound_controls_every_affordable_count, the_exact_positive_reference_has_the_correct_free_energy_readout, relative_exponential_accuracy_controls_the_free_energy_error, consistency_of_the_exponential_mean_transfers_through_the_logarithm, a_normalized_integrable_work_ensemble_has_a_positive_exponential_reference, independent_finite_exponential_means_are_square_integrable, independent_finite_exponential_means_are_unbiased, independent_finite_exponential_means_retain_the_inverse_sample_count_variance, independent_finite_exponential_means_have_a_computed_chebyshev_bound, finite_second_moment_and_independent_repetition_supply_consistency, a_reliable_count_has_an_actual_accurate_sample, the_accuracy_selection_bridge_uses_the_logarithmic_error_bound, reliable_sampling_exhibits_a_nonvacuous_accuracy_property, statistical_reliability_transfers_the_error_bound_only_to_a_selected_sample, consistency_supplies_reliable_finite_counts_beyond_any_fixed_budget, equation_three_retains_zero_and_unit_parameter_endpoints, named_trajectory_work_definition_does_not_supply_equation_three, actual_history_supplies_equation_three, actual_coupled_history_supplies_equation_three, actual_hamiltonian_history_supplies_the_selected_work_formula, selected_work_definition_retains_equation_three_formula, jarzynski_equality_and_positive_beta_yield_log_form, actual_hamiltonian_history_supplies_work_energy_balance, actual_coupled_history_supplies_hamiltonian_embedding, actual_coupled_history_supplies_the_selected_work_formula, actual_coupled_history_supplies_total_energy_balance, actual_coupled_history_supplies_full_work_energy_equation, actual_phase_integral_congruence, actual_phase_integral_scaling, actual_full_phase_integral_congruence, actual_full_phase_integral_scaling, liouville_transport_normalizes_the_actual_work_ensemble, full_liouville_transport_normalizes_the_actual_work_ensemble, liouville_transport_gives_the_actual_final_density_integral, full_liouville_transport_gives_the_actual_final_density_integral, actual_liouville_transport_derives_equation_six, actual_full_liouville_transport_derives_the_work_integral, canonical_initial_density_is_strictly_positive, canonical_initial_density_integrates_to_one, system_partition_ratio_is_strictly_positive, system_partition_identity_gives_positive_exponential_average, full_canonical_initial_density_is_strictly_positive, full_canonical_initial_density_integrates_to_one, full_partition_ratio_is_strictly_positive, full_partition_identity_gives_positive_exponential_average, weak_reservoir_conditions_retain_large_reservoir_sampling_scope, normalized_work_ensemble_derives_exponential_jensen, exponential_jensen_realizes_generic_convexity_transfer, canonical_liouville_and_work_energy_give_pointwise_cancellation, liouville_transport_retains_selected_initial_point_on_unique_trajectory, pointwise_cancellation_integrates_to_partition_ratio, full_canonical_liouville_and_work_energy_give_pointwise_cancellation, full_liouville_transport_retains_selected_initial_point_on_unique_trajectory, full_pointwise_cancellation_integrates_to_partition_ratio, endpoint_boltzmann_integrals_yield_partition_ratio_invariance, full_partition_ratio_identity_yields_path_rate_independence, quasistatic_reference_yields_endpoint_exponential_average, quasistatic_references_yield_comparison_equality, full_partition_ratio_and_quasistatic_comparison_yield_jarzynski_law, full_partition_ratio_and_quasistatic_references_yield_jarzynski_law, isolated_hamiltonian_switching_yields_jarzynski, actual_isolated_transport_yields_jarzynski, actual_hamiltonian_history_yields_jarzynski, actual_combined_transport_yields_full_partition_ratio, actual_coupled_history_yields_full_partition_ratio, weakly_coupled_reservoir_yields_jarzynski, weakly_coupled_reservoir_law_from_full_partition_ratio, weakly_coupled_reservoir_law, exponential_work_average_is_endpoint_independent, free_energy_from_exponential_work_average, quasistatic_limit_recovers_thermodynamic_integration, sudden_limit_recovers_free_energy_perturbation, jarzynski_and_jensen_imply_mean_work_bound, mean_work_bound_gives_nonnegative_dissipated_work, jarzynski_and_gaussian_cumulants_give_fluctuation_dissipation_relation, gaussian_fluctuation_dissipation_uses_the_actual_work_variance, nose_hoover_switching_yields_jarzynski_without_weak_coupling, metropolis_switching_yields_jarzynski, rare_event_risk_bounds_obstruct_only_sampling_within_the_declared_budget, actual_work_sampling_consistency_gives_free_energy_consistency, realizes_generic_nonequilibrium_work_semantics, nonequilibrium_work_model_retains_paper_semantics, jarzynski_inputs_realize_shared_nonequilibrium_work_setup, hamiltonian_transport_realizes_shared_work_identity_calculation, exponential_jensen_realizes_shared_work_convexity_bridge, jarzynski_inputs_make_shared_nonequilibrium_work_route_applicable, jarzynski_hamiltonian_route_realizes_shared_average_work_derivational_reduction, jarzynski_hamiltonian_inputs_realize_structural_nonequilibrium_work_explanation, jarzynski_source_derivation_makes_shared_work_route_applicable, jarzynski_source_inputs_realize_source_structural_nonequilibrium_work_explanation, jarzynski_source_inputs_realize_source_average_work_derivational_reduction, jarzynski_hamiltonian_route_realizes_shared_nonequilibrium_work_result, jarzynski_hamiltonian_route_exhibits_nonvacuous_shared_nonequilibrium_work_identity_and_bound, jarzynski_model_inputs_establish_theory_model_grounding, jarzynski_hamiltonian_route_establishes_grounded_shared_result, grounded_jarzynski_work_result_transfers_every_shared_claim, finite_canonical_updates_derive_the_paper_work_identity_and_mean_bound, finite_work_readouts_define_a_genuine_ensemble_mean, actual_finite_updates_supply_the_discrete_metropolis_calculation, normalized_physical_canonical_density_is_nonvacuously_realized, formal_canonical_density_does_not_supply_positive_partition, formal_canonical_density_does_not_supply_normalized_ensemble, formal_canonical_density_does_not_supply_positive_density, formal_partition_integral_does_not_supply_positive_partition, positive_partition_and_density_formula_do_not_supply_normalization, formal_partition_ratio_does_not_supply_positive_initial_partition, formal_partition_ratio_does_not_supply_positive_final_partition, formal_partition_ratio_does_not_supply_positive_ratio, positive_initial_partition_does_not_supply_positive_final_partition, same_system_endpoints_do_not_determine_full_endpoint_data, full_partition_ratio_identity_alone_does_not_give_path_rate_independence, full_partition_ratio_identity_does_not_supply_weak_reservoir_law, endpoint_invariant_full_partition_ratio_does_not_supply_weak_reservoir_law_without_quasistatic_comparison, fluctuating_work_satisfies_exact_exponential_identity, exact_ensemble_identity_does_not_imply_pathwise_reversible_work, canonical_density_and_liouville_need_work_energy_balance, endpoint_density_equality_does_not_supply_trajectory_back_map, weak_coupling_does_not_supply_large_reservoir_sampling_scope, large_reservoir_size_does_not_supply_canonical_system_sampling, gaussian_cumulant_output_does_not_identify_free_energy_without_jarzynski, ensemble_jensen_does_not_bound_an_unrelated_mean_work_label, work_is_the_actual_controlled_energy_change, the_rare_initial_state_has_its_computed_canonical_probability, actual_initial_probability_weights, the_canonical_law_computes_every_observable_mean, the_mean_work_is_minus_one, every_two_state_observable_has_a_finite_second_moment, the_actual_work_variance_is_ninety_nine, the_exponential_mean_is_computed_from_the_same_law, the_exponential_second_moment_has_its_actual_variance, the_energy_quench_has_the_actual_jarzynski_identity, the_low_work_boltzmann_weight_is_large, the_sampling_domain_is_physically_inhabited, the_repeated_trials_are_independent, the_selected_work_fluctuations_exceed_the_declared_thermal_scale, the_actual_rare_low_work_event_dominates_the_exponential_mean, the_independent_quench_estimator_is_consistent, the_quench_free_energy_estimator_is_consistent, rare_low_work_dominance_does_not_preclude_reliable_finite_sampling, missing_the_rare_state_leaves_only_unit_exponential_weight, unit_weight_is_outside_the_declared_relative_accuracy, the_probability_of_missing_the_rare_state_exceeds_the_budget_allowance, the_quench_has_computed_failure_bounds_at_every_affordable_count, the_quench_obstructs_the_budget_without_obstructing_consistency, an_all_common_sample_has_unit_exponential_mean, every_finite_all_common_sample_has_positive_probability, every_nonempty_all_common_sample_fails_the_actual_accuracy_test, reliable_finite_sampling_does_not_make_every_dataset_accurate, a_selected_finite_dataset_has_the_exact_exponential_mean, a_selected_finite_dataset_returns_the_exact_free_energy, a_correct_completed_dataset_does_not_supply_statistical_reliability, an_empty_sample_is_not_a_reliable_experiment, raising_the_rare_level_computes_positive_work_and_the_same_large_variance, large_work_variance_does_not_force_a_rare_low_work_tail, repeating_one_canonical_draw_preserves_every_single_trial_marginal, correlated_repetitions_still_have_normalized_sample_laws, correlated_all_common_data_keep_the_original_probability, canonical_marginals_and_the_exact_identity_do_not_supply_estimator_consistency
Coverage theorems (26)
normalized_ensembles_realize_reference_average_rules, actual_work_moments_realize_source_jensen, isolated_canonical_density_atom_retains_positive_partition_and_density, isolated_canonical_density_atom_is_normalized, system_partition_ratio_atom_is_strictly_positive, isolated_partition_identity_atom_retains_positive_exponential_average, full_canonical_density_atom_retains_positive_partition_and_density, full_canonical_density_atom_is_normalized, full_partition_ratio_atom_is_strictly_positive, full_partition_identity_atom_retains_positive_exponential_average, every_source_claim_has_semantics, isolated_hamiltonian_route_is_semantically_realized, isolated_route_from_actual_measure_transport, isolated_route_from_actual_hamiltonian_history, full_reservoir_partition_ratio_route_is_semantically_realized, full_reservoir_route_from_actual_coupled_histories, physical_reservoir_route_is_semantically_realized, direct_weak_coupling_reduction_route_is_semantically_realized, quasistatic_limit_route_is_semantically_realized, sudden_limit_route_is_semantically_realized, ensemble_consequences_route_is_semantically_realized, thermostat_extensions_route_is_semantically_realized, practical_scope_route_is_semantically_realized, finite_sampling_consistency_route_is_semantically_realized, all_routes_are_semantically_realizable, route_semantic_realization_is_exhaustive
Source-map audit theorems (23)
argument_wellFormed, argument_auditable, routes_wellFormed, routes_have_exact_predecessor_graph, isolated_source_contract_steps_are_independent_hypotheses, limit_and_extension_source_contract_steps_are_independent_hypotheses, result_steps_apply_exact_semantic_inputs, limit_and_practical_result_steps_apply_exact_semantic_inputs, central_law_retains_weak_coupling_qualification, path_rate_independence_depends_on_full_ratio_endpoint_invariance, path_rate_independence_depends_on_full_endpoint_setup, central_law_depends_on_quasistatic_reference, central_law_consumes_source_ordered_quasistatic_comparison, direct_reduction_law_is_independent_of_quasistatic_reference, exact_reservoir_ratio_is_independent_of_quasistatic_reference, isolated_equality_is_independent_of_deferred_calculation, physical_reservoir_law_is_independent_of_deferred_calculation, thermostat_equalities_are_independent_of_weak_coupling_step, practical_sampling_conclusion_retains_author_expectation, gaussian_relation_depends_on_jarzynski_equality, mean_work_bound_depends_on_ensemble_mean_definition, finite_sampling_consistency_is_independent_of_the_practical_obstruction, the_budget_risk_claim_does_not_require_the_exact_work_identity
Semantic atoms (91)
finiteClassicalSwitchingSetup, positiveInverseTemperature, workIsGeneralizedForceIntegralEq3, isolatedCanonicalPreparation, isolatedCanonicalDensityEquation, isolatedHamiltonianDynamics, isolatedWorkEnergyEquation, isolatedLiouvilleTransportEquation, isolatedExponentialAveragePhaseIntegralEq6, isolatedPointwiseBoltzmannCancellation, phaseSpaceIntegralCongruence, phaseSpaceIntegralScaling, finalBoltzmannIntegralEqualsPartitionFunction, systemPartitionRatioDefinition, isolatedExponentialAverageEqualsPartitionRatioEq8, systemPartitionRatioEncodesFreeEnergy, isolatedJarzynskiEquality, isolatedJarzynskiLogEqualityEq2b, fullCanonicalDensityEquation, fullWorkEnergyEquation, fullLiouvilleTransportEquation, fullExponentialAveragePhaseIntegral, fullPointwiseBoltzmannCancellation, fullPhaseSpaceIntegralCongruence, fullPhaseSpaceIntegralScaling, fullInitialBoltzmannIntegralEqualsPartitionFunction, fullFinalBoltzmannIntegralEqualsPartitionFunction, fullEndpointBoltzmannIntegralCongruence, fullPartitionRatioDefinition, fullExponentialAverageEqualsPartitionRatioEq9, fullPartitionRatioEndpointInvariant, quasistaticReferenceForEveryProtocol, allProtocolAverageCongruence, allProtocolAverageConstant, weakCouplingPartitionReductionRule, endpointPartitionRelationRule, weakReservoirJarzynskiLaw, directWeakCouplingJarzynskiLaw, selectedWeakReservoirConditions, selectedReservoirJarzynskiEquality, quasistaticComparisonEquality, selectedProtocolsHaveSameFullEndpointSetup, exponentialWorkAverageIndependentOfPathAndRate, quasistaticWeakReservoirConditions, quasistaticJarzynskiEquality, quasistaticSwitching, quasistaticWorkFormula, averageRespectsPointwiseEquality, averageOfConstant, thermodynamicIntegrationIdentityEq4, suddenWeakReservoirConditions, suddenJarzynskiEquality, instantaneousSwitching, hardWallExceptionExcluded, suddenWorkFormula, suddenAverageRespectsPointwiseEquality, freeEnergyPerturbationIdentityEq5, consequenceWeakReservoirConditions, consequenceJarzynskiEquality, meanWorkIsEnsembleAverage, workVarianceIsEnsembleVariance, exponentialJensenBound, meanWorkBoundEq1, dissipatedWorkNonnegative, gaussianWorkDistribution, cumulantExpansionValid, gaussianCumulantCalculation, gaussianFluctuationDissipationRelationEq12, noseHooverDynamics, noseHooverCanonicalInitialDensityEq15, noseHooverDensityEvolutionEq16, noseHooverAccumulatedWorkEq17, noseHooverPhaseSpaceCalculation, noseHooverJarzynskiEqualityWithoutWeakCoupling, metropolisDynamics, metropolisCanonicalPreparation, metropolisDiscreteWorkSum, metropolisCalculation, metropolisJarzynskiEquality, practicalWeakReservoirConditions, practicalJarzynskiEquality, practicalSamplingDomain, largeFluctuationsComparedWithThermalScale, largeFluctuationsProduceRareEventDominance, rareEventDominance, rareEventBudgetRiskAssessment, budgetLimitedSampling, computationalSamplingDomain, exponentialSamplingConsistencyCalculation, exponentialSampleMeanConsistent, freeEnergyEstimatorConsistent
Claim identifiers (91)
switchingSetup, inverseTemperature, workDefinition, isolatedPreparation, isolatedCanonicalDensity, isolatedDynamics, isolatedWorkEnergy, isolatedLiouville, isolatedAverageIntegral, isolatedPointwiseCancellation, integralCongruence, integralScaling, finalBoltzmannIntegral, partitionRatioDefinition, isolatedPartitionRatio, isolatedFreeEnergyRelation, isolatedEquality, isolatedLogEquality, reservoirCanonicalDensity, reservoirWorkEnergy, reservoirLiouville, reservoirAverageIntegral, reservoirPointwiseCancellation, reservoirIntegralCongruence, reservoirIntegralScaling, reservoirInitialIntegral, reservoirFinalIntegral, reservoirEndpointIntegralCongruence, reservoirRatioDefinition, reservoirPartitionRatio, reservoirEndpointInvariant, quasistaticReferences, referenceAverageCongruence, referenceAverageConstant, weakCouplingReduction, endpointPartitionRelation, centralWeakReservoirLaw, directReductionLaw, selectedReservoirConditions, selectedReservoirEquality, quasistaticComparisonEquality, sameFullEndpointSetup, pathRateIndependence, slowConditions, slowEquality, slowRegime, slowWorkFormula, slowAverageCongruence, slowAverageConstant, thermodynamicIntegrationIdentity, suddenConditions, suddenEquality, suddenRegime, hardWallScope, suddenWorkFormula, suddenAverageCongruence, freeEnergyPerturbationIdentity, consequenceConditions, consequenceEquality, meanWorkDefinition, workVarianceDefinition, jensenBound, meanWorkBound, nonnegativeDissipation, gaussianDistribution, cumulantExpansion, gaussianCalculation, fluctuationDissipationRelation, noseHooverEquations, noseHooverPreparation, noseHooverDensityEquation, noseHooverWorkEquation, noseHooverCalculation, noseHooverEquality, metropolisEquations, metropolisPreparation, metropolisWorkDefinition, metropolisCalculationOutput, metropolisEquality, practicalConditions, practicalEquality, practicalSamplingDomain, largeFluctuationCondition, largeFluctuationBridge, rareEventDominance, samplingRiskAssessment, budgetLimitedSampling, computationalSamplingDomain, samplingConsistencyCalculation, exponentialSampleMeanConsistency, freeEnergySamplingConsistency
Step identifiers (91)
specifySwitchingSetup, statePositiveInverseTemperature, defineTrajectoryWork, prepareIsolatedCanonicalEnsemble, stateIsolatedCanonicalDensityEquation, imposeIsolatedHamiltonianDynamics, identifyIsolatedWorkWithEnergyChange, invokeLiouvilleConservation, stateExponentialAveragePhaseIntegral, derivePointwiseBoltzmannCancellation, statePhaseSpaceIntegralCongruence, statePhaseSpaceIntegralScaling, identifyFinalBoltzmannIntegral, defineSystemPartitionRatio, deriveIsolatedPartitionRatio, stateIsolatedFreeEnergyRelation, concludeIsolatedEquality, deriveIsolatedLogEquality, stateReservoirCanonicalDensityEquation, stateReservoirWorkEnergyEquation, stateReservoirLiouvilleTransportEquation, stateReservoirExponentialAveragePhaseIntegral, deriveReservoirPointwiseBoltzmannCancellation, stateReservoirIntegralCongruence, stateReservoirIntegralScaling, identifyReservoirInitialBoltzmannIntegral, identifyReservoirFinalBoltzmannIntegral, stateFullEndpointBoltzmannIntegralCongruence, defineFullPartitionRatio, deriveFullPartitionRatio, deriveFullPartitionRatioEndpointInvariant, stateQuasistaticReferences, stateReferenceAverageCongruence, stateReferenceAverageConstant, stateWeakCouplingReduction, stateEndpointPartitionRelation, deriveCentralWeakReservoirLaw, deriveDirectReductionLaw, instantiateSelectedReservoirConditions, deriveSelectedReservoirEquality, deriveQuasistaticComparisonEquality, identifySameFullEndpointSetup, derivePathRateIndependence, instantiateSlowConditions, deriveSlowEquality, takeQuasistaticLimit, stateQuasistaticWorkFormula, stateSlowAverageCongruence, stateSlowAverageConstant, deriveThermodynamicIntegrationIdentity, instantiateSuddenConditions, deriveSuddenEquality, takeInstantaneousLimit, excludeHardWallException, stateSuddenWorkFormula, stateSuddenAverageCongruence, deriveFreeEnergyPerturbationIdentity, instantiateConsequenceConditions, deriveConsequenceEquality, defineMeanWork, defineWorkVariance, invokeExponentialJensenBound, deriveMeanWorkBound, deriveNonnegativeDissipation, assumeGaussianDistribution, invokeCumulantExpansion, stateGaussianCalculation, deriveFluctuationDissipationRelation, stateNoseHooverDynamics, prepareNoseHooverEnsemble, deriveNoseHooverDensityEvolution, deriveNoseHooverWorkEquation, stateNoseHooverCalculation, concludeNoseHooverEquality, stateMetropolisDynamics, prepareMetropolisEnsemble, defineMetropolisWorkSum, stateMetropolisCalculation, concludeMetropolisEquality, instantiatePracticalConditions, derivePracticalEquality, specifyPracticalSamplingDomain, stateLargeFluctuationCondition, stateLargeFluctuationBridge, inferRareEventDominance, stateSamplingRiskAssessment, concludeBudgetLimitedSampling, specifyComputationalSamplingDomain, stateSamplingConsistencyCalculation, deriveExponentialSampleMeanConsistency, deriveFreeEnergySamplingConsistency
Route identifiers (10)
isolatedHamiltonian, fullReservoirPartitionRatio, physicalReservoir, directWeakCouplingReduction, quasistaticLimit, suddenLimit, ensembleConsequences, thermostatExtensions, practicalScope, finiteSamplingConsistency
Route kinds (8)
exactHamiltonianDerivation, exactReservoirDerivation, weakCouplingDerivation, directPartitionReduction, equilibriumLimit, ensembleConsequence, alternativeDynamics, applicabilityQualification
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.
isolatedHamiltonian
Logical kind: exactHamiltonianDerivation.
Required predecessor routes: none.
Ordered inference steps: specifySwitchingSetup, statePositiveInverseTemperature, defineTrajectoryWork, prepareIsolatedCanonicalEnsemble, stateIsolatedCanonicalDensityEquation, imposeIsolatedHamiltonianDynamics, identifyIsolatedWorkWithEnergyChange, invokeLiouvilleConservation, stateExponentialAveragePhaseIntegral, derivePointwiseBoltzmannCancellation, statePhaseSpaceIntegralCongruence, statePhaseSpaceIntegralScaling, identifyFinalBoltzmannIntegral, defineSystemPartitionRatio, deriveIsolatedPartitionRatio, stateIsolatedFreeEnergyRelation, concludeIsolatedEquality, deriveIsolatedLogEquality.
Exported conclusions: isolatedEquality, isolatedLogEquality.
fullReservoirPartitionRatio
Logical kind: exactReservoirDerivation.
Required predecessor routes: none.
Ordered inference steps: stateReservoirCanonicalDensityEquation, stateReservoirWorkEnergyEquation, stateReservoirLiouvilleTransportEquation, stateReservoirExponentialAveragePhaseIntegral, deriveReservoirPointwiseBoltzmannCancellation, stateReservoirIntegralCongruence, stateReservoirIntegralScaling, identifyReservoirInitialBoltzmannIntegral, identifyReservoirFinalBoltzmannIntegral, stateFullEndpointBoltzmannIntegralCongruence, defineFullPartitionRatio, deriveFullPartitionRatio, deriveFullPartitionRatioEndpointInvariant.
Exported conclusions: reservoirPartitionRatio, reservoirEndpointInvariant.
physicalReservoir
Logical kind: weakCouplingDerivation.
Required predecessor routes: fullReservoirPartitionRatio.
Ordered inference steps: identifySameFullEndpointSetup, derivePathRateIndependence, stateQuasistaticReferences, stateReferenceAverageCongruence, stateReferenceAverageConstant, deriveQuasistaticComparisonEquality, deriveCentralWeakReservoirLaw, instantiateSelectedReservoirConditions, deriveSelectedReservoirEquality.
Exported conclusions: centralWeakReservoirLaw, selectedReservoirEquality, pathRateIndependence.
directWeakCouplingReduction
Logical kind: directPartitionReduction.
Required predecessor routes: fullReservoirPartitionRatio.
Ordered inference steps: stateWeakCouplingReduction, stateEndpointPartitionRelation, deriveDirectReductionLaw.
Exported conclusions: directReductionLaw.
quasistaticLimit
Logical kind: equilibriumLimit.
Required predecessor routes: physicalReservoir.
Ordered inference steps: instantiateSlowConditions, deriveSlowEquality, takeQuasistaticLimit, stateQuasistaticWorkFormula, stateSlowAverageCongruence, stateSlowAverageConstant, deriveThermodynamicIntegrationIdentity.
Exported conclusions: thermodynamicIntegrationIdentity.
suddenLimit
Logical kind: equilibriumLimit.
Required predecessor routes: physicalReservoir.
Ordered inference steps: instantiateSuddenConditions, deriveSuddenEquality, takeInstantaneousLimit, excludeHardWallException, stateSuddenWorkFormula, stateSuddenAverageCongruence, deriveFreeEnergyPerturbationIdentity.
Exported conclusions: freeEnergyPerturbationIdentity.
ensembleConsequences
Logical kind: ensembleConsequence.
Required predecessor routes: physicalReservoir.
Ordered inference steps: instantiateConsequenceConditions, deriveConsequenceEquality, defineMeanWork, defineWorkVariance, invokeExponentialJensenBound, deriveMeanWorkBound, deriveNonnegativeDissipation, assumeGaussianDistribution, invokeCumulantExpansion, stateGaussianCalculation, deriveFluctuationDissipationRelation.
Exported conclusions: meanWorkBound, nonnegativeDissipation, fluctuationDissipationRelation.
thermostatExtensions
Logical kind: alternativeDynamics.
Required predecessor routes: none.
Ordered inference steps: stateNoseHooverDynamics, prepareNoseHooverEnsemble, deriveNoseHooverDensityEvolution, deriveNoseHooverWorkEquation, stateNoseHooverCalculation, concludeNoseHooverEquality, stateMetropolisDynamics, prepareMetropolisEnsemble, defineMetropolisWorkSum, stateMetropolisCalculation, concludeMetropolisEquality.
Exported conclusions: noseHooverEquality, metropolisEquality.
practicalScope
Logical kind: applicabilityQualification.
Required predecessor routes: physicalReservoir.
Ordered inference steps: instantiatePracticalConditions, derivePracticalEquality, specifyPracticalSamplingDomain, stateLargeFluctuationCondition, stateLargeFluctuationBridge, inferRareEventDominance, stateSamplingRiskAssessment, concludeBudgetLimitedSampling.
Exported conclusions: practicalEquality, budgetLimitedSampling.
finiteSamplingConsistency
Logical kind: ensembleConsequence.
Required predecessor routes: thermostatExtensions.
Ordered inference steps: specifyComputationalSamplingDomain, stateSamplingConsistencyCalculation, deriveExponentialSampleMeanConsistency, deriveFreeEnergySamplingConsistency.
Exported conclusions: freeEnergySamplingConsistency.