Formal reconstruction · Quantum foundations
A Suggested Interpretation of the Quantum Theory in Terms of “Hidden” Variables
The logical anatomy of polar Schrödinger dynamics, added configuration guidance, effective collapse, equilibrium statistics, contextual observables, nonlocality, and deterministic completion
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
- structurePart II's separated apparatus packets, actual occupancy, and Born weights.
- structurePart II's apparatus-dependent contexts evade a system-only value assignment.
- structureThe original EPR position/momentum correlations and unchanged signal marginal.
- structurePart I's actual configuration, phase-gradient momentum, and guided motion.
- inductiveBohm's continuity-equation route to equilibrium preservation.
- structureThe stationary `s`-state has zero particle motion but nonzero total energy.
- structure
- structure
- structurePaper-local semantic vocabulary. The structure contains physical data and relations, never proofs of the paper's unresolved calculations.
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- structureRelations needed to ask whether an indicated value reveals a value possessed by the system before the selected measurement run.
- structurePhysical outcome support is meaningful without choosing whether a state is a complete ontic description.
- structure
- structure
- structureA probability distribution assigned to a statistical population.
- structureA theory- or model-indexed numerical prediction for an event.
- structurePredictions made by descriptions in regimes. `predicts` is relational so the signature can represent deterministic values, sets of allowed values, or probabilistic outputs without choosing among them.
- structure
Definitions and domain choices
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- 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
- definitionImmediate predecessor routes. Claims established by their transitive predecessors are inherited by the dependency closure.
- definition
- definition
- definition
- definition
- definition
- definitionTemporary reductio-introduction steps discharged by this inference. Discharge removes only those exact origins from the conclusion's epistemic basis; it does not assert the temporary hypotheses globally.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA source-mapped claim holds when its declared formula evaluates under the given paper-local semantic interpretation.
- definition
- definition
- definition
- definition
- definitionEvery claim in the supplied identifier list holds.
- definitionA source-mapped step is semantically sound when the interpreted premises imply the interpreted conclusion. Physical principles and imported calculations therefore remain explicit hypotheses of paper-specific certificates rather than acquiring truth from their source-map labels. A reductio hypothesis is different: it introduces a temporary assumption into a subargument and therefore is not required to hold globally. Its later uses remain ordinary premise-sensitive steps, and discharging it into a negated conclusion remains an ordinary semantic obligation.
- definitionEvery step in the supplied identifier list is semantically sound.
- definition
- definition
- definition
- definition
- definition
- definitionThe formula declared for a claim identifier, when that claim is present.
- definition
- definitionEvery source-mapped step whose justification contributes to the claim through declared premise-to-conclusion steps.
- definitionAll justification statuses contributed by the exact source-mapped origins of a claim. This records epistemic provenance; it does not assert any paper claim or discharge any physical assumption.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe declared argument step with the requested identifier, when present.
- definition
- definitionThe premise list and conclusion attached to a declared step identifier.
- definition
- definition
- definition
- definition
- definitionThe complete Lean-side fidelity certificate. The first conjunct is computed from source-map data; the second is supplied by checked route semantics; the third requires each declared independence boundary to have a countermodel.
- definition
- definition
- definition
- definition
- definitionA typed countermodel matrix avoids string-keyed audit rows. Each index selects one proposition-valued separation obligation.
- definition
- definitionEvery route actually declared in the source map has a semantic certificate under the paper-local interpretation.
- definition
- definition
- definitionOne countermodel row retains a weaker proposition while rejecting a stronger upgrade. This is a proposition, not a structure carrying proof fields.
- definition
- definition
- definitionIndependent dependency and epistemic ledgers must review the same actual source claims, including every public conclusion and the selected paper conclusion. Empty, duplicated, nonexistent, or one-sided entries are invalid.
- definitionEvery actually declared source route must have exactly one independently reviewed predecessor row. Correct rows for a selected subset are insufficient.
- definitionThe declared main conclusion must be exposed by at least one public route output, rather than existing only as an unexported source-map claim.
- definition
- definition
- definitionTwo finite lists describe the same dependency set. Duplicate expected entries are rejected so a ledger cannot pass by repeating a label.
- definitionEvery paper-level, claim-level, and step-level source reference is present and has a nonempty work and locator. PaperArgument.auditable separately checks that every claim and step carries at least one source.
- definitionA source reference is usable for review only when both the work and its locator are nonempty.
- definitionStatic fidelity checks that can be evaluated from a paper's source map alone. They do not assert the truth of any physical premise.
- definitionEvery declared output of a named source route holds under the semantic interpretation. This is the proof obligation discharged by paper-specific Lean theorems.
- definition
- definitionA route is fully certified only when both its individual steps and its declared outputs are semantically checked.
- definitionEvery source-mapped inference step in a named route is semantically sound.
- definitionEvery route named in the supplied identifier list is semantically certified.
- definition
- definition
- definition
- definition
- definition
- definitionThe source-mapped route with the requested identifier, when present.
- definition
- definitionThe public semantic interface inherited from predecessor routes. Descendants receive only declared route outputs, not every internal intermediate claim. Outputs still carrying a temporary reductio origin are excluded.
- definitionAll direct and inherited route dependencies. The route-order check separately ensures that the declared graph is acyclic and topologically ordered.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA differentiable phase with continuous but non-Lipschitz guidance at zero.
- definition
- definition
- definition
- definitionA uniform spatial Lipschitz bound on the selected time interval and chart.
- definitionThe coordinate decoder is required only along the actual history.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe analytic flow input is distinct from common pushforward transport.
- definitionActual initial configurations follow the very current used by the Born law.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionEquations (5) and (7) identify the two continuity evolutions.
- definition
- definition
- definition
- definitionRegular coordinate realization of the same selected wave, amplitude and phase. No continuity equation or Born-current conclusion is assumed here.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- 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 real parameter is the same clock used by the polar fields and endpoint map.
- definition
- definitionEvery selected-state successor represents an admissible solution, and every such solution is represented.
- definitionThe guidance postulate transports an ensemble density by the particle-current continuity equation. This is distinct from the wave-density equation obtained from polar decomposition.
- definition
- definitionPart I p. 171: the actual initial ensemble law equals the initial Born law.
- definition
- definition
- definition
- definition
- definition
- definitionPart I, equations (1)-(8): the polar decomposition of a Schrödinger solution produces a continuity equation and a Hamilton-Jacobi-like equation containing the quantum potential. This is a mathematical calculation, not yet the postulate that a particle occupies an actual configuration.
- definition
- definitionPhysical Review 85 (1952), p. 170, equations (5), (6), and the `R` form of equation (8). Bohm first writes `P = R^2`, identifies the probability-current components as `P grad S / m`, obtains the continuity equation, rewrites the Hamilton-Jacobi equation with the quantum potential, and gives `U = -(hbar^2 / 2m) (nabla^2 R / R)`. Derivatives, currents and the amplitude Laplacian are computed from actual coordinate fields. The open regular polar chart and its physical-coordinate calibration are explicit, with no extension through wave-function nodes.
- definition
- definition
- definition
- definition
- definitionApparatus occupancy refers to the apparatus's own hidden configuration.
- definitionRecorded momentum is contextual and need not equal actual initial momentum.
- definitionThe EPR argument combines its printed correlations with no-signalling.
- definitionThe selected actual momentum and configuration obey the printed guidance law.
- definitionThe stationary example retains its selected momentum and force balance.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionRaw Part I source chain. It contains neither an assembled equivariance setup nor any shared endpoint or explanation.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionContinuity of the selected physical coordinate history, not an assigned predicate.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA smooth stationary wave with a nodal plane; no global normalization is claimed.
- definitionA local Born-current result. It does not assert total probability one.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionOne forward continuation exists and every continuation from the same selected state and time is that continuation. This is nonvacuous, unlike uniqueness alone.
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA completion whose deterministic dynamics governs an actual system.
- definitionUniversal completion clauses, possibly vacuous over physical systems.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionSubstantive descriptive completeness: the selected regime contains at least one physically admissible element, and the description represents every such element. The coverage law alone may hold vacuously on an empty domain.
- definition
- definition
- definition
- definition
- definitionA concrete mathematical assignment whose state, quantity, and value all have the selected representation relations. This proposition deliberately stops before asserting that the physical quantity possesses the represented value.
- definition
- definitionActive unfaithfulness is a complete represented assignment whose represented physical value is absent from the physical state. It is stronger than merely negating `FaithfullyRepresentsAt`, which can also fail for lack of any value- bearing representation instance.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionActive unfaithfulness is witnessed by a recorded value absent from the premeasurement state, rather than by the mere absence of a faithful run.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionForget a supplied completeness classification without replacing it by false.
- definition
- definition
- definition
- definition
- definitionA selected observable sector.
- definitionTwo descriptions share at least one prediction in the selected sector.
- definitionEmpirical equivalence combines exact predictive agreement with a concrete observable and value predicted by both descriptions. The witness prevents an empty sector or two predictionless descriptions from establishing empirical equivalence.
- definitionExtensional agreement of two prediction relations on a selected sector. This low-level relation may hold vacuously when the sector or both prediction relations are empty; `EmpiricallyEquivalent` adds a common prediction.
- 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
Source mappings and interpretation choices
- inductive
- definition
- instance
- 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
- 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
- constructor
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- 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
- definition
- 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
- 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
- definition
- definition
- constructor
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- 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
- definition
- definition
- 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
- 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
- definition
- definition
- checked statement
- definition
- definition
- definition
- definition
- definition
- checked statement
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- definition
- inductive
- definition
- instance
- 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
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- definition
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- definition
- structure
- definition
- instance
- checked statement
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- constructor
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- checked statement
- recursor
- definition
- checked statement**Alias** of `PhysicsLogic.Papers.Bohm1952.SemanticContext.all_routes_are_semantically_realizable`.
- checked statement
- inductive
- definition
- instance
- definition
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- 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
- definition
- definition
- checked statement
- checked statement
- definition
- definition
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- checked statement
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- checked statement
- definition
- definition
- checked statement
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- 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 statementPart I p. 171 reaches the model-native stopping point: the selected ensemble starts with the wave density, both densities follow the selected common flow, and the later density agreement is retained. This does not add the separate Part II relaxation expectation.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
Axioms and trust boundaries
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- 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
- recursor
- constructor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
External mathematical declarations
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- 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 Bohm1952.lean,
SourceMap.lean, and Coverage.lean. The article
keeps mathematical consequences of the Schrödinger equation separate from
Bohm’s added physical postulates, exactly as the Lean architecture does.
Its named calculation contracts are independent hypotheses; only their
result steps apply the selected local inputs to obtain conclusions.
Those steps reconstruct their physics from checked premise maps; they
do not extract witnesses from completed route certificates.
The two papers are a network of independent calculations around one added ontology
The polar Schrödinger route provides a continuity equation and modified Hamilton–Jacobi equation. The guidance route adds actual configuration and deterministic dynamics. The other paper-local calculations record one-particle examples, many-body transitions, apparatus packets, equilibrium statistics, contextual observables, EPR analysis, and the radiation field without claiming that page order has already supplied their premises. Only the final completion assessment inherits the certified deterministic-motion output of the guidance route, and its completion step reconstructs that proposition from the checked premise map before extracting forward determinism. The formalization never treats the continuity equation as if it had already postulated a particle.
| Transition | Status | Retained qualification |
|---|---|---|
| Polar Schrödinger decomposition | mathematical paper derivation | It supplies equations, not an actual configuration. |
| Configuration and guidance | added physical postulates | The ontology and guidance law are not derived from continuity. |
| Trajectory existence/uniqueness | imported result | Integration of the guidance field is an explicit calculation input. |
| Packet, contextual, and EPR conclusions | calculation + interpretation | Each retains its apparatus, branch, equilibrium, and configuration-space premises. |
| Equilibrium relaxation | author expectation | Equivariance is proved locally; arbitrary relaxation is not. |
| Radiation-field calculation | deferred calculation | The field-mode output is supplied as a named hypothesis. |
| Completion and empirical scope | interpretive conclusion | Added postulates, sector-relative equivalence, and open extensions remain visible. |
The Schrödinger equation supplies a flow; Bohm separately postulates what flows
The mathematical setup assumes a one-particle wave obeying the Schrödinger equation in the atomic regime, a polar decomposition into selected amplitude and phase, and the identity of the selected density with the wave density.
∂tP + div(P∇S/m) = 0,
∂tS + |∇S|²/(2m) + V + U = 0,
U = −(ℏ²/2m)(∇²R/R). the typed bundle uses actual coordinate derivatives, currents and amplitude Laplacians on an open, nonempty polar region with R ≠ 0; chart calibration, regularity and the same-wave polar representation remain explicit inputs (1)
The setup and supplied separation calculation yield the quantum-potential identity, modified Hamilton–Jacobi equation, wave-density continuity equation, and PrintedPolarReductionFormulaBundle. The formula is projected by polar_decomposition_calculation_retains_printed_equations_five_six_and_eight before the result consumes it; named_polar_reduction_does_not_supply_printed_equations blocks a name-only replacement.
schrodinger_polar_decomposition_yields_continuity_and_quantum_hamilton_jacobi · Part I p. 170, equations (1)–(8)
Added configuration and guidance
The second route begins with a genuinely new source-level physical premise: the electron has an actual configuration at the initial time; its momentum obeys p = ∇S and its velocity is v = ∇S/m; the quantum potential acts on the electron at its configuration; and the complete state is the selected wave together with that configuration.
The calculation supplies an actual phase-gradient initial-value solution, a uniform spatial Lipschitz bound on the selected interval, and calibrated clock and state representation. Coordinate continuity and uniqueness among all admissible trajectories are derived. The successor state decodes to the configuration of the same guidance map used by probability transport. Universal forward determinism is a separate explicit premise, not inferred from this interval result.
The distinction is substantive: the differentiable phase with gradient 2 sqrt(|q|) admits q=0 and q=t^2 from the same initial position on [0,1], but its velocity fails the Lipschitz condition. This control does not assert the full Schrodinger/polar equations. Likewise, the encoding q to q^2 can have a unique encoded successor while erasing the sign of the physical configuration; the required state decoder excludes that identification.
trajectory_inputs_determine_the_actual_state · lipschitz_guidance_has_one_actual_history · certified_guidance_route_retains_actual_selected_trajectory
The admissible configuration element absent from the wave-only representation witnesses incompleteness. The supplemented description separately covers an inhabited admissible domain, and the generic descriptive-completeness theorem therefore excludes completeness of the wave-only description in the atomic regime. No determinism or empirical equivalence is used in this conclusion.
completion_setup_realizes_descriptive_completeness_transition · Part I pp. 166–169
Configuration/guidance postulates plus the supplied trajectory calculation establish a forward-deterministic continuous trajectory and retain the mass-normalized source guidance law.
added_configuration_guidance_and_uniqueness_yield_deterministic_continuous_motion · guidance_postulates_retain_printed_phase_gradient_and_mass · Part I pp. 166, 170–171
The ontology is not hidden in the algebra
continuity_equation_does_not_supply_an_actual_configuration
is the formal boundary: a density continuity equation can be derived
while the assertion of an actual configuration remains absent.
Stationary energy and two-slit interference separate particle motion from wave effects
Real stationary spatial wave
For the selected stationary state with a real spatial wave, the supplied calculation sets the particle momentum to zero and the particle at rest. Its particle kinetic energy vanishes and the classical and quantum forces balance. A nonzero total energy need not be particle motion; stationarity does not fix the sign or zero of that energy.
A normalized stationary-wave test
A(x)=sqrt(1/sqrt(pi))*exp(-x^2/2); psi_t(x)=A(x)*exp(-i*t/2).
i*d_t psi=-(1/2)*d_xx psi+V*psi; nu_t=N(0,1/2).
v=Im(d_x psi/psi)=0; E=-d_t phase=1/2.
Q=-A''/(2*A)=(1-x^2)/2; -V'-Q'=0. The same actual wave supplies the Born law, derivatives, guidance, energy, and quantum potential. At x=0, Q=1/2 is nonzero. This is a constructed control, not an extra calculation attributed to Bohm. (3a)
the_actual_wave_is_an_energy_eigenstate · the_quantum_potential_uses_the_same_actual_wave_amplitude · the_actual_classical_and_quantum_forces_balance
nu_C(t)=nu_t; v_C(t,x)=0; E_C(t)=E(t)+C.
C=-1 gives E_C=-1/2 with normalized stationary rest. The shifted wave solves the actual shifted Schrodinger equation. This is the constant-potential freedom of the nonrelativistic fixed-particle model, not a claim about gravitational vacuum energy. (3b)
normalized_stationary_rest_does_not_require_positive_total_energy · stationary_example_retains_zero_velocity_and_kinetic_energy
Two-slit wave and actual passage
In the two-slit setup the electron has an actual configuration. The calculation gives it a definite slit passage but denies that this passage is predictable. Meanwhile the wave produces the interference pattern and mediates dependence on the slit arrangement.
The two supplied calculations jointly establish the stationary energy/force balance and interference conclusions without mistaking nonzero energy for particle motion.
stationary_and_two_slit_examples_separate_actual_motion_from_wave_effects · stationary_example_retains_zero_velocity_and_kinetic_energy · Part I pp. 173–174
Configuration-space dynamics supplies nonlocal dependence and selects one quantized transition packet
The many-body setup contains a configuration-space wave and its guidance relation. Its calculation says that local motion depends on remote configuration and that the wave mediates an effective many-body interaction.
A second subroute starts with an interacting wave whose asymptotic packets separate, an actual configuration occupying one selected branch, and a correlation between that branch and an outcome. The calculation gives quantized transfer in the selected branch, makes the unoccupied branches dynamically irrelevant, and equates the ensemble probability of the selected outcome with its wave weight.
Pensemble(outcome) = weightψ(outcome). standard transition probability retained alongside definite branch occupancy (6)
The configuration-space and transition-packet calculations establish nonlocal dependence, effective interaction, selected quantized transfer, branch irrelevance, and the standard weight equality.
configuration_space_dynamics_and_packet_selection_explain_correlated_quantized_transitions · Part I pp. 174–177
Nonoverlapping apparatus packets yield effective collapse without fundamental wave collapse
The measurement interaction correlates branches of the wave with apparatus packets. Those packets do not overlap, exactly one actual apparatus configuration lies in one selected branch, and that branch correlates with a definite outcome while both wave branches retain their nonzero squared-coefficient probabilities.
unoccupied branches dynamically irrelevant, no fundamental collapse,
one actual outcome; Pleft = |cleft|², Pright = |cright|². both Born weights can remain nonzero without ontically multiple outcomes (7)
The apparatus-packet setup and calculation establish one actual occupied outcome, both explicit Born weights, definite record, occupied effective wave, unoccupied-branch irrelevance, and absence of fundamental collapse.
nonoverlapping_apparatus_packets_and_actual_configuration_yield_effective_collapse · apparatus_measurement_retains_one_actual_outcome_and_born_weights · Part II pp. 181–182, equations (8)–(11)
Effective is not fundamental
The countermodel effective_branch_selection_does_not_require_fundamental_collapse
records exactly this distinction. Branch separation and actual
occupancy can make one packet effective while the total wave does not
undergo a fundamental collapse.
Equivariance preserves quantum equilibrium; it does not prove arbitrary relaxation into it
The equilibrium setup assumes equality of the initial ensemble and Born measures. The calculation supplies their common configuration transport and the state/density regularity; it no longer supplies the desired later equality. The shared theorem derives that equality.
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. (8a)
The source ensemble-density representative is nonnegative and a.e. measurable. The original wave-density readout is calibrated to the squared complex wave at both endpoints. Common transport preserves probability normalization; later measurability then gives square integrability. Constructing this transport from the source continuity and guidance equations remains an explicit analytic input.
the_actual_guided_ensemble_realizes_nonvacuous_born_equivariance · actual_configuration_transport_derives_later_density_agreement · actual_equivariance_retains_the_source_density_calibration
The same transport map must also solve the phase-gradient guidance equation on a nonzero real-time interval, for almost every initial Born configuration. Its initial value, coordinate decoder, and clock are calibrated to the physical configuration and source fields. Positive density on the regular node-free chart then identifies each actual trajectory derivative with j/rho. Initial ensemble agreement transfers this almost-everywhere statement to the actual ensemble; the certified equilibrium conclusion retains it.
Endpoint pushforwards alone are insufficient: the path q(t)=q(0)+t(1-t) returns every configuration at t=1 and preserves a normalized stationary Gaussian at the endpoints, but violates zero phase-gradient guidance in between. An independent normalized moving Gaussian tests actual phase-derived motion and transport; it is a kinematic test, not an asserted free Schrodinger solution. Existence, uniqueness, global node avoidance, and the analytic derivation of measure transport from continuity remain separate obligations.
actual_equivariance_uses_the_phase_gradient_guidance_flow · certified_equilibrium_route_retains_actual_guidance · correct_born_pushforwards_do_not_establish_guidance
This route is also adapted to the shared guided-density framework. The local setup and calculation establish the direct nonvacuous proposition requiring initial agreement, common evolution, and later agreement together. That direct output reconstructs every shared equivariance claim. The adapter grounds only the selected pre-output setup in a framework-as-theory and an explicit world record; it does not assume the propagation calculation or later agreement.
bohm_route_realizes_shared_guided_density_equivariance · bohm_route_exhibits_nonvacuous_shared_guided_density_equivariance · grounded_bohm_equivariance_transfers_every_shared_claim
bohm_source_inputs_establish_equivariance_setup_and_calculation
derives the setup from polar continuity, guidance, ensemble
continuity, and their common-flow calculation.
bohm_source_inputs_make_shared_equivariance_route_applicable
then enters the shared route. The conclusions
bohm_source_inputs_realize_structural_guided_density_equivariance_explanation
and
bohm_source_inputs_realize_source_structural_guided_density_equivariance_explanation
distinguish the mechanism-neutral explanation from the one retaining
Bohm's typed derivation.
Relaxation remains an expectation
A separate assessment says relaxation toward wave density is expected but explicitly denies that a detailed proof has been supplied. The qualified theorem conjoins this expectation with the proved preservation result; it does not infer relaxation from equivariance.
The common-flow calculation preserves the equilibrium density, while the author assessment keeps general relaxation plausible but unproved.
equilibrium_is_preserved_while_general_relaxation_remains_an_expectation · Part I p. 171; Part II pp. 185–186, with the explicit proof disclaimer on p. 186
Preservation is not convergence
The actual stationary oscillator preserves its Born ensemble, while a displaced Gaussian follows the same zero-velocity flow without ever acquiring exact Born equilibrium. The earlier scalar history remains a formula-level illustration; the fidelity boundary now uses actual normalized waves, dynamics, and probability measures.
mu_t=nu_t if and only if mu_s=nu_s.
In the stationary control, nu_t=N(0,1/2), mu_t=N(1,1/2), and Phi_s,t=id. This excludes finite-time exact fine-grained equilibration in the selected flow. It does not rule out weak, asymptotic, or coarse-grained relaxation, modified dynamics, or Bohm's proposed chaotic macroscopic mechanism. Forward equivariance does not assume a global inverse through nodes. (8b)
the_actual_displaced_ensemble_never_reaches_exact_born_equilibrium
Measured observables are apparatus-contextual, while EPR influence is nonlocal but nonsignalling in equilibrium
A standard momentum measurement need not reveal prior momentum
In the selected run, the standard procedure produces a record indicating a measured value for the momentum quantity. The calculation nevertheless assigns a different actual premeasurement momentum value, denies that the measured value was the premeasurement value, says the procedure transforms the wave, and makes the apparatus context affect the outcome. Position and momentum apparatuses also carry distinct hidden configurations and distinct context-dependent hidden-variable distributions.
ρposition apparatus ≠ ρmomentum apparatus. therefore this indicated run actively misreports the premeasurement particle momentum (9)
The measurement run and supplied calculation establish the actual value, its mismatch with the record, a positive witness of active unfaithfulness, wave transformation, and apparatus dependence. The conclusion cannot hold merely because no run occurred.
standard_momentum_observable_need_not_reveal_premeasurement_particle_momentum · contextual_measurement_retains_distinct_apparatus_distributions · Part II pp. 183–184
EPR-correlated configuration-space wave
The EPR setup is both correlated and many-body in configuration space, retaining x₁ − x₂ = a and p₁ + p₂ = 0. The calculation says a distant measurement choice changes conditional motion and transmits an instantaneous configuration-space influence. In quantum equilibrium it simultaneously denies a controllable signal and retains the standard relativistically consistent predictions.
x₁ − x₂ = a, p₁ + p₂ = 0, remote momentum changes,
quantum equilibrium ⇒ unchanged remote operational marginal + no controllable signal. nonlocal influence and operational no-signalling are distinct claims (10)
The EPR setup and calculation establish distant conditional change, instantaneous influence, absence of an equilibrium signal, and relativistic consistency of standard predictions.
epr_route_is_nonlocal_but_not_a_controllable_signal_in_quantum_equilibrium · epr_analysis_retains_equal_marginal_and_remote_motion_change · Part II pp. 186–187
The countermodel instantaneous_configuration_influence_does_not_itself_supply_a_signal
prevents the first half of this conjunction from being substituted for
the second.
Actual field-mode configurations extend packet selection to radiation quanta
Appendix A supplies a radiation mode with an actual configuration and a radiation super-wave functional. The field calculation is explicitly classified as deferred in the source map.
separated photoelectric and Compton packets ⇒ quantized energy transfer + standard probabilities. the exact Appendix A calculation is a supplied proposition-valued input (11)
The field setup and supplied calculation establish quantum-potential modification, packet separation, quantized transfer, and standard photoelectric and Compton probabilities.
field_configuration_and_superwave_extend_packet_logic_to_radiation_quanta · Part II Appendix A, pp. 189–191
The completion is deterministic at the individual level and probabilistic at the predictive and ensemble levels
The completion setup selects an observable sector. It states that actual configuration is physically admissible but absent from the wave-only representation, that a configuration supplement extends the wave-only description to a completed description, that the result is complete in the atomic regime, that the selected dynamics governs physical systems, that the selected electron is an actual physical system, and that the completed and wave-only descriptions are empirically equivalent in the selected sector.
The completion setup and forward determinism establish a configuration-supplemented, complete, deterministic, empirically equivalent description whose dynamics governs the selected physical electron. The corresponding universal law alone is kept distinct because it can hold over an empty physical-system scope.
paper_realizes_supplemented_deterministic_completion · Part I p. 166; Part II pp. 180, 188
Predictive branching without ontic branching
The wave-only description gives positive weight to two distinct outcomes. A separate determinacy premise says every physically possible outcome of the actual state equals the selected outcome. Lean then proves that the description branches predictively while the physical state does not branch ontically.
With standard statistics and agreement between ensemble probability and wave weight, a further theorem keeps three roles distinct: predictive probability, ensemble probability, and ontic possibility. The first two may share the same numerical weight while the third remains unbranched.
probabilistic_predictions_coexist_with_a_determinate_individual_outcome · standard_statistics_and_hidden_configuration_keep_probability_roles_distinct
Qualified empirical and extension scope
The paper scope says standard quantum theory applies in the atomic regime and the interpretations are not experimentally distinguishable there. A short-distance modification is proposed but not established, and no relativistic completion is supplied in the encoded short-distance regime. Thus empirical equivalence is local to the domain where current quantum theory applies; proposed departures remain speculative.
The scope assessment is projected unchanged into the five-part qualified conclusion.
empirical_equivalence_is_atomic_regime_scoped_and_short_distance_extensions_remain_speculative · Part I p. 179; Part II pp. 187–188
Concept guide
Terms linked throughout the article resolve to these paper-local definitions and conclusions.
Polar Schrödinger reduction
The amplitude–phase decomposition yielding a typed p. 170 regular-region bundle for P = R², current continuity, the quantum-potential-modified Hamilton–Jacobi equation, and U = −(ℏ²/2m)(∇²R/R).
PolarDecompositionCalculation
Configuration guidance
The added actual configuration, phase momentum, quantum-potential action, and complete wave-plus-configuration state.
ConfigurationGuidancePostulates
Deterministic continuous motion
Actual guidance trajectories and decoded physical successor states, with interval uniqueness derived from an explicit Lipschitz condition and universal determinism kept as a separate premise.
TrajectoryExistenceUniquenessCalculation
Quantum potential
The amplitude-defined additional potential in the Hamilton–Jacobi equation, asserted to act on the actual configuration.
quantumPotentialIdentity
Configuration-space nonlocality
Dependence of local motion on remote coordinates through the many-body configuration-space wave.
ManyBodyCalculation
Packet selection
Actual configuration occupies one separated branch, making unoccupied branches dynamically irrelevant for the selected outcome.
TransitionPacketCalculation
Effective collapse
A definite occupied apparatus packet and effective wave without fundamental collapse of the total wave.
MeasurementPacketCalculation
Guided-density equivariance
Preservation of equality between ensemble density and wave density when both follow the same guided continuity flow.
EquivarianceCalculation
Relaxation expectation
The expectation that nonequilibrium approaches wave density, paired with the explicit absence of a detailed proof.
RelaxationAssessment
Contextual observable
An actual indicated measurement outcome shaped by wave transformation and apparatus context, together with a complete mathematical state, quantity, assignment, and value representation whose physical value is witnessed to be absent from the premeasurement particle quantity.
ContextualObservableCalculation
EPR influence without signal
Instantaneous configuration-space influence with no controllable signal in quantum equilibrium.
EPRCalculation
Radiation-field extension
Actual field-mode configuration and super-wave packet logic for quantized photoelectric and Compton transfers.
RadiationFieldCalculation
Supplemented completion
A configuration-extended deterministic description complete and empirically equivalent in a selected atomic observable sector.
CompletionSetup
Distinct probability roles
Numerically aligned predictive and ensemble probabilities alongside one determinate, nonbranching physical outcome.
DistinctProbabilityRoleResult
Qualified empirical scope
Atomic-regime equivalence with unestablished short-distance modification and no supplied relativistic completion.
PaperScopeAssessment
Route inventory and formal provenance
The source map declares ten routes and forty-one semantic atoms. Coverage interprets every atom and provides a realization theorem for every route from twenty-seven raw paper-local inputs rather than assumed route certificates.
| Route | Declared dependencies | Principal output | Profile |
|---|---|---|---|
| Schrödinger decomposition | — | Continuity and quantum Hamilton–Jacobi equations | mathematical derivation |
| Configuration guidance | — | Deterministic continuous motion | added postulates + imported calculation |
| One-particle examples | — | Stationary-state and two-slit conclusions | paper calculations |
| Many-body transitions | — | Nonlocal dependence and quantized packet transition | configuration-space and scattering calculations |
| Measurement packets | — | Effective collapse without fundamental collapse | apparatus-packet calculation |
| Equilibrium statistics | — | Equivariance and qualified relaxation | derivation + author expectation |
| Contextual observables | — | Contextual momentum conclusion | measurement interpretation |
| EPR nonlocality | — | Influence without equilibrium signal | configuration-space interpretation |
| Radiation field | — | Quantized radiation transfer and probabilities | deferred field calculation |
| Completion and scope | Configuration guidance | Completion, statistical determinism, qualified scope | interpretive synthesis + open obligations |
Schrödinger route · schrodinger_decomposition_route_is_semantically_realized
Guidance route · configuration_guidance_route_is_semantically_realized
Examples route · one_particle_examples_route_is_semantically_realized
Many-body route · many_body_transitions_route_is_semantically_realized
Measurement route · measurement_packets_route_is_semantically_realized
Equilibrium route · equilibrium_statistics_route_is_semantically_realized
Contextual route · contextual_observables_route_is_semantically_realized
EPR route · epr_nonlocality_route_is_semantically_realized
Radiation route · radiation_field_route_is_semantically_realized
Completion route · completion_and_scope_route_is_semantically_realized
Formal non-implications
| Available fact | Conclusion not supplied | Lean witness |
|---|---|---|
| Regular polar sector, Hamilton–Jacobi relation, and quantum potential | The full printed p. 170 system, including continuity | named_polar_reduction_does_not_supply_printed_equations |
| Conserved density | Actual configuration | continuity_equation_does_not_supply_an_actual_configuration |
| Actual normalized stationary dynamics and preserved Born equilibrium | Finite-time exact equilibration of a displaced ensemble | the_actual_displaced_ensemble_never_reaches_exact_born_equilibrium |
| Actual normalized rest after a constant potential shift | A positive total-energy origin | normalized_stationary_rest_does_not_require_positive_total_energy |
| Separated apparatus branches with actual occupancy | Fundamental collapse | effective_branch_selection_does_not_require_fundamental_collapse |
| Instantaneous influence | Controllable signal | instantaneous_configuration_influence_does_not_itself_supply_a_signal |
The equilibrium and stationary-energy boundaries now use actual Gaussian waves and measures. Other controls retain finite source-formula, packet-support, or remote-configuration data; they do not thereby construct a complete microscopic measurement model.
Exhaustive coverage and inherited status
route_semantic_realization_is_exhaustive constructs all
ten route certificates from raw paper-local inputs. Coverage uses
conclusion-only certification only for premise-free source contracts;
every substantive result rebuilds its physics from the exact checked
premise map and contains no route-certificate output extraction.
Dedicated source-map audits retain author-expectation status in
relaxation, deferred-calculation status in the radiation result,
added-physical-postulate ancestry in the completion, and open
short-distance and relativistic obligations in the scope.
Lean-encoded bibliographic record
D. Bohm, A Suggested Interpretation of the Quantum Theory in Terms
of “Hidden” Variables. I, Physical Review 85 (1952), 166–179; and
II, Physical Review 85 (1952), 180–193. All page and equation
locators above are 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 (115)
source_guidance_retains_phase_gradient_momentum_and_velocityphase_gradient_momentum_does_not_supply_mass_normalized_velocitysource_stationary_particle_has_zero_motion_and_positive_energypositive_stationary_energy_does_not_require_particle_motionstationary_rest_does_not_remove_the_quantum_potentialstationary_rest_does_not_supply_classical_quantum_force_balancesource_packets_have_one_actual_outcome_and_two_born_weightsseparated_packets_do_not_select_an_actual_occupied_branchcorrelated_packet_centers_do_not_supply_nonoverlapoccupied_packet_does_not_remove_the_other_wave_branchborn_weighted_branches_do_not_imply_multiple_actual_outcomessquared_wave_weights_do_not_supply_ensemble_probability_agreementsource_contextual_measurement_retains_apparatus_hidden_variablesidentical_system_configuration_does_not_determine_contextual_outcomecontextual_apparatuses_do_not_share_one_hidden_variable_distributiondifferent_apparatus_configurations_do_not_fix_distribution_contextmeasured_momentum_need_not_equal_premeasurement_particle_momentumsource_epr_correlations_change_motion_without_changing_signal_marginalepr_state_correlations_do_not_supply_remote_configuration_influenceunchanged_operational_marginal_does_not_imply_local_particle_motionthe_actual_amplitude_is_positivethe_squared_amplitude_is_the_gaussian_densitythe_actual_wave_has_the_stationary_born_densitythe_actual_wave_is_square_integrablethe_actual_born_measure_is_the_stationary_gaussianthe_amplitude_has_its_actual_derivativethe_amplitude_has_its_actual_second_derivativethe_wave_has_its_actual_spatial_derivativethe_wave_has_its_actual_second_spatial_derivativethe_phase_has_its_actual_derivativethe_wave_has_its_actual_time_derivativethe_actual_phase_has_positive_stationary_energythe_actual_wave_is_an_energy_eigenstatethe_actual_wave_satisfies_schrodinger_evolutionthe_actual_wave_has_no_nodesthe_actual_guidance_velocity_vanishesthe_quantum_potential_uses_the_same_actual_wave_amplitudethe_actual_classical_and_quantum_forces_balancethe_model_born_law_is_the_actual_stationary_wave_lawthe_actual_wave_is_normalizedthe_stationary_trajectories_obey_the_actual_wave_guidancethe_same_stationary_wave_and_flow_realize_the_dynamicsboth_actual_probability_laws_follow_the_stationary_flowactual_equilibrium_requires_the_zero_density_offsetthe_normalized_stationary_wave_has_a_nontrivial_eventthe_actual_stationary_ensemble_has_nonvacuous_born_equivariancethe_actual_displaced_ensemble_never_reaches_exact_born_equilibriumactual_positive_energy_does_not_require_particle_motionactual_stationary_rest_does_not_remove_the_quantum_potentialshifting_the_energy_origin_changes_the_actual_phase_frequencythe_energy_shift_factor_has_unit_moduluschanging_energy_origin_preserves_the_actual_born_measurethe_energy_shifted_wave_is_normalizedthe_energy_shifted_wave_has_its_spatial_derivativethe_energy_shifted_wave_has_its_second_spatial_derivativethe_energy_shifted_wave_has_its_time_derivativethe_energy_shifted_wave_solves_the_shifted_schrodinger_equationthe_energy_shifted_wave_has_no_nodeschanging_energy_origin_preserves_actual_restan_energy_origin_shift_preserves_the_normalized_stationary_dynamicsnormalized_stationary_rest_does_not_require_positive_total_energycoordinate_fields_retain_the_selected_physical_valuespolar_decomposition_calculation_retains_printed_equations_five_six_and_eightprinted_polar_equations_give_actual_born_currentschrodinger_polar_decomposition_yields_continuity_and_quantum_hamilton_jacobitrajectory_inputs_determine_the_actual_stateadded_configuration_guidance_and_uniqueness_yield_deterministic_continuous_motionguidance_postulates_retain_printed_phase_gradient_and_massguidance_data_realize_nonvacuous_unique_forward_evolutionstationary_and_two_slit_examples_separate_actual_motion_from_wave_effectsstationary_example_retains_zero_velocity_and_kinetic_energystationary_example_retains_zero_kinetic_positive_total_energyconfiguration_space_dynamics_and_packet_selection_explain_correlated_quantized_transitionsnonoverlapping_apparatus_packets_and_actual_configuration_yield_effective_collapseapparatus_measurement_retains_one_actual_outcome_and_born_weightsthe_actual_guided_ensemble_realizes_nonvacuous_born_equivarianceactual_equivariance_uses_the_phase_gradient_guidance_flowthe_actual_guided_ensemble_has_born_equivariance_and_current_velocityactual_configuration_transport_derives_later_density_agreementa_realized_source_density_defines_the_actual_born_measureactual_equivariance_retains_the_source_density_calibrationbohm_source_inputs_establish_equivariance_setup_and_calculationguided_density_equivariance_model_retains_paper_semanticsbohm_equivariance_setup_realizes_shared_setupbohm_equivariance_calculation_realizes_shared_calculationbohm_inputs_make_shared_equivariance_route_applicablebohm_source_inputs_make_shared_equivariance_route_applicablebohm_source_inputs_realize_structural_guided_density_equivariance_explanationbohm_source_inputs_realize_source_structural_guided_density_equivariance_explanationbohm_route_realizes_shared_guided_density_equivariancebohm_route_exhibits_nonvacuous_shared_guided_density_equivarianceestablished_bohm_equivariance_realizes_every_shared_claimbohm_guided_density_model_inputs_establish_theory_model_groundingbohm_route_establishes_theory_model_grounded_equivariancegrounded_bohm_equivariance_transfers_every_shared_claimequilibrium_is_preserved_while_general_relaxation_remains_an_expectationstandard_momentum_observable_need_not_reveal_premeasurement_particle_momentumcontextual_measurement_retains_distinct_apparatus_distributionsstandard_momentum_mathematical_observable_is_actively_unfaithfulepr_route_is_nonlocal_but_not_a_controllable_signal_in_quantum_equilibriumepr_analysis_retains_equal_marginal_and_remote_motion_changefield_configuration_and_superwave_extend_packet_logic_to_radiation_quantacompletion_setup_realizes_descriptive_completeness_transitionpaper_realizes_supplemented_deterministic_completionprobabilistic_predictions_coexist_with_a_determinate_individual_outcomestandard_statistics_and_hidden_configuration_keep_probability_roles_distinctempirical_equivalence_is_atomic_regime_scoped_and_short_distance_extensions_remain_speculativenamed_polar_reduction_does_not_supply_printed_equationscontinuity_equation_does_not_supply_an_actual_configurationequivariance_does_not_prove_relaxation_from_arbitrary_nonequilibriumeffective_branch_selection_does_not_require_fundamental_collapseinstantaneous_configuration_influence_does_not_itself_supply_a_signalexcursion_history_uses_the_same_transport_mapexcursion_velocity_uses_the_same_phase_guidancecorrect_born_pushforwards_do_not_establish_guidance
Coverage theorems (12)
every_source_claim_has_semanticsschrodinger_decomposition_route_is_semantically_realizedconfiguration_guidance_route_is_semantically_realizedone_particle_examples_route_is_semantically_realizedmany_body_transitions_route_is_semantically_realizedmeasurement_packets_route_is_semantically_realizedequilibrium_statistics_route_is_semantically_realizedcontextual_observables_route_is_semantically_realizedepr_nonlocality_route_is_semantically_realizedradiation_field_route_is_semantically_realizedcompletion_and_scope_route_is_semantically_realizedall_routes_are_semantically_realizable
Source-map audit theorems (19)
argument_wellFormedargument_auditableroutes_wellFormedroutes_have_exact_predecessor_graphroutes_have_exact_dependency_closureearly_local_inputs_are_independent_hypotheseslate_local_inputs_are_independent_hypothesesearly_calculation_contracts_are_independent_hypotheseslate_calculation_contracts_are_independent_hypothesesprinted_polar_formula_step_applies_exact_calculation_inputsearly_result_steps_apply_selected_inputs_and_contractspolar_result_retains_printed_formula_steplate_result_steps_apply_selected_inputs_and_contractsindependent_paper_local_routes_do_not_claim_unearned_predecessor_outputscompletion_route_consumes_certified_deterministic_motionrelaxation_claim_retains_author_expectationradiation_route_retains_deferred_calculationcompletion_retains_added_physical_postulatesscope_retains_open_short_distance_and_relativistic_obligations
Semantic atoms (42)
schrodingerPolarSetuppolarDecompositionCalculationprintedPolarReductionFormulaBundlecontinuityAndQuantumHamiltonJacobiconfigurationGuidancePostulatestrajectoryExistenceUniquenessCalculationdeterministicContinuousMotionstationaryStateSetupstationaryStateCalculationtwoSlitSetuptwoSlitCalculationoneParticleExampleConclusionsmanyBodySetupmanyBodyCalculationconfigurationSpaceNonlocalitytransitionPacketSetuptransitionPacketCalculationcorrelatedQuantizedTransitionmeasurementPacketSetupmeasurementPacketCalculationeffectiveCollapseWithoutFundamentalCollapseequivarianceSetupequivarianceCalculationequilibriumPreservationrelaxationAssessmentqualifiedRelaxationClaimstandardMomentumMeasurementRuncontextualObservableCalculationcontextualMomentumConclusioneprSetupeprCalculationnonlocalInfluenceWithoutEquilibriumSignalradiationFieldSetupradiationFieldCalculationradiationQuantumConclusioncompletionSetupsupplementedDeterministicCompletionpredictiveBranchingSetupindividualOutcomeDeterminationprobabilisticPredictionWithDeterminateOutcomepaperScopeAssessmentqualifiedEmpiricalScope
Claim identifiers (42)
polarSetuppolarCalculationpolarFormulapolarConclusionguidancePostulatestrajectoryCalculationdeterministicMotionstationarySetupstationaryCalculationslitSetupslitCalculationexamplesConclusionmanyBodySetupmanyBodyCalculationnonlocalManyBodytransitionSetuptransitionCalculationtransitionConclusionmeasurementSetupmeasurementCalculationeffectiveCollapseequilibriumSetupequilibriumCalculationequilibriumPreservedrelaxationAssessmentrelaxationQualifiedmomentumRuncontextualCalculationcontextualConclusioneprSetupeprCalculationeprConclusionradiationSetupradiationCalculationradiationConclusioncompletionSetupcompletionConclusionbranchingSetupoutcomeDeterminationstatisticalDeterminismscopeAssessmentscopeConclusion
Step identifiers (42)
statePolarSetupsupplyPolarCalculationretainPolarFormuladerivePolarConclusionstateGuidancePostulatessupplyTrajectoryCalculationderiveDeterministicMotionstateStationarySetupsupplyStationaryCalculationstateSlitSetupsupplySlitCalculationderiveExamplesConclusionstateManyBodySetupsupplyManyBodyCalculationderiveManyBodyNonlocalitystateTransitionSetupsupplyTransitionCalculationderiveTransitionConclusionstateMeasurementSetupsupplyMeasurementCalculationderiveEffectiveCollapsestateEquilibriumSetupsupplyEquivarianceCalculationderiveEquilibriumPreservationstateRelaxationAssessmentretainQualifiedRelaxationstateMomentumRunsupplyContextualCalculationderiveContextualConclusionstateEprSetupsupplyEprCalculationderiveEprConclusionstateRadiationSetupsupplyRadiationCalculationderiveRadiationConclusionstateCompletionSetupderiveCompletionConclusionstateBranchingSetupstateOutcomeDeterminationderiveStatisticalDeterminismstateScopeAssessmentretainQualifiedScope
Route identifiers (10)
schrodingerDecompositionconfigurationGuidanceoneParticleExamplesmanyBodyTransitionsmeasurementPacketsequilibriumStatisticscontextualObservableseprNonlocalityradiationFieldcompletionAndScope
Route kinds (10)
polarSchrodingerReductionaddedConfigurationDynamicsstationaryAndInterferenceExamplesconfigurationSpaceAndScatteringPacketsapparatusPacketSelectionequivarianceAndRelaxationStatusapparatusContextualObservableeprConfigurationSpaceInfluencefieldModeConfigurationExtensionempiricalCompletionAndQualifiedExtensions
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.
schrodingerDecomposition
Logical kind: polarSchrodingerReduction.
Required predecessor routes: none.
Ordered inference steps: statePolarSetup, supplyPolarCalculation, retainPolarFormula, derivePolarConclusion.
Exported conclusions: polarConclusion.
configurationGuidance
Logical kind: addedConfigurationDynamics.
Required predecessor routes: none.
Ordered inference steps: stateGuidancePostulates, supplyTrajectoryCalculation, deriveDeterministicMotion.
Exported conclusions: deterministicMotion.
oneParticleExamples
Logical kind: stationaryAndInterferenceExamples.
Required predecessor routes: none.
Ordered inference steps: stateStationarySetup, supplyStationaryCalculation, stateSlitSetup, supplySlitCalculation, deriveExamplesConclusion.
Exported conclusions: examplesConclusion.
manyBodyTransitions
Logical kind: configurationSpaceAndScatteringPackets.
Required predecessor routes: none.
Ordered inference steps: stateManyBodySetup, supplyManyBodyCalculation, deriveManyBodyNonlocality, stateTransitionSetup, supplyTransitionCalculation, deriveTransitionConclusion.
Exported conclusions: nonlocalManyBody, transitionConclusion.
measurementPackets
Logical kind: apparatusPacketSelection.
Required predecessor routes: none.
Ordered inference steps: stateMeasurementSetup, supplyMeasurementCalculation, deriveEffectiveCollapse.
Exported conclusions: effectiveCollapse.
equilibriumStatistics
Logical kind: equivarianceAndRelaxationStatus.
Required predecessor routes: none.
Ordered inference steps: stateEquilibriumSetup, supplyEquivarianceCalculation, deriveEquilibriumPreservation, stateRelaxationAssessment, retainQualifiedRelaxation.
Exported conclusions: equilibriumPreserved, relaxationQualified.
contextualObservables
Logical kind: apparatusContextualObservable.
Required predecessor routes: none.
Ordered inference steps: stateMomentumRun, supplyContextualCalculation, deriveContextualConclusion.
Exported conclusions: contextualConclusion.
eprNonlocality
Logical kind: eprConfigurationSpaceInfluence.
Required predecessor routes: none.
Ordered inference steps: stateEprSetup, supplyEprCalculation, deriveEprConclusion.
Exported conclusions: eprConclusion.
radiationField
Logical kind: fieldModeConfigurationExtension.
Required predecessor routes: none.
Ordered inference steps: stateRadiationSetup, supplyRadiationCalculation, deriveRadiationConclusion.
Exported conclusions: radiationConclusion.
completionAndScope
Logical kind: empiricalCompletionAndQualifiedExtensions.
Required predecessor routes: configurationGuidance.
Ordered inference steps: stateCompletionSetup, deriveCompletionConclusion, stateBranchingSetup, stateOutcomeDetermination, deriveStatisticalDeterminism, stateScopeAssessment, retainQualifiedScope.
Exported conclusions: completionConclusion, statisticalDeterminism, scopeConclusion.