Formal reconstruction · Quantum foundations
Quantum Equilibrium and the Origin of Absolute Uncertainty
The logical anatomy of guided dynamics, equivariant density, conditional wave functions, single-world typicality, multitime statistics, and an environment-grounded limit on knowledge
Definitions, structures, and assumptions
Structures, classes, and inductive alternatives
- inductive
- structureThe repeated constraint selected by one guided-density route.
- structureNeutral semantics for the two densities and their common guided evolution. The equality type is Lean equality on the paper-local density carrier.
- structureThe repeated constraint paired with one typed paper-local derivation.
- structurePaper-local meanings of the theory using the density model and of the physical ensemble represented by it.
- structureProof-free semantics selected by one guided-density calculation. No field stores initial agreement, common evolution, uniqueness, or later agreement.
- structureLater density agreement produced by the selected guided evolution.
- structure
- structure
- structure
- structure
- structure
- structure
- inductive
- inductive
- inductive
- structure
- inductive
- structure
- structureA selected claim must depend on exactly these source-map steps.
- structureA selected claim must retain exactly these epistemic statuses.
- structureA selected route must name exactly these immediate predecessor routes.
- structure
- structure
- inductive
- structureOriginal sections 5-6 at two resolved subsystem configurations and two environment configurations. The actual environment selects the conditional wave; effective-branch disjointness and normalized Born probabilities remain separate source relations.
- inductiveThe paper's current-identity and continuity-equation route.
- structureA finite family of empirical tests at a fixed observation time. The conditional law is on initial configurations, not an actual-world frequency.
- structureOriginal section 3, equations (3.8)-(3.18), at one selected configuration coordinate. Derivatives and flux divergences are imported physical readouts; the complex wave, guidance velocity, Born density, current, and continuity relations themselves are retained as actual values.
- structurePaper-local physical vocabulary. All unresolved mathematics and physical interpretation occur as predicates, never as proof fields.
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- structureSection 7, equation (7.17): all selected tests concern one initial configuration law. Repeated times do not assert statistical independence.
- structure
- structureAn empirical relative frequency in an observed or selected sample.
- 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
- definitionThe imported uniqueness or propagation calculation. Merely naming a common continuity equation does not make this implication automatic.
- definition
- definition
- definition
- definition
- definition
- definitionThe selected model retains all five physical indices and all three semantic families exactly. It supplies no density agreement or propagation result.
- definition
- definition
- definitionThe exact proof-free model selected by this context.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe unique model fixed by the context's five selected indices.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe realized stopping point of the shared equivariance route, stated directly on one model. It retains initial agreement, the selected common guided evolution, and later agreement without letting the implication-valued propagation calculation become true merely because setup is absent.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- 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
- 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.
- 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
- definitionFinite two-event projection of `P(X in dx | Y) = |psi_Y(x)|^2 dx`.
- definitionThe paper's literal conditional wave `psi(x) = Psi(x,Y)`.
- definitionOccupied environment-branch support does not overlap the discarded branch.
- definition`Psi(x,y) = psi(x) Phi(y) + Psi_perp(x,y)`.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe conditioned-to-unconditioned passage retains its exact integral identity.
- definition
- definitionThe conditional joint law of all selected subsystem coordinates.
- definition
- definitionThe imported weak-law output bounds test failures, not a selected sample.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe actual positive wave-derived density is `|psi|^2`, not `|psi|`.
- definition
- definition
- definitionThe analytic substitution from `J = |psi|^2 v` into its divergence.
- definitionThe real-coordinate form of the printed Schroedinger probability current.
- definition
- definitionEquation (3.15): `partial_t rho + div(rho v) = 0`.
- definition
- definition
- definitionThe printed Bohmian velocity `v = (hbar/m) Im(grad psi / psi)`.
- definition
- definitionThe source's unsimplified current: `J = hbar/(2 i m) (psi* grad psi - psi grad psi*)`.
- definition
- definitionSchroedinger continuity: `partial_t |psi|^2 + div J = 0`.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe ensemble and wave density now obey the same selected guidance flow.
- definition
- definitionConditional predictions are normalized squared amplitudes, not chances.
- definitionEffective branch and conditional wave are tied to the actual environment.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe actual source density and both printed current formulas.
- definitionSubstitution of equation (3.17) converts current continuity to guidance continuity.
- definitionEquations (7.6)-(7.7) combine a finite test family by a union bound.
- definition
- definitionThe tests use the same initial Born measure and the subsystem Born law as the source argument. Conditional-law disintegration remains separate.
- definitionEquation (3.15): guidance transports an ensemble by its continuity law.
- definition
- definitionEquation (7.2) is an equality of actual joint probability laws.
- definition
- definition
- definition
- definition
- definition
- definitionSection 3: symmetry selects the guidance law, while the two first-order evolution equations determine the complete history from initial data.
- definitionThe selected source coordinate obeys the actual complex guiding 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
- definitionThe actual finite-sample assertion uses Born expectations of the selected bounded probes. It is not supplied by the weak-law statement alone.
- definition
- definition
- definition
- definition
- definitionSection 7, equation (7.17): every selected time refers to the same initial Born law, while subsystem reference waves may depend on time and environment. These identifications are separate from the reliability inputs.
- definition
- definition
- definitionEquations (7.13)-(7.16) retain the integration of conditional failures. This mathematical input does not identify the actual configuration as typical.
- definition
- definitionSchroedinger continuity together with equation (3.17), `J = |psi|^2 v`.
- definitionThe imported weak law returns per-test failure bounds, not a claim that one selected initial configuration passes the tests.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionRaw section 3 derivation. It retains the current identity and both continuity equations without assuming an assembled setup or shared endpoint.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- 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 (7.3) assigns an actual relative frequency to any configuration event. Approximate agreement with a Born probability is a different claim.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe selected environment has conditional amplitudes `(3, 4)` and therefore probabilities `(9 / 25, 16 / 25)`, while its actual subsystem position is `0`.
- definition
- definition
- definitionA nonzero complex phase gradient gives actual Bohmian motion and current.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe source's "most times" statement is reconstructed quantitatively: the confidence cost is the average timewise failure divided by a tolerated fraction of bad times, not the sum needed for agreement at every time.
- definition
- definitionThe common initial law and every environment-relative reference law are identified with the selected source Born measures, not arbitrary statistics.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- 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
Selected instances and coercions
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
Source mappings and interpretation choices
- 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
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- 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
- 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
- inductive
- definition
- instance
- 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
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- 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
- 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
- inductive
- definition
- instance
- 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
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- 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
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- checked statement
- definition
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- definition
- definition
- inductive
- definition
- instance
- 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
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- inductive
- definition
- instance
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- structure
- definition
- instance
- checked statement
- definition
- checked statement
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- checked statement
- checked statement
- checked statement
- recursor
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- definition
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- 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
- definition
- checked statement
- checked statement
- definition
- definition
- checked statement
- definition
- definition
- checked statement
- checked statement
- definition
- 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
- checked statement
- checked statement
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
Checked statements: parameters, hypotheses, and interpretation
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementSection 3 does not obtain the common-flow setup from guided dynamics alone. It also uses initial density agreement, both continuity calculations, the current-velocity substitution, and the common-flow calculation.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementOriginal pp. 14-15, including equation (3.16), reach the model-native stopping point: selected initial equilibrium, common guided continuity evolution, and later density agreement. Typicality and absolute uncertainty remain separate paper-local routes.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked 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 joint event uses one initial configuration for all selected times and fails when at least one of the actual empirical probes fails.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe tail event counts failed selected times, not failed probes, and retains the closed threshold and the division by the number of times.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
Axioms and trust boundaries
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
Constructors, projections, and other meaning dependencies
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- constructor
- 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
Every physical statement, dependency,
equation-level paraphrase, and epistemic qualifier in this edition is taken
only from DurrGoldsteinZanghi1992.lean,
SourceMap.lean, and Coverage.lean. Continuity-
equation uniqueness, probability disintegration, weak-law estimates,
selected typicality, and multitime factorization remain named hypotheses.
The finite union bound, reference-identification bridge, and finite
probability diagnostics are checked deductions, with their scope explicit.
The wave-density formula reaches experience through two different bridges
The central chain moves from deterministic guided dynamics to equivariant universal density, then through the actual environment to a conditional subsystem distribution. From there it forks. Equal-time product systems lead through a weak law to conditioned agreement sets and then through selected typicality to one actual universe. Environment-recorded random systems lead through retained records to multitime outcomes. Absolute uncertainty consumes the conditional formula with its own interpretive premise, not the equal-time or multitime conclusions.
environment-recorded random systems → retained records → multitime distributions
| Transition | Status | Retained qualification |
|---|---|---|
| Symmetry requirements to guidance law | paper calculation | The velocity law is supplied as a proposition-valued calculation; Lean checks its consequences. |
| Initial density equality to later equality | imported continuity uniqueness | Equivariance preserves equality; it does not establish relaxation from nonequilibrium. |
| Branch decomposition to effective wave | controlled branch selection | Macroscopic disjointness and the actual environment are explicit premises. |
| Universal measure to conditional formula | imported probability disintegration | The universal equilibrium measure and subsystem result are both required. |
| Conditional independent trials to an agreement set | imported weak law + checked finite union bound | Finite selected tests retain their summed failure budget at one time. |
| Agreement set to one actual configuration | disintegration + selected typicality | The Born-reference bridge is derived; actual membership remains a premise. |
| Recorded selections to multitime distributions | imported iterated factorization | Selected wave and record retention must be stated separately. |
| Conditional independence to absolute uncertainty | interpretive inference | All possible information must be grounded in the environment. |
| Final synthesis | open scope retained | No relativistic generalization and no explicit spin or indistinguishability analysis are supplied. |
Deterministic history and equivariant density are distinct claims
Guided dynamics assumes a Schrödinger-evolving universal wave, an actual configuration at the initial time, completion of the wave description by that configuration, and homogeneity, time-reversal, and Galilean symmetry requirements. The symmetry calculation selects the guidance law; because both wave and configuration obey first-order evolution, their initial data determine the history.
ρψ = |ψ|², Jk = [ℏ / (2i mk)] (ψ*∇kψ − ψ∇kψ*) = ρψvkψ,
Ψ(t0) + Q(t0) + the two first-order equations ⇒ Ψ(t) and Q(t) form a determined history. the actual complex guidance, Born density, current identity, and antisymmetric current are encoded as value-level Lean relations; source equations (3.8)–(3.10), (3.17), and (3.18) (1)
The setup and supplied guidance calculation retain Schrödinger evolution, actual configuration, positive Planck constant and mass, nonzero wave amplitude, the printed imaginary-part velocity, and history determination. Separate source theorems derive the exact current identity and wave-guidance continuity from the actual complex formulas.
schrodinger_evolution_actual_configuration_and_symmetry_yield_guided_dynamics · archived author PDF pp. 10–13
Equivariance starts from a different setup: at the initial time the selected ensemble law equals the actual squared-wave Born measure. The analytic calculation realizes common configuration transport and regularity. Equality at the later time is then derived from those pushforwards, not supplied as the calculation's answer.
ρt₀ = |Ψt₀|² and common guided continuity evolution
⇒ ρt = |Ψt|². ensemble continuity is equation (3.15), equivariance is equation (3.16), and the current identity is equation (3.17) (2)
nu_t=(Phi_s,t)_*nu_s; mu_t=(Phi_s,t)_*mu_s.
mu_s=nu_s implies mu_t=nu_t, with normalized laws at both times. The initial wave is square-integrable and its Born law normalized; the later wave is a.e. strongly measurable. The flow map is a.e. measurable under both initial laws. The nonvacuous result also requires s!=t and an initial event with probability strictly between zero and one. (2a)
This is the measure-level commutative diagram in section 3's footnote. The original density representatives are calibrated to the actual complex wave; ensemble densities must be nonnegative and a.e. measurable. Flow construction from guidance and continuity remains an explicit analytic input. The forward theorem does not presume global invertibility at wave-function nodes.
the_actual_guided_ensemble_realizes_nonvacuous_born_equivariance · actual_equivariance_retains_the_source_density_calibration
Initial equality, realized common transport, and state regularity establish later equality of the actual measures and a normalized square-integrable later wave.
quantum_equilibrium_route_realizes_shared_guided_density_equivariance · archived author PDF pp. 14–15
dgz_source_inputs_establish_equivariance_setup_and_calculation
derives common flow through ensemble continuity, Schrödinger
current continuity, J = |psi|^2 v, and substitution.
dgz_source_inputs_make_shared_equivariance_route_applicable
then enters the shared route. The conclusions
dgz_source_inputs_realize_structural_guided_density_equivariance_explanation
and
dgz_source_inputs_realize_source_structural_guided_density_equivariance_explanation
keep the mechanism-neutral explanation distinct from the one
retaining the typed 1992 derivation.
The shared established result is the direct initial/common-evolution/later endpoint. Its theory-model grounding requires the selected initial agreement and common evolution, but not the imported propagation calculation or later agreement.
No relaxation theorem is hidden here
The field arbitraryNonequilibriumRelaxesToWaveDensity remains absent from the equivariance setup and conclusion. The strengthened boundary now uses an actual oscillator wave and two transported Gaussian laws; the older scalar history is only a formula-level illustration.
An evolving normalized wave tests the distinction
A_t(x)=sqrt(1/sqrt(2*pi))*exp(-(x-sin(t))^2/4).
theta_t(x)=cos(t)*x/2-sin(t)*cos(t)/4-t/2; psi_t=A_t*exp(i*theta_t).
2*i*d_t psi=-2*d_xx psi+V*psi; v=2*Im(d_x psi/psi)=cos(t).
Phi_s,t(x)=x+sin(t)-sin(s); nu_t=N(sin(t),1).
J=|psi|^2*v; d_t |psi|^2+d_x J=0. The wave, current, derivatives, and trajectory law are computed from the same functions. This is a constructed control, not an additional calculation attributed to the original paper's universal system. (2b)
the_actual_wave_satisfies_the_harmonic_schrodinger_equation · the_actual_configuration_trajectories_obey_the_same_wave_guidance · the_actual_wave_and_current_satisfy_the_continuity_equation
At t=0, psi and conjugate(psi) have the same Born law,
but their actual guidance velocities are +1 and -1. The phase comparison is instantaneous; timewise conjugation is not asserted to solve the same forward Schrodinger evolution. A frozen ensemble has initial Born agreement but fails common transport and later agreement. (2c)
actual_equivariance_does_not_make_the_born_distribution_stationary · the_same_instantaneous_born_law_does_not_determine_guidance · initial_born_agreement_does_not_preserve_an_untransported_ensemble
R_*mu_t=R_*nu_t, while mu_t!=nu_t.
0 < (R_*nu_t)([0,1/4]) < 1. The record is measurable and genuinely random, not a constant readout. The two full laws follow the same actual guided flow. Selected record statistics do not reconstruct the full configuration law. (2d)
nontrivial_record_agreement_does_not_supply_full_born_equilibrium
mu_t=nu_t if and only if mu_s=nu_s. Only finite-time exact fine-grained equilibration is excluded. Weak, asymptotic, and coarse-grained relaxation are different questions; a global inverse through nodes is not assumed by forward equivariance. (2e)
The actual environment selects a conditional and effective subsystem wave
The universal configuration is split into subsystem and environment. The universal wave is decomposed into branches, the selected branch has macroscopically disjoint environment support, and the actual environment occupies that branch. A controlled calculation then supplies four outputs: an effective wave, a conditional-wave identity, equality between the selected and conditional waves, and guidance of the subsystem by that wave.
Ψ(x,y) = ψ(x)Φ(y) + Ψ⊥(x,y), Y ∈ supp Φ, suppy Φ ∩ suppy Ψ⊥ = ∅,
ψY(x) = Ψ(x,Y) = ψ(x)Φ(Y), ψ guides X. effective branch equations (5.17)–(5.18); actual-environment conditional wave equation (5.19); Φ(Y) is nonzero (3)
Subsystem–environment splitting, the actual complex branch decomposition, disjoint environment support, actual occupied-branch selection, and the supplied calculation establish the effective and conditional waves. The selected conditional wave agrees with the effective branch up to its nonzero environment factor.
branch_decomposition_and_actual_environment_yield_effective_and_conditional_wave · archived author PDF pp. 21–26
The result says that the conditional wave guides the subsystem. It does not
say that this wave necessarily obeys an autonomous Schrödinger equation.
The theorem conditional_wave_source_does_not_supply_autonomous_schrodinger_evolution exhibits the full complex source model with actual branch selection and normalized Born probabilities but without autonomous conditional evolution.
Universal equilibrium descends to the subsystem only through conditional disintegration
The conditional-probability route joins the two descendants of guided dynamics. It consumes established equivariance, the effective/conditional subsystem wave, and a universal quantum-equilibrium measure defined by the squared universal-wave density. An imported conditional-probability calculation disintegrates that universal density at the actual environment.
P(X=x │ Y) = |Ψ(x,Y)|² / Σz|Ψ(z,Y)|²,
and subsystem configuration and environment are conditionally independent given ψt. source equation (6.1), with normalization explicitly required by footnote 24; the finite Lean model proves the probabilities sum to one (4)
Established universal equivariance, the universal measure, the subsystem-wave result, and the supplied calculation establish normalized squared-amplitude conditional probabilities and conditional independence. For the selected actual environment, amplitudes (3,4) produce exactly (9/25,16/25), while the subsystem has exactly one actual configuration.
universal_equivariance_and_conditional_wave_yield_fundamental_conditional_probability · archived author PDF pp. 30–31
The theorem explicitly extracts later-time density agreement from the
equivariance certificate, but the conditional calculation remains an
independent hypothesis. The source-map audit
equivariance_retains_imported_mathematics prevents the shared
continuity argument from being mistaken for a proof of probability
disintegration.
Product structure and a weak law bound a conditioned agreement set
Consider many simultaneous subsystems whose effective state has product form. Applying the conditional formula to that product makes their configurations conditionally independent and identically distributed at the selected time. A weak-law hypothesis controls failure of a finite nonempty family of bounded tests, for a positive tolerance and nonempty sample. All measures are normalized, and the reference is identified with the subsystem Born law. The resulting bound is conditional on the selected environment; it does not yet assert empirical agreement of the actual initial configuration.
AY = {Q : for every selected j, |M-1Σifj(Xi(Q)) - ∫fjdρY| ≤ ε},
PY(AYc) ≤ ΣjδY,j ≤ δ < 1. conditioned agreement-set bound, not universal or selected-configuration agreement (5)
The product-wave setup, actual test domain, conditional-independence calculation, and weak-law input establish a nonvacuous conditioned agreement set. The finite union bound is proved, and a strict total failure budget exhibits an agreeing configuration in the same environment fiber.
product_effective_wave_and_conditional_formula_yield_conditioned_agreement_bounds · archived author PDF pp. 33-36, equations (7.3)-(7.7)
The imported probability theorem remains visible
empirical_statistics_retain_weak_law_dependency certifies that the equal-time result inherits an imported result. The formalization therefore does not turn conditional independence alone into an empirical-frequency theorem.
Probability bounds do not select the actual configuration
Finite tests use the sum of the individual failure budgets. The
conditional-to-global step retains the integral identity
unconditionalFailure = integral conditionalFailure.
A small average does not certify every admissible environment.
Applying the empirical bound to the actual configuration still requires
membership in the agreement set, and agreement with an unrelated
reference measure does not supply agreement with the Born law.
- Two independent Bernoulli coordinates with excitation probability
1/3give a computed failure probability1/9. The double-excitation configuration remains a positive-probability exception. - Three tests each fail with probability
1/3, while their joint failure probability is1, not1/3. - A rare environment has probability
1/100and conditional failure1, despite unconditional failure1/100.
Empty samples and empty test families do not satisfy the nonvacuous contract. These are finite probability diagnostics, not complete Bohmian universes. The weak law's general large-sample limit remains an imported calculation; this route uses its selected finite-sample bounds. It does not infer full joint independence from an empirical histogram.
Section 7, archived author PDF pp. 33-36;EmpiricalAgreementData and EmpiricalAgreementControls
Quantum equilibrium is used as typicality for one actual universe
The typicality route does not reinterpret the selected ensemble as many existing universes. It uses the universal quantum-equilibrium measure to classify initial universal configurations as typical. The actual initial configuration is assumed typical in its actual environment fiber. The conditioned bounds and an explicit disintegration identity establish the global typical-property statement. The Born-reference identification derives the bridge to the selected configuration's empirical tests.
+ typical actual initial configuration + typical-property bridge
⇒ one-universe empirical statistics governed by the wave density. typicality selects a configuration; it is not an ensemble-of-universes frequency statement (6)
The theorem retains, rather than derives, typicality of the selected initial configuration. It derives the selected Born-probe inequalities and normalized empirical frequencies for configuration events. High measure alone does not supply the selection premise.
quantum_equilibrium_typicality_places_empirical_statistics_in_one_universe · archived author PDF pp. 30 and 33-36
The separate countermodel formalizes the conceptual gap: a distribution over universes, by itself, does not give frequencies within one universe. The typicality setup and bridge are the encoded answer to that gap.
ensemble_of_universes_does_not_supply_single_world_empirical_frequencies
Multitime statistics require selection and memory to be physical records
A random system is not represented as an unexplained random variable. Its subsystem and time are selected by an experiment, and that selection is recorded in the environment. The fundamental conditional formula can then be extended to the selected system. To compare several times, the selected effective wave must be nonrandom for the experiment and earlier outcomes must remain in the environment before later selections.
+ fixed selected wave + retained prior records + iterated factorization
⇒ selected outcomes are independent and have the quantum distributions. ordered recorded experiments; archived author PDF pp. 40–45 (7)
Recorded selection, the random-system conditional calculation, a fixed selected wave, retained records, and the multitime calculation establish the selected conditional formula, independence, and quantum outcome distribution.
environment_recorded_selection_and_retained_records_yield_multitime_quantum_statistics · archived author PDF pp. 40–45
The result concerns statistics of a deterministic guided history. It does
not add randomness to the underlying history. The countermodel
deterministic_history_and_quantum_statistics_do_not_imply_ontic_randomness
keeps this logical distinction explicit.
Absolute uncertainty limits environment-grounded knowledge, not objective configuration
The formal route is placed downstream of equal-time and multitime statistics. Its core setup combines the fundamental conditional result with a physical premise: every device, record, or knower carrying information about the subsystem is grounded in the environment. The interpretive bridge says that this environment-grounded information cannot improve on the conditional wave density.
+ P(X ∈ dx │ Y) = |ψ(x)|²dx + uncertainty bridge
⇒ no such information improves on |ψ|², absolute uncertainty holds,
while the actual subsystem configuration still exists. epistemic limitation with ontology retained (8)
The conditional result, environment-grounding premise, interpretive bridge, and existence of actual configuration establish all three conjuncts.
conditional_independence_and_environmental_grounding_yield_absolute_uncertainty · archived author PDF pp. 46–49
The scope assessment then records six qualifications: quantum equilibrium functions as a typicality measure; convergence or ergodicity is not required; thermodynamic and quantum equilibrium are distinct; global thermodynamic nonequilibrium permits records; spin and indistinguishability are not explicitly analyzed; and no relativistic generalization is supplied.
Guided dynamics, equivariance, conditional probability, equal-time statistics, typicality, multitime statistics, absolute uncertainty, and the scope assessment are retained as one conjunction.
paper_conclusion_retains_dynamics_statistics_uncertainty_and_scope · archived author PDF p. 56
Three statements the conclusion does not make
It does not derive dynamical relaxation, it does not convert statistical predictions into ontic randomness, and it does not deny the actual configuration. The source-map theorems absolute_uncertainty_retains_interpretive_bridge and final_conclusion_retains_nonrelativistic_scope ensure that the interpretation and omissions remain inherited.
Concept guide
Guided dynamics
First-order wave and configuration evolution selected under the paper’s symmetry requirements and fixed by initial data.
GuidedDynamicsResultEquivariance
Preservation of equality between actual ensemble and squared-wave measures under common configuration transport. It need not be stationarity of either measure.
EquivarianceCalculation · actual_configuration_transport_derives_later_density_agreementEffective wave
The macroscopically disjoint universal-wave branch occupied by the actual environment.
SubsystemWaveResultConditional wave
The universal wave evaluated at the actual environment configuration; in the selected branch it equals the effective wave and guides the subsystem.
conditionalWaveIdentityAtFundamental conditional probability
The wave-density distribution of subsystem configuration conditional on the environment, plus conditional independence given the subsystem wave.
FundamentalConditionalProbabilityResultEqual-time empirical statistics
Conditional i.i.d. subsystem configurations and nonvacuous agreement-set bounds for finite bounded tests, before any actual configuration is selected.
EqualTimeEmpiricalStatisticsResultQuantum-equilibrium typicality
Use of the universal equilibrium measure together with a separate typicality premise for the actual initial configuration in its environment fiber.
TypicalitySetupRandom system
A subsystem and time whose experimental selection is itself recorded in the environment.
RandomSystemSetupMultitime statistics
Independent quantum-distributed outcomes obtained when selected waves are fixed and prior outcomes remain recorded.
RandomSystemMultitimeResultAbsolute uncertainty
The environment-grounded limit saying available information cannot improve on the subsystem wave density, while actual configuration remains objective.
AbsoluteUncertaintyResultThermodynamic distinction
Quantum equilibrium is a global typicality measure distinct from thermodynamic equilibrium; nonequilibrium can be required for records.
ScopeAssessmentTheory–model grounding
The exact identification of the shared equivariance model with the paper-local theory and selected wave–ensemble world.
toGuidedDensityEquivarianceInterpretationRoute inventory, countermodels, and formal provenance
The source map declares nine routes, forty-one semantic claims, and forty-one
sourced steps. Raw physical and calculation inputs are premise-free;
every nonempty result step reconstructs its exact ClaimsHold
premises before applying the paper-local theorem. Coverage interprets
every atom in the paper-local framework and certifies every route under
its exact direct predecessor outputs and explicit hypotheses.
| Route | Direct dependencies | Declared output | Profile |
|---|---|---|---|
| Guided dynamics | — | Symmetry-selected first-order guided history | paper calculation |
| Density equivariance | Guided dynamics | Later ensemble–wave density agreement | imported continuity uniqueness |
| Subsystem wave | — | Effective/conditional wave identity and subsystem guidance | controlled branch selection |
| Conditional probability | Density equivariance; subsystem wave | Conditional wave-density formula and independence | imported disintegration |
| Equal-time statistics | Conditional probability | Conditional i.i.d. structure and agreement-set bounds | weak-law dependency |
| Typical single-world statistics | Equal-time statistics | Statistics for a separately selected typical actual configuration | disintegration + selection + derived bridge |
| Random-system multitime statistics | Conditional probability | Independent quantum-distributed recorded outcomes | imported multitime factorization |
| Absolute uncertainty | Conditional probability | No environment-grounded improvement; uncertainty with actual configuration | interpretive bridge |
| Paper scope | Guided dynamics; density equivariance; conditional probability; equal-time statistics; typicality; multitime statistics; absolute uncertainty | Qualified conjunction of every route | nonrelativistic scope |
Guided dynamics · guided_dynamics_route_is_semantically_realized
Density equivariance · density_equivariance_route_is_semantically_realized
Subsystem wave · subsystem_wave_route_is_semantically_realized
Conditional probability · conditional_probability_route_is_semantically_realized
Equal-time statistics · equal_time_statistics_route_is_semantically_realized
Typicality · typical_single_world_statistics_route_is_semantically_realized
Random-system multitime statistics · random_system_multitime_route_is_semantically_realized
Absolute uncertainty · absolute_uncertainty_route_is_semantically_realized
Qualified scope · paper_scope_route_is_semantically_realized
Physically inhabited fidelity boundaries
| Available fact | Conclusion not supplied | Lean witness |
|---|---|---|
| Actual Gaussian Born equivariance and guided dynamics | Finite-time exact equilibration of the displaced ensemble | the_displaced_ensemble_never_acquires_exact_born_equilibrium |
| Actual Born equivariance | A stationary Born distribution | actual_equivariance_does_not_make_the_born_distribution_stationary |
| Initial Born agreement | Preservation without common ensemble transport | initial_born_agreement_does_not_preserve_an_untransported_ensemble |
| The same instantaneous Born law | The same phase-dependent guidance | the_same_instantaneous_born_law_does_not_determine_guidance |
| Equal genuinely random modular-position records | Full configuration-law equilibrium | nontrivial_record_agreement_does_not_supply_full_born_equilibrium |
| A subsystem wave equals the conditional wave | It obeys autonomous Schrödinger evolution | conditional_wave_identity_does_not_supply_autonomous_evolution |
| A distribution over universes is given | Empirical frequencies hold inside one universe | ensemble_of_universes_does_not_supply_single_world_empirical_frequencies |
| History is determinate and outcomes have quantum statistics | The history is ontically random | deterministic_history_and_quantum_statistics_do_not_imply_ontic_randomness |
| Absolute uncertainty holds | No objective actual configuration exists | absolute_uncertainty_does_not_deny_actual_configuration |
| A zero-wave node has a totalized zero quotient | It defines physically admissible Bohmian guidance | zero_wave_node_does_not_define_a_physical_guidance_velocity |
| The real wave gradient is nonzero | Its real part supplies the Bohmian velocity | real_amplitude_gradient_does_not_supply_bohmian_velocity |
| The mass and a proposed velocity are positive | The velocity has the printed hbar/m coefficient | wrong_mass_coefficient_does_not_supply_printed_guidance |
| A nonzero current has the correct magnitude | Reversing its sign preserves the Born-guidance identity | reversing_only_the_current_breaks_born_guidance_identity |
| The amplitude and assigned density are both positive | The linear amplitude is the squared Born density | linear_amplitude_is_not_born_density |
| Schrödinger-current continuity holds | The guidance-flux divergence substitution holds | schrodinger_current_continuity_does_not_supply_guidance_flux_substitution |
| An alternative environment defines a valid different wave | That wave is conditional on the actual selected environment | alternative_environment_wave_is_not_actual_conditional_wave |
| Linear-amplitude weights are positive and normalized | They equal normalized squared Born weights | normalized_linear_weights_are_not_conditional_born_probabilities |
| Branch decomposition, conditional identity, and normalized probabilities hold | The occupied and discarded branches have disjoint support | overlapping_environment_branch_does_not_supply_effective_wave_selection |
| The full complex conditional-wave and Born source relations hold | The conditional wave obeys autonomous Schrödinger evolution | conditional_wave_source_does_not_supply_autonomous_schrodinger_evolution |
| Both conditional outcomes have strictly positive probability | More than one subsystem configuration is actually realized | nontrivial_born_probabilities_coexist_with_one_actual_configuration |
| Conditional product law and nonvacuous agreement with failure 1/9 | The double-excitation configuration passes | high_measure_agreement_does_not_make_every_configuration_agree |
| Each of three tests has failure 1/3 | The joint failure is bounded by 1/3 | the_joint_failure_is_one_not_the_individual_budget |
| Actual disintegration and average failure 1/100 | Every admitted environment has a small conditional failure | small_averaged_failure_does_not_control_every_admissible_environment |
| A sample agrees with a different normalized reference | It agrees with the selected Born probe | agreement_with_a_different_reference_is_not_born_probe_agreement |
| Normalized probability laws and a totalized empty frequency | A nonempty empirical experiment is realized | totalized_empty_sampling_does_not_realize_an_empirical_experiment |
| Every configuration vacuously passes an empty test family | A nonvacuous agreement contract is realized | empty_tests_do_not_supply_nonvacuous_agreement |
The 26 boundaries include actual Gaussian transport, complex source formulas, conditional-wave selection, and the six finite empirical-test distinctions above. The probability diagnostics use computed measures, finite sample functions, and actual reference integrals. They are not complete Bohmian-universe constructions.
Machine-checked audit boundary
argument_wellFormed, argument_auditable, routes_wellFormed, and routes_have_exact_predecessor_graph certify source-map structure. Three source-input audits require premise-free raw hypotheses, and three result-step audits require exact premise lists for every composition. route_semantic_realization_is_exhaustive proves that the nine listed certificates cover every route identifier. The status audits retain imported mathematics, the interpretive uncertainty bridge, and the open nonrelativistic scope rather than converting them into proved foundations.
Lean-encoded bibliographic record
D. Dürr, S. Goldstein, and N. Zanghì, Quantum Equilibrium and the Origin of Absolute Uncertainty, Journal of Statistical Physics 67 (1992), 843–907. All locators above refer to the archived author PDF pages stored in SourceMap.lean.
TraceComplete Lean semantic identifier ledger
Reading note. The article above is the human exposition. This collapsed cross-reference records every public theorem and every constructor of the five paper-local source-map vocabularies. It introduces no additional claim; its purpose is to make semantic omissions mechanically detectable.
Primary semantic theorems (182)
finite_test_failures_combine_with_the_sum_of_the_budgetsthe_conditional_failure_is_bounded_by_the_selected_total_budgeta_strict_failure_budget_has_an_agreeing_configuration_in_the_same_fiberconditional_control_and_disintegration_bound_unconditional_disagreementnonvacuous_conditioned_agreement_exhibits_a_selected_test_statea_nonempty_sample_has_a_normalized_empirical_frequencyan_indicator_probe_computes_the_actual_empirical_frequencyjoint_failure_bound_iff_explicit_empirical_unionmost_times_bound_iff_explicit_empirical_fractioncommon_initial_law_transfers_conditioned_bounds_to_each_selected_timeselected_times_combine_under_one_measure_without_independencethe_fraction_of_disagreeing_times_is_measurableexpected_disagreement_fraction_is_bounded_by_average_failuresmall_average_failure_controls_most_selected_timesa_strict_joint_budget_exhibits_one_configuration_passing_every_selected_timea_strict_most_times_budget_exhibits_a_configuration_with_few_bad_timescommon_born_measure_controls_joint_and_most_time_agreementthe_disagreement_fraction_is_at_most_onesource_born_density_is_strictly_positiveborn_density_and_guidance_give_printed_current_identitycurrent_substitution_gives_wave_guidance_continuityequal_initial_density_and_common_flux_give_equal_density_derivativesconditional_wave_equals_occupied_effective_branch_up_to_nonzero_factorconditional_born_probabilities_are_normalizedconditional_born_probability_is_nonnegativeactual_subsystem_configuration_is_uniquetraveling_wave_realizes_printed_guidance_current_and_continuitytime_reversed_wave_reverses_guidance_velocity_and_currentreal_stationary_wave_has_nonzero_born_density_without_motionzero_wave_node_does_not_define_a_physical_guidance_velocityreal_amplitude_gradient_does_not_supply_bohmian_velocitywrong_mass_coefficient_does_not_supply_printed_guidancereversing_only_the_current_breaks_born_guidance_identitylinear_amplitude_is_not_born_densityschrodinger_current_continuity_does_not_supply_guidance_flux_substitutionselected_environment_realizes_printed_conditional_wave_and_born_probabilitiesnontrivial_born_probabilities_coexist_with_one_actual_configurationconditional_wave_source_does_not_supply_autonomous_schrodinger_evolutionalternative_environment_changes_selected_conditional_wave_and_probabilitynonzero_wave_rescaling_preserves_normalized_conditional_probabilitiesalternative_environment_wave_is_not_actual_conditional_wavenormalized_linear_weights_are_not_conditional_born_probabilitiesoverlapping_environment_branch_does_not_supply_effective_wave_selectionthe_gaussian_amplitude_is_strictly_positivethe_squared_amplitude_is_the_actual_gaussian_densitythe_phase_factor_has_unit_modulusthe_actual_wave_born_density_is_gaussianthe_wave_is_square_integrablethe_actual_born_measure_is_a_normalized_gaussianthe_actual_configuration_maps_obey_time_compositionthe_actual_configuration_maps_are_measurable_embeddingsthe_actual_trajectories_have_the_common_velocitythe_model_born_law_uses_the_evolving_waveboth_actual_laws_follow_the_same_configuration_transportthe_wave_is_a_normalized_born_stateactual_equilibrium_is_exactly_the_zero_density_offsetthe_actual_gaussian_law_assigns_positive_mass_to_intervalsthe_actual_born_law_has_a_nontrivial_configuration_eventthe_coherent_wave_and_its_ensemble_realize_nonvacuous_equivarianceactual_equivariance_does_not_make_the_born_distribution_stationarythe_displaced_ensemble_never_acquires_exact_born_equilibriumthe_amplitude_has_its_actual_spatial_derivativethe_amplitude_has_its_actual_time_derivativethe_phase_has_its_actual_spatial_derivativethe_phase_has_its_actual_time_derivativethe_wave_has_its_actual_spatial_derivativethe_wave_has_its_actual_time_derivativethe_spatial_log_derivative_has_its_actual_derivativethe_wave_has_its_actual_second_spatial_derivativethe_actual_wave_satisfies_the_harmonic_schrodinger_equationthe_actual_wave_has_no_nodesthe_actual_wave_guidance_is_the_configuration_velocitythe_actual_configuration_trajectories_obey_the_same_wave_guidancethe_actual_probability_current_is_born_density_times_guidancethe_actual_born_density_has_its_time_derivativethe_actual_born_density_has_its_spatial_derivativethe_actual_wave_and_current_satisfy_the_continuity_equationthe_same_wave_and_flow_realize_the_oscillator_dynamicsthe_untransported_ensemble_has_a_normalized_initial_wavethe_untransported_ensemble_has_initial_born_equilibriumthe_untransported_ensemble_lacks_later_born_equilibriuminitial_born_agreement_does_not_preserve_an_untransported_ensemblethe_frozen_ensemble_fails_the_required_common_transportconjugating_the_actual_wave_preserves_its_instantaneous_born_lawconjugating_the_actual_wave_reverses_its_instantaneous_guidancethe_same_instantaneous_born_law_does_not_determine_guidancethe_displaced_and_born_ensembles_have_the_same_modular_position_lawthe_modular_position_record_has_a_genuinely_random_eventnontrivial_record_agreement_does_not_supply_full_born_equilibriumschrodinger_evolution_actual_configuration_and_symmetry_yield_guided_dynamicsguided_result_retains_actual_bohmian_velocitythe_actual_guided_ensemble_realizes_nonvacuous_born_equivarianceactual_configuration_transport_derives_later_density_agreementa_realized_source_density_defines_the_actual_born_measureactual_equivariance_retains_the_source_density_calibrationguided_dynamics_and_continuity_calculations_yield_equivariance_setupsource_derivation_retains_printed_guidance_current_and_continuitysource_derivation_yields_actual_born_guidance_current_identitysource_derivation_yields_actual_wave_guidance_continuitydgz_source_inputs_establish_equivariance_setup_and_calculationguided_density_equivariance_model_retains_paper_semanticspaper_equivariance_setup_realizes_shared_setuppaper_equivariance_calculation_realizes_shared_calculationquantum_equilibrium_inputs_make_shared_equivariance_route_applicabledgz_source_inputs_make_shared_equivariance_route_applicabledgz_source_inputs_realize_structural_guided_density_equivariance_explanationdgz_source_inputs_realize_source_structural_guided_density_equivariance_explanationquantum_equilibrium_route_realizes_shared_guided_density_equivariancequantum_equilibrium_route_exhibits_nonvacuous_shared_guided_density_equivarianceestablished_quantum_equilibrium_realizes_every_shared_claimquantum_equilibrium_model_inputs_establish_theory_model_groundingquantum_equilibrium_route_establishes_theory_model_grounded_equivariancegrounded_quantum_equilibrium_transfers_every_shared_claimbranch_decomposition_and_actual_environment_yield_effective_and_conditional_wavesubsystem_result_retains_actual_environment_conditioned_wavesubsystem_result_retains_nonzero_occupied_effective_branchuniversal_equivariance_and_conditional_wave_yield_fundamental_conditional_probabilityconditional_result_retains_normalized_born_probabilityconditional_result_probabilities_sum_to_oneconditional_result_probabilities_are_nonnegativeconditional_probability_and_product_wave_yield_equal_time_setupthe_finite_test_union_bound_realizes_the_frequency_calculationproduct_effective_wave_and_conditional_formula_yield_conditioned_agreement_boundsidentified_born_probes_realize_the_typicality_bridgeconditioned_agreement_and_disintegration_establish_the_typical_propertythe_typical_property_has_an_actual_selected_configurationquantum_equilibrium_typicality_places_empirical_statistics_in_one_universeone_initial_born_measure_controls_joint_and_most_selected_timesconditional_probability_and_recorded_selection_yield_random_system_setupenvironment_recorded_selection_and_retained_records_yield_multitime_quantum_statisticsconditional_independence_and_environmental_grounding_yield_absolute_uncertaintypaper_conclusion_retains_dynamics_statistics_uncertainty_and_scopequalified_conclusion_retains_actual_guidance_and_conditional_probabilityequivariance_does_not_imply_relaxation_from_nonequilibriumconditional_wave_identity_does_not_supply_autonomous_evolutionensemble_of_universes_does_not_supply_single_world_empirical_frequenciesdeterministic_history_and_quantum_statistics_do_not_imply_ontic_randomnessabsolute_uncertainty_does_not_deny_actual_configurationbit_weightsthe_subsystem_reference_is_the_computed_bernoulli_meanthe_two_actual_coordinates_have_the_conditional_product_lawthe_empirical_probe_fails_exactly_on_the_double_excitationthe_disagreement_event_is_the_actual_double_excitationthe_double_excitation_has_positive_probabilitythe_sample_and_test_domain_is_nonemptythe_conditional_and_initial_laws_are_actual_probabilitiesthe_selected_budget_is_strictly_less_than_onethe_individual_error_budget_is_computed_from_the_product_lawthe_conditional_and_unconditional_failures_are_one_ninththe_conditioning_identity_is_realizedthe_actual_product_law_realizes_nonvacuous_conditioned_agreementhigh_measure_agreement_does_not_make_every_configuration_agreeagreement_with_a_different_reference_is_not_born_probe_agreementtotalized_empty_sampling_does_not_realize_an_empirical_experimentempty_tests_do_not_supply_nonvacuous_agreementeach_cell_has_one_third_of_the_probabilityeach_reference_test_has_mean_one_thirdeach_probe_fails_on_its_own_cellevery_individual_test_has_failure_one_thirdno_configuration_passes_all_three_teststhe_joint_failure_is_one_not_the_individual_budgetthe_rare_environment_has_nonzero_probabilityagreement_is_the_actual_zero_outcomethe_disagreement_is_the_true_outcomethe_conditioned_failure_is_an_actual_indicatorthe_initial_and_conditioned_laws_form_a_probability_setupthe_unconditional_failure_is_one_percentthe_actual_conditioned_failures_integrate_to_the_averagesmall_averaged_failure_does_not_control_every_admissible_environmenta_time_fails_exactly_on_its_selected_cellthe_collection_has_one_normalized_initial_laweach_selected_time_has_failure_one_thirdtimewise_bounds_are_computed_from_the_common_measureevery_configuration_fails_at_one_selected_timethe_actual_bad_time_fraction_is_one_thirdthe_joint_budget_and_average_budget_are_differentmost_times_agreement_does_not_supply_all_times_agreementchanging_the_measure_can_make_each_failure_zerotime_dependent_zero_failures_do_not_give_a_common_zero_failurethe_per_time_empirical_inputs_are_realizedthe_complete_time_typicality_route_has_inhabited_inputsempty_time_selection_does_not_realize_the_empirical_domain
Coverage theorems (17)
every_source_claim_has_semanticsguided_dynamics_atom_retains_printed_bohmian_velocitysubsystem_wave_atom_retains_actual_environment_conditional_waveconditional_probability_atom_retains_normalized_born_distributionqualified_conclusion_atom_retains_guidance_and_born_probabilitytime_collection_atom_retains_born_measure_and_distinct_time_boundsguided_dynamics_route_is_semantically_realizeddensity_equivariance_route_is_semantically_realizedsubsystem_wave_route_is_semantically_realizedconditional_probability_route_is_semantically_realizedequal_time_statistics_route_is_semantically_realizedtypical_single_world_statistics_route_is_semantically_realizedcommon_measure_time_collection_route_is_semantically_realizedrandom_system_multitime_route_is_semantically_realizedabsolute_uncertainty_route_is_semantically_realizedpaper_scope_route_is_semantically_realizedroute_semantic_realization_is_exhaustive
Source-map audit theorems (14)
argument_wellFormedargument_auditableroutes_wellFormedroutes_have_exact_predecessor_graphguided_and_equivariance_source_inputs_are_independent_hypothesessubsystem_conditional_and_equal_time_source_inputs_are_independent_hypothesestypicality_random_uncertainty_and_scope_source_inputs_are_independent_hypothesesguided_and_equivariance_result_steps_apply_exact_inputssubsystem_conditional_and_equal_time_result_steps_apply_exact_inputstypicality_random_uncertainty_and_scope_result_steps_apply_exact_inputsequivariance_retains_imported_mathematicsempirical_statistics_retain_weak_law_dependencyabsolute_uncertainty_retains_interpretive_bridgefinal_conclusion_retains_nonrelativistic_scope
Semantic atoms (44)
guidedDynamicsSetupguidanceLawCalculationguidedDynamicsResultinitialQuantumEquilibriumDensityensembleGuidanceContinuityCalculationwaveCurrentContinuityCalculationcurrentVelocitySubstitutionCalculationcommonGuidedContinuityCalculationequivarianceSetupequivarianceCalculationestablishedEquivariancesubsystemWaveSetupsubsystemWaveCalculationsubsystemWaveResultuniversalEquilibriumMeasureconditionalProbabilityCalculationfundamentalConditionalProbabilityequalTimeStatisticsSetupsimultaneousProductWaveempiricalTestSetupequalTimeIndependenceCalculationweakLawCalculationempiricalFrequencyCalculationequalTimeEmpiricalStatisticstypicalitySetuptypicalityCalculationtypicalityBridgetypicalSingleWorldStatisticstimeCollectionSetupperTimeTypicalityInputstimeCollectionResultrandomSystemSelectionrandomSystemSetuprandomSystemConditionalCalculationselectedWaveNonrandompriorRecordsRetainedmultitimeStatisticsCalculationrandomSystemMultitimeStatisticsinformationEnvironmentGroundedabsoluteUncertaintyBridgeactualConfigurationabsoluteUncertaintyscopeAssessmentqualifiedPaperConclusion
Claim identifiers (44)
guidedSetupguidanceCalculationguidedResultinitialDensityAgreementensembleContinuityCalculationwaveCurrentCalculationcurrentVelocitySubstitutioncommonContinuityCalculationequivarianceSetupequivarianceCalculationequivarianceResultsubsystemSetupsubsystemCalculationsubsystemResultuniversalMeasureconditionalCalculationconditionalResultequalTimeSetupproductWaveempiricalTestsindependenceCalculationweakLawfrequencyCalculationequalTimeResulttypicalitySetuptypicalityCalculationtypicalityBridgetypicalityResulttimeCollectionSetupperTimeInputstimeCollectionResultrandomSelectionrandomSetuprandomCalculationselectedWavepriorRecordsmultitimeCalculationmultitimeResultinformationGroundinguncertaintyBridgeactualConfigurationuncertaintyResultscopequalifiedConclusion
Step identifiers (44)
stateGuidedSetupsupplyGuidanceCalculationderiveGuidedResultstateInitialDensityAgreementsupplyEnsembleContinuityCalculationsupplyWaveCurrentContinuityCalculationsupplyCurrentVelocitySubstitutionCalculationsupplyCommonContinuityCalculationderiveEquivarianceSetupsupplyEquivarianceCalculationderiveEquivarianceResultstateSubsystemSetupsupplySubsystemCalculationderiveSubsystemResultstateUniversalMeasuresupplyConditionalCalculationderiveConditionalResultstateProductWavestateEmpiricalTestsderiveEqualTimeSetupsupplyIndependenceCalculationsupplyWeakLawsupplyFrequencyCalculationderiveEqualTimeResultstateTypicalitySetupsupplyTypicalityCalculationstateTypicalityBridgederiveTypicalityResultstateTimeCollectionSetupsupplyPerTimeInputsderiveTimeCollectionResultstateRandomSelectionderiveRandomSetupsupplyRandomCalculationstateSelectedWavestatePriorRecordssupplyMultitimeCalculationderiveMultitimeResultstateInformationGroundingstateUncertaintyBridgestateActualConfigurationderiveUncertaintyResultstateScopeassembleQualifiedConclusion
Route identifiers (10)
guidedDynamicsdensityEquivariancesubsystemWaveconditionalProbabilityequalTimeStatisticstypicalSingleWorldStatisticscommonMeasureTimeCollectionrandomSystemMultitimeabsoluteUncertaintypaperScope
Route kinds (10)
symmetrySelectedGuidedDynamicscontinuityEquationEquivarianceeffectiveAndConditionalSubsystemWaveuniversalToSubsystemConditionalProbabilitysingleWorldEmpiricalFrequencyquantumEquilibriumTypicalitycommonInitialMeasureTimeTypicalityenvironmentSelectedMultitimeExperimentenvironmentGroundedKnowledgeLimitationtypicalityAndNonrelativisticScope
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.
guidedDynamics
Logical kind: symmetrySelectedGuidedDynamics.
Required predecessor routes: none.
Ordered inference steps: stateGuidedSetup, supplyGuidanceCalculation, deriveGuidedResult.
Exported conclusions: guidedResult.
densityEquivariance
Logical kind: continuityEquationEquivariance.
Required predecessor routes: guidedDynamics.
Ordered inference steps: stateInitialDensityAgreement, supplyEnsembleContinuityCalculation, supplyWaveCurrentContinuityCalculation, supplyCurrentVelocitySubstitutionCalculation, supplyCommonContinuityCalculation, deriveEquivarianceSetup, supplyEquivarianceCalculation, deriveEquivarianceResult.
Exported conclusions: equivarianceResult.
subsystemWave
Logical kind: effectiveAndConditionalSubsystemWave.
Required predecessor routes: none.
Ordered inference steps: stateSubsystemSetup, supplySubsystemCalculation, deriveSubsystemResult.
Exported conclusions: subsystemResult.
conditionalProbability
Logical kind: universalToSubsystemConditionalProbability.
Required predecessor routes: densityEquivariance, subsystemWave.
Ordered inference steps: stateUniversalMeasure, supplyConditionalCalculation, deriveConditionalResult.
Exported conclusions: conditionalResult.
equalTimeStatistics
Logical kind: singleWorldEmpiricalFrequency.
Required predecessor routes: conditionalProbability.
Ordered inference steps: stateProductWave, stateEmpiricalTests, deriveEqualTimeSetup, supplyIndependenceCalculation, supplyWeakLaw, supplyFrequencyCalculation, deriveEqualTimeResult.
Exported conclusions: equalTimeResult.
typicalSingleWorldStatistics
Logical kind: quantumEquilibriumTypicality.
Required predecessor routes: equalTimeStatistics.
Ordered inference steps: stateTypicalitySetup, supplyTypicalityCalculation, stateTypicalityBridge, deriveTypicalityResult.
Exported conclusions: typicalityResult.
commonMeasureTimeCollection
Logical kind: commonInitialMeasureTimeTypicality.
Required predecessor routes: none.
Ordered inference steps: stateTimeCollectionSetup, supplyPerTimeInputs, deriveTimeCollectionResult.
Exported conclusions: timeCollectionResult.
randomSystemMultitime
Logical kind: environmentSelectedMultitimeExperiment.
Required predecessor routes: conditionalProbability.
Ordered inference steps: stateRandomSelection, deriveRandomSetup, supplyRandomCalculation, stateSelectedWave, statePriorRecords, supplyMultitimeCalculation, deriveMultitimeResult.
Exported conclusions: multitimeResult.
absoluteUncertainty
Logical kind: environmentGroundedKnowledgeLimitation.
Required predecessor routes: conditionalProbability.
Ordered inference steps: stateInformationGrounding, stateUncertaintyBridge, stateActualConfiguration, deriveUncertaintyResult.
Exported conclusions: uncertaintyResult.
paperScope
Logical kind: typicalityAndNonrelativisticScope.
Required predecessor routes: guidedDynamics, densityEquivariance, conditionalProbability, equalTimeStatistics, typicalSingleWorldStatistics, randomSystemMultitime, absoluteUncertainty.
Ordered inference steps: stateScope, assembleQualifiedConclusion.
Exported conclusions: qualifiedConclusion.