PhysicsLogic · Paper-first edition Lean-extracted article 053

Formal reconstruction · Quantum measurement and relative states

The “Relative State” Formulation of Quantum Mechanics

The logical anatomy of closed-system applicability, universal linear dynamics, relative subsystem states, correlated observer records, branching repeatability, square-amplitude measure, statistical typicality, and multiple-observer consistency

Original work encoded in Lean: Hugh Everett III Edition: human-readable logical reconstruction
Formal object PhysicsLogic.Papers.Everett1957
Physical result An observer treated as a physical subsystem inside an isolated closed system exposes the limited domain of an external-observation and Process-1 projection formulation. Pure wave mechanics is proposed as a complete internal model: universal linear Process-2 dynamics with no fundamental collapse. In a composite state, a selected state of one subsystem determines a unique correlated relative state of the other, while no independent absolute subsystem state is generally assigned. A calibrated measurement interaction maps two distinct eigenstates to distinct observer memories; linearity produces both correlated components, definite records relative to each component, and no selected global outcome. Repetition yields agreeing records within every retained branch, a branching memory tree, simultaneous retention of all branches, and no possible-to-actual transition. Positivity, phase independence, orthogonal additivity, and branching conservation uniquely select square-amplitude measure up to normalization. With product sequence measure and an imported limiting probability result, exceptional memory sequences have measure tending to zero and Process-1 frequencies and averages hold almost everywhere in the infinite-observation limit. Communicating observers agree; a noncommuting intervention breaks repeat correlation; remote observation of a correlated noninteracting system leaves the first observer’s repeated result unchanged. The final equivalence of predictions is interpretive and scoped.
Argument architecture 9 routes · 32 semantic claims · 20 source contracts · 12 exact joins · 35 independent fidelity boundaries · 1 grounded shared relative-measurement model

Definitions, structures, and assumptions

Structures, classes, and inductive alternatives

  • structureLinear dynamics on initially ready apparatus and communication registers.
  • inductive
  • structureThe calibrated-superposition constraint used by the shared route.
  • structureShared relational semantics for the repeated linear-correlation and relative-record route. The physical meanings of states, records, branches, and interactions remain paper-local.
  • structureThe same constraint paired with one typed paper-local derivation.
  • structure
  • structureProof-free semantics selected from one linear relative-state measurement argument. No field stores a setup proof, calculation, interpretation, or conclusion.
  • structureThe correlated two-record phenomenon produced by the selected measurement. It retains the situated output without retaining a derivation token.
  • 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
  • inductive
  • inductive
  • structure
  • structureEquations (10)-(12) retain actual calibration, coefficient-preserving linear branching, branch-relative records, phase freedom, and no collapse.
  • structureEquations (33)-(34) give product measure rather than branch counting; positive-measure finite exceptional sequences are not deleted.
  • structurePages 461-462 distinguish ordinary observer agreement, disturbance by a noncommuting local observation, and an undisturbed remote intervention.
  • structureThe normalized two-subsystem expansion on p. 456, with distinct conditional subsystem states and no independently assigned absolute state.
  • structurePaper-local semantic vocabulary. Fields are physical data or proposition-valued relations; none supplies a proof of a desired conclusion.
  • structure
  • structure
  • structure
  • structure
  • structure
  • inductiveEverett's Process-2 route from calibrated observation to memory records.
  • structureOriginal Reviews of Modern Physics p. 460, equations (27)-(31), as a selected real-valued readout of Everett's branch-weight calculation. The functional equation and uniqueness argument remain imported mathematics; this readout keeps the square-amplitude result from collapsing into a named measure.
  • structure
  • structure
  • structure
  • structureRecord access within one specified physical description. Configurations may be classical runs or supported quantum alternatives; the context does not declare them observer-independent worlds or supply a probability law.
  • structure
  • structurePhysical observerhood requires only a physical-system relation and an observer-role relation. It does not require a paper to classify consciousness.
  • structureThe minimal semantics of typicality. `propertyTypicalFor` can mean measure one, overwhelming measure, or another paper-specified small-exception notion; the bridge states how that notion licenses a claim about a typical state.
  • structure

Definitions and domain choices

  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionOne observer reads the pointer; the other reads only the match question M. The two kinds of record are kept distinct, within the same description.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionAn inhabited two-branch measurement used to audit all twenty retained fields. Every relation is sensitive to the selected measurement data rather than being uniformly true or false.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe selected model retains all thirteen physical indices and all seven semantic relation families exactly. This certificate supplies no setup, calculation, interpretation, or physical conclusion.
  • definition
  • definition
  • definition
  • definitionThe exact proof-free calculation model selected by this context.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe unique model fixed by the context's thirteen selected indices.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe complete inhabited two-alternative route, stated directly on every retained physical index and relation family. This is stronger than a collection of implication-valued calculations: both calibrations, both correlated branches, both relative records, and failure of global selection hold at the same selected measurement.
  • definitionPaper-local bridges from one realized technical branch to the four independent conditions defining an operational observer. The observer and target systems are external to the calculation model: neither is inferred from the names of `ObserverState` or `SystemState`.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • 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
  • 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
  • definitionAt the selected two-observation depth, only the all-first history lies outside the chosen frequency tolerance; the other three histories do not.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionPadding a ready register is an isometric embedding, not a communication.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionEven the exact Born-product weight of a selected exceptional history can decay while the independently supplied measure of the whole set does not.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe selected equations-(27)-(31) readout is attached to Everett's two measurement coefficients, selected branch measure, and their two reported measure values. The formula remains Everett-local and is not exported into the shared relative-measurement framework.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe selected first record must belong to the same coefficient model as the paper's post-measurement state. Calibration is on the ready-apparatus subspace; nonzero support selects a relative record, not a global outcome.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe paper-local bridge from membership outside the exceptional set to the corresponding assertion about an individual memory sequence.
  • definition
  • definition
  • definitionThe old numerical readout is attached to one supported configuration of the actual comparison. Its record equality is not an input.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe source-map square-amplitude result retains the generic measure conclusion beside Everett's literal equations-(27)-(31) readout.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionRaw journal pp. 457-458 source chain. It retains Everett's good-observation calibration, linear Process-2 calculation, and relative-memory interpretation without assuming the shared route, endpoint, or explanation.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionAgreement is a property of the computed supported record configurations, not a supplied observer-agreement predicate.
  • definitionPages 455 and 457 use physical systems with memory. Their physical observer role does not require a separate classification of consciousness.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionThe selected Everett measure regards a memory sequence as typical exactly when it lies outside the paper's exceptional set. The only property exposed to the shared context is the Process-1 average statement in the selected asymptotic regime; other measures and regimes are not silently generalized.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionJournal p. 460, equation (31), retained for the selected coefficient and the two component coefficients used in the additivity step: `m(a) = c |a|^2`.
  • definitionThe p. 460 additivity equation represented by equations (27)-(30): the measure of the composite orthogonal component is the sum of the component measures.
  • definitionThe selected normalization is positive, and every value called an amplitude square is nonnegative. The composite component is the orthogonal two-branch sum used in Everett's additivity step.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • 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 universal linear commitment with an actual system and branch.
  • definitionUniversal clauses, possibly vacuous over systems or branches.
  • definition
  • definition
  • definition
  • definition
  • definition
  • 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 realized record constrains a physical value when every compatible configuration satisfies the specified property. This need not identify an exact value, assign a probability, or identify the actual configuration.
  • definitionA realized record determines a value only if every compatible alternative agrees.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionA model-to-world interpretation law. It does not assert that the model has produced a conclusion; use `GroundedModelConclusionAt` for that.
  • definitionA model-to-theory interpretation law. It does not assert that the model has produced a conclusion; use `GroundedModelConclusionAt` for that.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionBuild the epistemic dependency basis in paper order. A conclusion inherits the justification origin of its own step and every origin already attached to its premises.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definitionExpand a set of route identifiers by one dependency edge, iterated with enough fuel to traverse any acyclic graph on the declared routes.
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition

Selected instances and coercions

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

Source mappings and interpretation choices

  • inductive
  • definition
  • instance
  • constructor
  • definition
  • checked statement
  • definition
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • 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
  • recursor
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • inductive
  • definition
  • instance
  • 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
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • 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
  • constructor
  • definition
  • checked statement
  • inductive
  • definition
  • instance
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • recursor
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • definition
  • definition
  • checked statement
  • definition
  • checked statement
  • instance
  • checked statement
  • checked statement
  • instance
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • checked statement
  • checked statement
  • definition
  • definition
  • definition
  • inductive
  • definition
  • instance
  • definition
  • definition
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • recursor
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • 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
  • definition
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • constructor
  • definition
  • checked statement
  • definition
  • definition
  • constructor
  • definition
  • checked statement
  • definition
  • checked statement
  • recursor
  • definition
  • definition
  • structure
  • definition
  • instance
  • definition
  • definition
  • checked statement
  • checked statement
  • definition
  • definition
  • definition
  • definition
  • definition
  • checked statement
  • checked statement
  • checked statement
  • constructor
  • definition
  • checked statement
  • checked statement
  • definition
  • checked statement
  • checked statement
  • definition
  • definition
  • checked statement
  • checked statement
  • checked statement
  • recursor
  • definition
  • checked statement
  • checked statement
  • checked statement
  • checked statementThe square-amplitude source atom retains Everett's literal equations-(27)-(31) formula beside the generic measure conclusion.
  • 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
  • definition
  • definition
  • checked statement
  • checked statement
  • definition
  • checked statement
  • checked statement
  • checked statement
  • definition
  • checked statement
  • checked statement
  • instance
  • checked statement
  • checked statement
  • instance
  • checked statement
  • checked statement
  • instance
  • checked statement
  • checked statement
  • instance
  • checked statement
  • checked statement
  • instance
  • checked statement
  • checked statement
  • instance
  • definition
  • definition
  • instance
  • definition
  • definition
  • instance
  • definition
  • definition
  • instance
  • definition
  • definition
  • instance
  • definition
  • definition
  • checked statement
  • checked statement
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • definition
  • checked statement
  • definition
  • definition
  • checked statement
  • checked statement
  • checked statement
  • definition
  • definition
  • checked statement
  • checked statement
  • definition
  • definition
  • definition
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement

Checked statements: parameters, hypotheses, and interpretation

  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementThe reconstructed exceptional tail genuinely converges to zero but remains strictly positive at every finite observation depth.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementEverett 1957, pp. 457-458, especially equations (8) and (10)-(12): a good observation calibrates distinct records on eigenstates, while Process-2 linearity maps their superposition to correlated relative records without Process-1 selection in the total description.
  • checked statement
  • checked statementEverett 1957, pp. 457-458: the same established route contains two distinct system alternatives, observer states, records, and branches, with both calibrated correlations present in one unselected total state.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementEverett's physical-system and memory semantics connect the first realized shared branch to the neutral operational-observer conditions.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementThe actual measurement route preserves both unequal amplitudes, both calibrated records, branch-relative repetition, and absence of selection.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementThe observer route distinguishes local noncommuting disturbance from a remote observation of a correlated but noninteracting system.
  • checked statementA realized operational record has a nonempty pointer fiber whose compatible configurations all give the same object value.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementThe p. 456 source route retains the actual normalized coefficient array and both different conditioned subsystem vectors.
  • checked statement
  • checked statementThe established shared relative-state route realizes Everett's operational observer role only through the paper-local physical-memory bridge.
  • checked statement
  • checked statement
  • checked statement
  • checked statementA chosen product-history weight and the entire exceptional-set measure are distinct limits; the second still needs the imported typicality result.
  • checked statementEquations (33)-(34) remain product weights rather than equal branch counting, and the finite exceptional set remains nonempty before the limit.
  • checked statementEverett 1957, p. 461: a memory sequence outside the exceptional set inherits the Process-1 average statement. The limiting calculation and the set-to-sequence bridge remain separate explicit inputs.
  • checked statementCalibration alone does not make the zero vector a record-bearing state. This input is not a normalized physical state; it tests nonvacuity.
  • checked statementRetaining the paper's role labels and correlation predicates while replacing the coefficient dynamics by zero cannot realize a record.
  • checked statement
  • checked statementA measure with the right name can preserve two-component additivity while failing equation (31): the selected squared amplitude is one but its assigned measure is zero.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statementEquations (27)-(31) retain both the orthogonal additivity equation and the square-amplitude value assigned to the selected coefficient.
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement
  • checked statement

Axioms and trust boundaries

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

Constructors, projections, and other meaning dependencies

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

Every physical statement, dependency, equation-level paraphrase, and epistemic qualifier in this edition is taken only from Everett1957.lean, its imported shared semantics, SourceMap.lean, and Coverage.lean. Composite-state decomposition and limiting probability are retained as imported results. The finite record component now derives measurement and communication coefficients from calibrated linear maps. Their physical realization, repeated-observation inputs, local intervention, and remote noninteraction remain separately explicit; equations (27)–(31) are displayed below because the Lean file now retains their positive domain, additive component measure, and value-level square-amplitude formula. Relative-record and final-scope claims remain interpretations. No later “many-worlds” terminology, decoherence theory, decision theory, or stronger probability claim is introduced.

01

Universal dynamics, relative records, and statistical typicality are successive—not interchangeable—claims

Everett presents the external-observation limitation, pure Process-2 proposal, relative states, calibrated measurement, repetition, measure, and multiple-observer cases in a conceptual sequence. The source map does not turn that chronology into entailment: those seven routes begin from independent paper-local contracts. The checked cross-route edges are narrower. Square-amplitude output plus product-sequence data constructs the typicality setup, and the final conclusion combines pure dynamics, typicality, observer agreement, and an explicit universal-realization bridge.

Closed-system limitationobserver inside isolated system · no external observation · Process 1 inapplicable · external formulation incomplete
Pure Process-2 wave mechanicscomplete universal description · deterministic linear dynamics · no fundamental collapse
Relative states and calibrated measurementunique relative subsystem state · correlated records in two retained components · no global outcome selection
Two downstream branchesrepeatability → branching memory → square-amplitude measure → typicality  │  multiple observers → communication/intervention consistency
Qualified relative-state conclusionuniversal linear relative states · orthodox statistics almost everywhere · observer agreement
Figure 1. The paper's expository order. The checked route graph keeps the first seven route families independent, joins measure output to product-sequence data only at typicality, and joins pure dynamics, typicality, and observer agreement only at the qualified conclusion.
Epistemic ledger
TransitionStatusRetained qualification
Closed observer system to external-formulation limitobstructionThe limitation does not by itself construct pure wave mechanics.
Pure Process 2 to universal completionphysical postulate + calculationCompleteness and absence of collapse are explicit outputs.
Composite state to relative subsystem statesimported setup + calculationA unique state is relative to a chosen state of the other subsystem.
Linear interaction to definite recordscalculation + relative-record interpretationDefiniteness is branch-relative; no global outcome is selected.
Repeated observation to branching memorycalculationEvery retained branch is repeatable; no possible-to-actual transition occurs.
Measure axioms to square amplitudeuniqueness calculationPositivity alone is insufficient; all four axioms are used.
Product measure to Process-1 statisticsimported asymptotic limitThe result is almost everywhere and exact only in the infinite-observation limit.
Pure dynamics and statistics to final scopeinterpretive assessmentEquivalence of predictions is asserted within the paper’s stated domain.
02

An observer inside a closed system cannot be treated from an external vantage point

The universe system is isolated and contains the observer system, which is explicitly both an observer and a physical system. The limitation calculation denies external observation, denies applicability of Process 1 to the closed system, and says neither approximate measurement in general nor the closed universe is covered by the external-observer description.

observer ⊂ isolated universe ⇒ no external observer position,
Process 1 not applicable to the total closed system and external-observation formulation insufficient. applicability obstruction, not yet an alternative dynamical theory (1)
Closed-system limitation theoremdomain obstruction

The physical-observer setup and limitation establish all four failures of external-observation coverage.

external_observation_formulation_does_not_cover_closed_observer_systems · RMP pp. 454–455

The proposed completion assigns a universal wave function to the closed system, makes it obey the linear wave equation, and embeds any externally observed subsystem in a larger isolated system.

universal wave description + linear Process-2 evolution
⇒ complete model for every isolated system + universal deterministic linear dynamics + no fundamental collapse. paper’s pure-wave postulate and completion calculation (2)
Pure-wave completion theorempostulate + checked composition

The setup and completion calculation establish mathematical completeness, representational completeness, linear universal dynamics, and absence of collapse.

pure_process_two_supplies_the_internal_closed_system_theory · RMP p. 455
03

A composite state determines correlated relative states, not independent absolute subsystem states

The imported setup identifies an object and observer as subsystems of one composite system. Given a selected state of the object, the calculation constructs a state of the observer relative to it, proves uniqueness of that relative state, records subsystem correlation, and denies assignment of the selected independent absolute object state.

composite state |Ψobject+observer⟩ + chosen object state |si⟩
⇒ unique observer state relative to |si⟩,
while the subsystem generally has no independent absolute state. schematic relative-state construction of RMP p. 456 (3)
Relative-state theoremimported composite formalism + calculation

The composite setup and calculation establish non-absolute assignment, relative assignment, uniqueness, and correlation.

composite_formalism_yields_unique_relative_not_absolute_subsystem_state · RMP p. 456
04

Linearity turns a calibrated observation into correlated relative records without global selection

A good measurement has two distinct eigenstates, observer states, records, and branches. The interaction is calibrated so each eigenstate leaves the object value stable and produces its corresponding memory symbol. The input object state superposes the two eigenstates, and Process-2 linearity applies.

(c₁|s₁⟩ + c₂|s₂⟩)|O₀⟩ → c₁|s₁⟩|O₁, record 1⟩ + c₂|s₂⟩|O₂, record 2⟩,
each record definite relative to its component, but no single global outcome selected. schematic equations (10)–(12); coefficients remain abstract paper-local objects (4)
Linear relative-record theoremcalculation + interpretation

The calibrated setup, linear calculation, and relative-record bridge establish both contained branches, both relative definite records, and absence of global selection.

linear_measurement_produces_correlated_relative_records_without_selection · RMP pp. 457–458

The operational-observer adapter adds a useful semantic check: the observer role is realized through physical status, calibrated interaction, produced information, and an available record. Consciousness or a bare observer label is not used as sufficient evidence.

Operational observer theoremsemantic realization

A correlated definite memory record realizes observation of the object by the physical observer system.

correlated_memory_record_realizes_operational_observer_role
05

A repeated observation agrees within every retained branch and extends the memory tree

The observer measures the same quantity again while both original branches remain in the state. Applying the interaction branch by branch produces two record sequences, and each new record agrees with the earlier record in its own branch.

record 1 → record 1, record 1;   record 2 → record 2, record 2,
observer memory forms a branching tree, all branches remain retained, and no possible-to-actual transition occurs. branch-relative repeatability of equations (19)–(23) (5)
Branching-repeatability theoremlinear repeated-observation calculation

The repeated setup and calculation establish agreement in both branches, branching memory, simultaneous branch retention, and absence of outcome actualization.

repeated_observation_is_repeatable_within_every_retained_branch · RMP pp. 458–459

The countermodel two_correlated_branches_do_not_select_one_global_outcome makes the intended non-implication explicit: correlation and branch existence do not provide a unique globally selected outcome.

06

Square amplitude follows from four measure axioms; orthodox frequencies require a further asymptotic theorem

The branch measure is required to be positive, insensitive to phase, additive over orthogonal components, and conserved under later branching. A supplied functional calculation then identifies square amplitude as the unique measure up to normalization and assigns measures to the two selected coefficients.

positivity + phase independence + orthogonal additivity + conservation under branching
⇒ m(a) = c |a|2,
|a12|2 = |a1|2 + |a2|2,    m(a12) = m(a1) + m(a2). equations (27)–(31), with positive c and nonnegative squared amplitudes, up to normalization (6)
Measure-uniqueness theoremfunctional calculation

The stronger source result retains orthogonal additivity and m(a) = c |a|^2 beside the generic square-amplitude conclusion and selected coefficient measures. The older theorem remains a projection used by downstream typicality.

additive_branch_conserved_measure_retains_equations_twenty_seven_through_thirty_one · additive_branch_conserved_measure_is_square_amplitude · RMP p. 460

For repeated observations, each memory sequence receives the product of its component square-amplitude measures. The limiting probability statement is imported: exceptional sequences have measure tending to zero. Only with that limit do Process-1 independent weights, averages, frequencies, and apparent validity follow almost everywhere.

sequence measure = product of branch square amplitudes + infinite-sequence probability limit
⇒ measure(exceptional sequences) → 0,
Process-1 averages and frequencies hold for almost all sequences. asymptotic and almost-everywhere recovery, not a finite-sequence identity (7)
Statistical-typicality theoremimported probability limit

Square-amplitude product measure and the imported limit establish independent weights, a vanishing exceptional set, Process-1 averages outside it, and apparent validity to the observer.

product_measure_and_limit_recover_process_one_statistics_almost_everywhere · RMP p. 461

Three missing shortcuts

positivity_alone_does_not_identify_square_amplitude requires the remaining measure axioms. named_square_amplitude_measure_does_not_supply_equations_twenty_seven_through_thirty_one keeps a name and two-component additivity from substituting for equation (31). finite_sequence_data_does_not_supply_the_asymptotic_limit requires the imported infinite-sequence result.

07

Observer agreement survives communication, while noncommuting intervention has a distinct effect

The multiple-observer setup includes separate observation of the same quantity, subsequent communication, an intervention measuring a noncommuting observable, and a remote system correlated but noninteracting with the first. Calibrated linear maps now derive record agreement. The other intervention results remain separate physical inputs, not consequences of agreement alone.

U e_i=e_(i,i); V e_(i,j)=e_(i,j,j), for every basis input.
psi=U a; Psi=V psi; psi(i,i)=Psi(i,i,i)=a(i).
sum |a(i)|^2=1 implies ||psi||^2=||Psi||^2=1. The same complex coefficients are retained. These are maps on ready-apparatus subspaces, not arbitrary-state cloning or a derived physical Hamiltonian.
A={(i,j,k): Psi(i,j,k)!=0}; r_O(i,j,k)=j; r_P(i,j,k)=k.
A is nonempty; every admitted configuration has i=j=k.
A record determines v only if its compatible set is nonempty and every compatible configuration has value v. Agreement is derived from calibration and actual support, not supplied as an endpoint. Agreement alone does not establish true value determination or select a single-outcome quantum state.

The process uses the selected initial object state and the selected measurement and communication interactions. Exact representation inputs attach its two coefficient states to the paper's correlated-measurement and multiple-observer states. The selected numerical records refer to one supported configuration of this same process.

observer_comparison_derives_actual_record_access · OriginalObserverInterventionSourceInputs · RMP pp. 458, 461-462
Illustrative input: a(0)=3/5; a(1)=4i/5.
Psi(0,0,0)*conj(Psi(1,1,1))=-12i/25 != 0.
An unread receiving register instead has Psi_unread(1,1,0)=4i/5: norm one, but records do not agree. Finite physical controls, not numerical data reported by Everett. Communication preserves this coherence; no Born rule or outcome ontology is inferred.
record_agreement_does_not_produce_a_single_outcome_state · correlated_measurement_does_not_supply_communication · communicating_records_do_not_remove_global_coherence
same-quantity observations + communication ⇒ records agree,
noncommuting intervention ⇒ repeat correlation not preserved,
remote observation of correlated noninteracting system ⇒ first observer’s local repeat result unchanged. combined Rules 1–2 calculation of RMP pp. 461–462 (8)
Multiple-observer theoremcombined observer-memory calculation

The setup and calculation establish communication agreement, intervention-sensitive repeatability, and remote-record stability.

multiple_observers_agree_with_the_qualified_intervention_rules · RMP pp. 461–462

The final scope requires four established ingredients: universal linear relative-state dynamics applied to an actual physical observer with an actual retained branch and branch-relative definite record, continuous state-function evolution of the selected composite observer system, Process-1 statistics appearing valid in the asymptotic regime, and agreement between communicating observers. Universal clauses over empty system or branch scopes do not realize this commitment, and universal-linear labels alone do not supply continuity.

Qualified relative-state theoremfinal interpretive assessment

The setup and assessment preserve the paper’s claim that continuous pure Process-2 evolution covers closed systems and observer interactions while retaining standard statistical predictions within the encoded scope.

relative_state_formulation_has_the_paper_s_qualified_scope · qualified_conclusion_retains_continuous_state_evolution · RMP p. 462

everett_route_recovers_orthodox_statistics_without_process_one_dynamics makes the central combination explicit: no fundamental collapse and no global outcome selection coexist with recovered asymptotic statistics.

08

The shared model isolates calibrated linear measurement and relative records

The existing reusable linear-relative-state model selects the object and observer, two object states, two observer states, two records, two branches, the calibrated interaction, correlated output, and measurement regime. A separate finite coefficient component now derives actual record comparison and is also used by Rovelli. Neither component absorbs measure uniqueness, typicality, or the separate intervention conclusions.

Shared realization boundary
IncludedPaper-local and excluded
Distinct inputs and records, calibrated interaction, linear two-branch correlation, relative definite records, no global selectionClosed-universe motivation, repeated branching, square-amplitude derivation, statistical limit, multiple-observer rules, final scope
Grounded relative-measurement theoremsemantic realization and transfer

The calibrated setup, linear calculation, and relative-record interpretation establish the direct fifteen-fact shared endpoint. Explicit theory/world interpretation grounds the good-measurement setup independently of correlation and record outputs, then transfers every shared claim. Calculation and interpretation contracts are reconstructed from the output-led result.

everett_measurement_model_inputs_establish_theory_model_grounding · everett_measurement_establishes_grounded_shared_relative_measurement · grounded_everett_measurement_transfers_every_shared_claim
Process-2 source explanationsource-sensitive structural explanation

The raw source relation retains the good-observation calibration, Process-2 linear correlation, and relative-memory interpretation. It makes the shared route applicable and realizes both the ordinary structural explanation and the stronger explanation that exposes Everett's derivation. The completed branch route reaches the operational-observer role only through its separate physical-memory bridge.

everettLinearRelativeStateMeasurementDerivationObtains · everett_source_inputs_make_shared_relative_measurement_route_applicable · everett_source_inputs_realize_structural_linear_relative_state_measurement_explanation · everett_source_inputs_realize_source_structural_linear_relative_state_measurement_explanation · first_shared_relative_record_realizes_operational_observer_bridge · shared_relative_measurement_realizes_operational_observer_role · RMP pp. 457–458
Reader aids and formal audit
A

Concept guide

Closed observer system

An isolated physical system containing its own physical observer, with no external observation position.

ExternalObservationProblemSetup

Universal Process 2

A complete deterministic linear wave dynamics for every isolated system, with no fundamental collapse.

PureWaveCompletionCalculation

Relative subsystem state

The unique state of one subsystem conditional on a selected state of the other, replacing a generally unavailable independent absolute state.

RelativeStateCalculation

Correlated relative records

Distinct observer memories correlated with object eigenstates and definite relative to their retained components.

RelativeRecordInterpretation

No global outcome selection

The explicit denial that the correlated measurement state selects one independent global outcome.

globallySelectsSingleOutcome

Branching memory

Repeatable branch-relative record histories with all branches retained and no possible-to-actual transition.

RepeatedObservationCalculation

Square-amplitude measure

The unique normalized form selected by positivity, phase independence, orthogonal additivity, and branching conservation, with equations (27)–(31) retained as explicit value relations.

SquareAmplitudeMeasureResult · SquareAmplitudeFormulaReadout

Statistical typicality

Almost-everywhere recovery of Process-1 weights, averages, and frequencies under product measure in the infinite-sequence limit.

StatisticalTypicalityCalculation

Multiple-observer consistency

Agreement after communication, intervention-sensitive repeat correlation, and stability under remote noninteracting observation.

MultipleObserverCalculation

Qualified relative-state scope

The interpretive conjunction of nonvacuously realized universal linear dynamics, an actual retained observer branch, apparent orthodox statistics, and observer agreement.

QualifiedConclusionCalculation

Shared relative-measurement model

The reusable calibrated linear correlation and relative-record structure.

relativeMeasurementModel
B

Route inventory, non-implications, and formal provenance

The source map declares nine routes and thirty-two semantic claims. Twenty source-contract steps are premise-free; twelve deductions reopen exact premise maps. Coverage interprets every atom and certifies every route without extracting semantic outputs from route certificates.

Complete route inventory
RouteDirect dependenciesOutputProfile
Closed-system applicability—External-observation formulation insufficientobstruction
Internal Process-2 completionIndependentUniversal pure-wave theoryphysical postulate
Composite subsystem relativityIndependentUnique correlated relative states, no absolute assignmentimported setup + calculation
Calibrated linear observationIndependentRelative records without global selectioncalculation + interpretation
Branch-relative repeatabilityIndependentRepeatability and retained branching memorycalculation
Branch-measure derivationIndependentSquare-amplitude measureuniqueness calculation
Asymptotic statistical recoveryMeasure uniquenessProcess-1 statistics almost everywhereimported probability limit
Observer communication consistencyIndependentQualified multiple-observer rulescalculation
Interpretive scopePure wave; typicality; observersQualified relative-state conclusioninterpretive assessment
External limit · external_observation_limit_route_is_semantically_realized
Certifies the physical observer setup and all four limits of external observation.
Pure wave · pure_wave_theory_route_is_semantically_realized
Certifies universal linear completion without collapse.
Relative state · relative_state_route_is_semantically_realized
Certifies relative assignment, uniqueness, correlation, and non-absolute status.
Linear measurement · linear_measurement_route_is_semantically_realized
Certifies branch containment and relative records without global selection from setup, linear calculation, and the explicit relative-record interpretation.
Repeated branching · repeated_branching_route_is_semantically_realized
Certifies repeatability, memory tree, retention, and no actualization transition.
Measure · measure_uniqueness_route_is_semantically_realized
Certifies the four axioms and square-amplitude uniqueness.
Typicality · statistical_typicality_route_is_semantically_realized
Builds the setup from checked square-amplitude output and independent product-measure data, then certifies the imported limit, exceptional-set bridge, and almost-everywhere statistics.
Multiple observers · multiple_observers_route_is_semantically_realized
Certifies communication, intervention, and remote-observation outputs.
Qualified conclusion · qualified_conclusion_route_is_semantically_realized
Consumes pure-wave, typicality, and observer outputs plus the explicit universal-realization bridge, then certifies final scope.

Selected formal non-implications

The summary counts the independent Lean fidelity inventory. This table illustrates selected paper-local or shared-framework witnesses; it does not define that inventory.

Available factConclusion not suppliedLean witness
External formulation fails for a closed observer systemPure-wave completionclosed_system_limitation_does_not_supply_pure_wave_completion
Two correlated branches existOne globally selected outcometwo_correlated_branches_do_not_select_one_global_outcome
A branch measure is positiveSquare-amplitude formpositivity_alone_does_not_identify_square_amplitude
A named additive measure has a nonnegative selected valueEquations-(27)-(31) square-amplitude packagenamed_square_amplitude_measure_does_not_supply_equations_twenty_seven_through_thirty_one
Finite memory-sequence dataThe asymptotic limiting theoremfinite_sequence_data_does_not_supply_the_asymptotic_limit
An aggregate small exceptional set and an outside sequenceThe individual frequency bridgebulk_typicality_does_not_supply_the_individual_sequence_bridge
Universal and linear dynamics labelsContinuous composite-system state evolutionuniversal_linear_dynamics_labels_do_not_supply_continuous_state_evolution

The witnesses are value-bearing: one isolated observer system has zero external runs and no internal model; two calibrated alternatives retain both correlated branches; normalized weights one-half and one-half disagree with squared amplitudes one-quarter and three-quarters; a length-two product sequence has a nonvanishing one-half exceptional tail; an outside length-four sequence has frequency zero, outside the one-quarter tolerance around the one-half expected weight; and two linearly evolved states have zero continuous histories. No proposition pair or Unit-carrier truth table replaces these distinctions.

Machine-checked audit boundary

argument_wellFormed, argument_auditable, routes_wellFormed, route_order_is_valid, and route_outputs_are_produced certify source-map structure. routes_have_exact_predecessor_graph, the two source-contract audits, the two result-input audits, and cross_route_joins_apply_exact_semantic_inputs pin the premise graph. route_semantic_realization_is_exhaustive constructs all nine routes from source inputs. The status audits retain the imported typicality limit and interpretive final scope.

Lean-encoded bibliographic record

H. Everett III, “Relative State” Formulation of Quantum Mechanics, Reviews of Modern Physics 29 (1957), 454–462. 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 (93)

original_unequal_composite_coefficients_have_distinct_normalized_relative_statesoriginal_two_retained_observer_branches_have_unequal_phase_insensitive_weightsoriginal_product_measure_differs_from_branch_counting_and_retains_finite_exceptionsoriginal_selected_exceptional_tail_is_positive_at_every_finite_depthoriginal_noncommuting_observation_disturbs_local_repeat_but_remote_observation_does_notequations_twenty_seven_through_thirty_one_retain_square_amplitude_additivityoriginal_normalized_square_amplitude_measure_has_unequal_branch_weightsnamed_square_amplitude_measure_does_not_supply_equations_twenty_seven_through_thirty_onephysical_observer_role_iff_declared_role_and_physical_systemclosed_system_setup_realizes_physical_observer_roleexternal_observation_formulation_does_not_cover_closed_observer_systemspure_process_two_supplies_the_internal_closed_system_theorycomposite_formalism_yields_unique_relative_not_absolute_subsystem_staterelative_state_route_retains_original_normalized_conditional_coefficientslinear_measurement_produces_correlated_relative_records_without_selectionmeasurement_route_retains_original_unequal_relative_memory_branchescorrelated_memory_record_realizes_operational_observer_roleoperational_observer_exposes_a_supported_pointer_recordzero_output_measurement_cannot_realize_an_operational_observerzero_input_preserves_calibration_but_cannot_realize_a_recordrepeated_observation_is_repeatable_within_every_retained_branchadditive_branch_conserved_measure_is_square_amplitudeadditive_branch_conserved_measure_retains_equations_twenty_seven_through_thirty_onesquare_amplitude_measure_result_retains_equations_twenty_seven_through_thirty_onesquare_amplitude_result_and_product_measures_establish_typicality_setupmemory_sequence_bridge_realizes_shared_typical_property_bridgeproduct_measure_and_limit_recover_process_one_statistics_almost_everywherestatistical_route_retains_original_product_measure_and_finite_exceptionsstatistical_route_distinguishes_selected_history_from_exceptional_set_limitstatistical_limit_realizes_shared_typical_propertytypical_memory_sequence_inherits_process_one_averagesmultiple_observers_agree_with_the_qualified_intervention_rulesobserver_comparison_derives_actual_record_accessobserver_route_retains_original_local_disturbance_and_remote_stabilitypaper_commitments_realize_universal_linear_relative_stateprior_outputs_and_universal_bridge_establish_qualified_conclusion_setuprelative_state_formulation_has_the_paper_s_qualified_scopequalified_conclusion_retains_continuous_state_evolutioneverett_route_recovers_orthodox_statistics_without_process_one_dynamicslinear_relative_state_measurement_model_retains_paper_semanticsgood_measurement_realizes_shared_calibrated_setuplinear_calculation_realizes_shared_branch_correlationrelative_records_realize_shared_interpretationeverett_source_inputs_make_shared_relative_measurement_route_applicableeverett_source_inputs_realize_structural_linear_relative_state_measurement_explanationeverett_source_inputs_realize_source_structural_linear_relative_state_measurement_explanationeverett_inputs_make_shared_relative_measurement_route_applicableeverett_measurement_realizes_shared_relative_state_measurementeverett_measurement_exhibits_nonvacuous_shared_two_branch_routefirst_shared_relative_record_realizes_operational_observer_bridgeshared_relative_measurement_realizes_operational_observer_roleeverett_measurement_model_inputs_establish_theory_model_groundingeverett_measurement_establishes_grounded_shared_relative_measurementgrounded_everett_measurement_transfers_every_shared_claimclosed_system_limitation_does_not_supply_pure_wave_completiontwo_correlated_branches_do_not_select_one_global_outcomepositivity_alone_does_not_identify_square_amplitudefinite_sequence_data_does_not_supply_the_asymptotic_limita_vanishing_selected_product_history_does_not_make_the_whole_exceptional_set_vanishbulk_typicality_does_not_supply_the_individual_sequence_bridgeuniversal_linear_dynamics_labels_do_not_supply_continuous_state_evolutiona_nonzero_composite_coefficient_does_not_fix_relative_state_normalizationnormalization_does_not_make_a_composite_state_nonfactorizablethe_first_conditioned_subsystem_state_does_not_fix_the_seconddistinct_relative_states_do_not_supply_an_independent_absolute_statecalibration_of_one_eigenstate_does_not_calibrate_the_otherpreserving_one_superposition_coefficient_does_not_preserve_the_othertwo_retained_relative_branches_do_not_select_one_global_outcomeone_definite_relative_memory_does_not_delete_the_other_branchtwo_equally_counted_branches_do_not_have_equal_square_amplitude_weightan_amplitude_phase_reversal_does_not_preserve_the_signed_amplituderepeatability_in_one_relative_branch_does_not_prove_the_other_branchnormalized_single_observation_weights_do_not_supply_a_sequence_productone_sequence_product_does_not_fix_the_reverse_sequence_weightcounting_mixed_branches_does_not_give_their_square_amplitude_measurea_normalized_product_measure_does_not_remove_positive_measure_finite_exceptionsa_vanishing_asymptotic_exceptional_measure_does_not_vanish_at_finite_lengtha_decreasing_exceptional_tail_does_not_remove_the_next_finite_exceptionone_finite_memory_sequence_need_not_have_the_born_frequencya_small_finite_exceptional_measure_does_not_eliminate_exceptional_sequencesone_correct_sequence_product_does_not_normalize_all_memory_sequencesobserver_agreement_does_not_prevent_a_noncommuting_local_disturbancea_noncommuting_local_disturbance_does_not_disturb_a_remote_repeatremote_noninteraction_does_not_make_local_observables_commuteuninterrupted_repeatability_does_not_survive_a_noncommuting_interventionunequal_complex_process_has_actual_calibrated_inputsunequal_complex_process_retains_two_nonzero_amplitudesactual_communication_derives_record_agreementrecord_agreement_does_not_produce_a_single_outcome_stateunread_register_keeps_the_actual_normcorrelated_measurement_does_not_supply_communicationactual_records_retain_complex_interbranch_coherencecommunicating_records_do_not_remove_global_coherence

Shared observer and source-explanation identifiers (6)

first_shared_relative_record_realizes_operational_observer_bridgeshared_relative_measurement_realizes_operational_observer_roleeverettLinearRelativeStateMeasurementDerivationObtainseverett_source_inputs_make_shared_relative_measurement_route_applicableeverett_source_inputs_realize_structural_linear_relative_state_measurement_explanationeverett_source_inputs_realize_source_structural_linear_relative_state_measurement_explanation

Coverage theorems (13)

observer_consistency_atom_retains_actual_record_accessevery_source_claim_has_semanticssquare_amplitude_measure_atom_retains_equations_twenty_seven_through_thirty_oneexternal_observation_limit_route_is_semantically_realizedpure_wave_theory_route_is_semantically_realizedrelative_state_route_is_semantically_realizedlinear_measurement_route_is_semantically_realizedrepeated_branching_route_is_semantically_realizedmeasure_uniqueness_route_is_semantically_realizedstatistical_typicality_route_is_semantically_realizedmultiple_observers_route_is_semantically_realizedqualified_conclusion_route_is_semantically_realizedroute_semantic_realization_is_exhaustive

Source-map audit theorems (16)

argument_wellFormedargument_auditableroutes_wellFormedroute_order_is_validroute_outputs_are_producedreductio_scopes_are_route_localroute_outputs_discharge_temporary_assumptionsroutes_have_exact_predecessor_graphearly_source_contracts_are_independent_hypotheseslate_source_contracts_are_independent_hypothesesearly_result_steps_apply_exact_semantic_inputslate_result_steps_apply_exact_semantic_inputscross_route_joins_apply_exact_semantic_inputstypicality_retains_imported_limit_statusindividual_sequence_result_retains_limit_and_bridge_statusfinal_scope_retains_interpretive_status

Semantic atoms (32)

closedObserverSystemSetupexternalObservationLimitationexternalFormulationInsufficientpureWaveTheorySetupuniversalCompletionCalculationpureProcessTwoTheoryrelativeStateSetuprelativeStateCalculationrelativeSubsystemStatesgoodMeasurementSetuplinearMeasurementCalculationrelativeRecordInterpretationrelativeRecordsWithoutSelectionrepeatedObservationSetuprepeatedObservationCalculationbranchingRepeatabilitymeasureAxiomsmeasureUniquenessCalculationsquareAmplitudeMeasurememorySequenceProductMeasuresstatisticalTypicalitySetupstatisticalLimitCalculationmemorySequenceTypicalityBridgeprocessOneStatisticsAlmostEverywheretypicalMemorySequenceProcessOneAveragesmultipleObserverSetupmultipleObserverCalculationobserverConsistencyqualifiedUniversalRealizationBridgequalifiedConclusionSetupqualifiedConclusionCalculationqualifiedRelativeStateConclusion

Claim identifiers (32)

externalSetupexternalCalculationexternalResultpureSetuppureCalculationpureResultrelativeSetuprelativeCalculationrelativeResultmeasurementSetupmeasurementCalculationmeasurementInterpretationmeasurementResultrepeatSetuprepeatCalculationrepeatResultmeasureSetupmeasureCalculationmeasureResulttypicalityProductstypicalitySetuptypicalityCalculationtypicalityBridgetypicalityResulttypicalSequenceResultobserversSetupobserversCalculationobserversResultconclusionBridgeconclusionSetupconclusionCalculationconclusionResult

Step identifiers (32)

stateExternalSetupsupplyExternalCalculationderiveExternalResultstatePureSetupsupplyPureCalculationderivePureResultstateRelativeSetupsupplyRelativeCalculationderiveRelativeResultstateMeasurementSetupsupplyMeasurementCalculationsupplyMeasurementInterpretationderiveMeasurementResultstateRepeatSetupsupplyRepeatCalculationderiveRepeatResultstateMeasureSetupsupplyMeasureCalculationderiveMeasureResultsupplyTypicalityProductsderiveTypicalitySetupsupplyTypicalityCalculationstateTypicalityBridgederiveTypicalityResultderiveTypicalSequenceResultstateObserversSetupsupplyObserversCalculationderiveObserversResultsupplyConclusionBridgederiveConclusionSetupsupplyConclusionCalculationderiveConclusionResult

Route identifiers (9)

externalObservationLimitpureWaveTheoryrelativeStatelinearMeasurementrepeatedBranchingmeasureUniquenessstatisticalTypicalitymultipleObserversqualifiedConclusion

Route kinds (9)

closedSystemApplicabilityinternalProcessTwoCompletioncompositeSubsystemRelativitycalibratedLinearObservationbranchRelativeRepeatabilitybranchMeasureDerivationasymptoticStatisticalRecoveryobserverCommunicationConsistencyinterpretiveScope

C

Relative coefficients, product histories, and physical observers

The selected normalized composite amplitudes are 3/5 and 4/5; the two conditioned subsystem vectors are (1,0) and (0,1), with no independently assigned absolute subsystem state. The corresponding retained observer-memory branches have unequal weights 9/25 and 16/25. Reversing the sign of the first amplitude preserves its weight.

For two observations the four sequence weights are 81/625, 144/625, 144/625, and 256/625. The mixed-history measure is 288/625, not the equal branch-counting fraction 1/2. One finite exceptional history retains positive measure 81/625 under frequency tolerance 1/2; its actual Born-product tail (9/25)^(n+2) stays positive at every finite depth and converges to zero. A separate countermodel retains that decaying history while the entire exceptional set has nonvanishing measure 1/2.

Communicating observers agree, a noncommuting local measurement changes the repeated local record, and a remote noninteracting measurement does not. These reconstructed instances preserve the paper's original asymptotic and observer distinctions through 32 physically inhabited boundaries.

R

Checked source-route details

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

externalObservationLimit

Logical kind: closedSystemApplicability.

Required predecessor routes: none.

Ordered inference steps: stateExternalSetup, supplyExternalCalculation, deriveExternalResult.

Exported conclusions: externalResult.

pureWaveTheory

Logical kind: internalProcessTwoCompletion.

Required predecessor routes: none.

Ordered inference steps: statePureSetup, supplyPureCalculation, derivePureResult.

Exported conclusions: pureResult.

relativeState

Logical kind: compositeSubsystemRelativity.

Required predecessor routes: none.

Ordered inference steps: stateRelativeSetup, supplyRelativeCalculation, deriveRelativeResult.

Exported conclusions: relativeResult.

linearMeasurement

Logical kind: calibratedLinearObservation.

Required predecessor routes: none.

Ordered inference steps: stateMeasurementSetup, supplyMeasurementCalculation, supplyMeasurementInterpretation, deriveMeasurementResult.

Exported conclusions: measurementResult.

repeatedBranching

Logical kind: branchRelativeRepeatability.

Required predecessor routes: none.

Ordered inference steps: stateRepeatSetup, supplyRepeatCalculation, deriveRepeatResult.

Exported conclusions: repeatResult.

measureUniqueness

Logical kind: branchMeasureDerivation.

Required predecessor routes: none.

Ordered inference steps: stateMeasureSetup, supplyMeasureCalculation, deriveMeasureResult.

Exported conclusions: measureResult.

statisticalTypicality

Logical kind: asymptoticStatisticalRecovery.

Required predecessor routes: measureUniqueness.

Ordered inference steps: supplyTypicalityProducts, deriveTypicalitySetup, supplyTypicalityCalculation, stateTypicalityBridge, deriveTypicalityResult, deriveTypicalSequenceResult.

Exported conclusions: typicalityResult, typicalSequenceResult.

multipleObservers

Logical kind: observerCommunicationConsistency.

Required predecessor routes: none.

Ordered inference steps: stateObserversSetup, supplyObserversCalculation, deriveObserversResult.

Exported conclusions: observersResult.

qualifiedConclusion

Logical kind: interpretiveScope.

Required predecessor routes: pureWaveTheory, statisticalTypicality, multipleObservers.

Ordered inference steps: supplyConclusionBridge, deriveConclusionSetup, supplyConclusionCalculation, deriveConclusionResult.

Exported conclusions: conclusionResult.