import PhysicsLogic.Philosophy.Observer import PhysicsLogic.Philosophy.ProbabilityRoles import PhysicsLogic.Paradigm.QuantumInterpretiveCommitments import PhysicsLogic.Framework.LinearRelativeStateMeasurement import Mathlib.Analysis.SpecificLimits.Basic import Mathlib.Data.Real.Basic import Mathlib.Tactic.NormNum /-! # Formal Logic of Everett 1957 This module parses Hugh Everett III's *"Relative State" Formulation of Quantum Mechanics*. It separates the paper's logical routes: * the external-observation formulation does not apply to a closed system containing its observers; * pure linear wave mechanics is proposed as a complete internal theory; * interacting subsystems have relative rather than independent absolute states; * a calibrated measurement of a superposition produces correlated observer-record branches without selecting one global outcome; * repeated observations produce branch-relative repeatability and a branching memory tree; * positivity, phase insensitivity, additivity, and branching conservation restrict the branch measure to square amplitude; * the product-measure and limiting calculations recover Process-1 statistics for almost all memory sequences; * communication and further interventions reproduce the paper's multi-observer consistency claims. Hilbert-space decompositions, the uniqueness calculation for the measure, and the limiting probability theorem remain explicit theorem hypotheses. -/ set_option autoImplicit false namespace PhysicsLogic.Papers.Everett1957 open PhysicsLogic.Philosophy.Observer open PhysicsLogic.Philosophy.ProbabilityRoles open PhysicsLogic.Paradigm.QuantumInterpretiveCommitments open PhysicsLogic.Framework universe u structure EverettTypes where Description : Type u State : Type u System : Type u Dynamics : Type u Interaction : Type u Branch : Type u Record : Type u Observable : Type u Value : Type u Regime : Type u Coefficient : Type u BranchMeasure : Type u MemorySequence : Type u SequenceSet : Type u /-- The normalized two-subsystem expansion on p. 456, with distinct conditional subsystem states and no independently assigned absolute state. -/ structure OriginalRelativeSubsystemReadout where firstFirstCoefficientValue : Real firstSecondCoefficientValue : Real secondFirstCoefficientValue : Real secondSecondCoefficientValue : Real firstRelativeNormalizationValue : Real secondRelativeNormalizationValue : Real firstRelativeFirstComponentValue : Real firstRelativeSecondComponentValue : Real secondRelativeFirstComponentValue : Real secondRelativeSecondComponentValue : Real independentlyAssignedAbsoluteStateCountValue : Nat namespace OriginalRelativeSubsystemReadout def HasOriginalNormalizedNonfactorizableCompositeExpansion (readout : OriginalRelativeSubsystemReadout) : Prop := 0 < readout.firstFirstCoefficientValue ∧ 0 < readout.secondSecondCoefficientValue ∧ readout.firstFirstCoefficientValue ^ 2 + readout.firstSecondCoefficientValue ^ 2 + readout.secondFirstCoefficientValue ^ 2 + readout.secondSecondCoefficientValue ^ 2 = 1 ∧ readout.firstFirstCoefficientValue * readout.secondSecondCoefficientValue - readout.firstSecondCoefficientValue * readout.secondFirstCoefficientValue ≠ 0 def HasOriginalDistinctNormalizedRelativeStates (readout : OriginalRelativeSubsystemReadout) : Prop := 0 < readout.firstRelativeNormalizationValue ∧ 0 < readout.secondRelativeNormalizationValue ∧ readout.firstRelativeNormalizationValue ^ 2 = readout.firstFirstCoefficientValue ^ 2 + readout.firstSecondCoefficientValue ^ 2 ∧ readout.secondRelativeNormalizationValue ^ 2 = readout.secondFirstCoefficientValue ^ 2 + readout.secondSecondCoefficientValue ^ 2 ∧ readout.firstRelativeFirstComponentValue = readout.firstFirstCoefficientValue / readout.firstRelativeNormalizationValue ∧ readout.firstRelativeSecondComponentValue = readout.firstSecondCoefficientValue / readout.firstRelativeNormalizationValue ∧ readout.secondRelativeFirstComponentValue = readout.secondFirstCoefficientValue / readout.secondRelativeNormalizationValue ∧ readout.secondRelativeSecondComponentValue = readout.secondSecondCoefficientValue / readout.secondRelativeNormalizationValue ∧ readout.firstRelativeFirstComponentValue ≠ readout.secondRelativeFirstComponentValue ∧ readout.independentlyAssignedAbsoluteStateCountValue = 0 def RetainsOriginalCompositeExpansionAndRelativeSubsystemStates (readout : OriginalRelativeSubsystemReadout) : Prop := readout.HasOriginalNormalizedNonfactorizableCompositeExpansion ∧ readout.HasOriginalDistinctNormalizedRelativeStates noncomputable def physicalThreeFifthsFourFifthsRelativeStates : OriginalRelativeSubsystemReadout where firstFirstCoefficientValue := 3 / 5 firstSecondCoefficientValue := 0 secondFirstCoefficientValue := 0 secondSecondCoefficientValue := 4 / 5 firstRelativeNormalizationValue := 3 / 5 secondRelativeNormalizationValue := 4 / 5 firstRelativeFirstComponentValue := 1 firstRelativeSecondComponentValue := 0 secondRelativeFirstComponentValue := 0 secondRelativeSecondComponentValue := 1 independentlyAssignedAbsoluteStateCountValue := 0 theorem original_unequal_composite_coefficients_have_distinct_normalized_relative_states : physicalThreeFifthsFourFifthsRelativeStates |>.RetainsOriginalCompositeExpansionAndRelativeSubsystemStates := by norm_num [RetainsOriginalCompositeExpansionAndRelativeSubsystemStates, HasOriginalNormalizedNonfactorizableCompositeExpansion, HasOriginalDistinctNormalizedRelativeStates, physicalThreeFifthsFourFifthsRelativeStates] rfl end OriginalRelativeSubsystemReadout /-- Equations (10)-(12) retain actual calibration, coefficient-preserving linear branching, branch-relative records, phase freedom, and no collapse. -/ structure OriginalCalibratedBranchMemoryReadout where firstInputAmplitudeValue : Real secondInputAmplitudeValue : Real firstOutputAmplitudeValue : Real secondOutputAmplitudeValue : Real firstObjectOutcomeValue : Nat secondObjectOutcomeValue : Nat firstObserverRecordValue : Nat secondObserverRecordValue : Nat firstRepeatedRecordValue : Nat secondRepeatedRecordValue : Nat unmatchedRecordCountValue : Nat retainedBranchCountValue : Nat globallySelectedOutcomeCountValue : Nat firstBranchWeightValue : Real secondBranchWeightValue : Real phaseReversedFirstAmplitudeValue : Real phaseReversedFirstWeightValue : Real namespace OriginalCalibratedBranchMemoryReadout def HasOriginalEigenstateCalibrationAndLinearCorrelation (readout : OriginalCalibratedBranchMemoryReadout) : Prop := readout.firstObjectOutcomeValue ≠ readout.secondObjectOutcomeValue ∧ readout.firstOutputAmplitudeValue = readout.firstInputAmplitudeValue ∧ readout.secondOutputAmplitudeValue = readout.secondInputAmplitudeValue ∧ readout.firstObserverRecordValue = readout.firstObjectOutcomeValue ∧ readout.secondObserverRecordValue = readout.secondObjectOutcomeValue ∧ readout.unmatchedRecordCountValue = 0 ∧ readout.retainedBranchCountValue = 2 def HasOriginalRepeatedRelativeRecordsWithoutGlobalSelection (readout : OriginalCalibratedBranchMemoryReadout) : Prop := readout.firstObserverRecordValue ≠ readout.secondObserverRecordValue ∧ readout.firstRepeatedRecordValue = readout.firstObserverRecordValue ∧ readout.secondRepeatedRecordValue = readout.secondObserverRecordValue ∧ readout.globallySelectedOutcomeCountValue = 0 def HasOriginalPhaseInsensitiveUnequalSquareAmplitudeWeights (readout : OriginalCalibratedBranchMemoryReadout) : Prop := readout.firstBranchWeightValue = readout.firstInputAmplitudeValue ^ 2 ∧ readout.secondBranchWeightValue = readout.secondInputAmplitudeValue ^ 2 ∧ readout.firstBranchWeightValue + readout.secondBranchWeightValue = 1 ∧ readout.firstBranchWeightValue ≠ readout.secondBranchWeightValue ∧ readout.phaseReversedFirstAmplitudeValue = -readout.firstInputAmplitudeValue ∧ readout.phaseReversedFirstWeightValue = readout.phaseReversedFirstAmplitudeValue ^ 2 ∧ readout.phaseReversedFirstWeightValue = readout.firstBranchWeightValue def RetainsOriginalLinearBranchMemoryAndUnequalWeights (readout : OriginalCalibratedBranchMemoryReadout) : Prop := readout.HasOriginalEigenstateCalibrationAndLinearCorrelation ∧ readout.HasOriginalRepeatedRelativeRecordsWithoutGlobalSelection ∧ readout.HasOriginalPhaseInsensitiveUnequalSquareAmplitudeWeights noncomputable def physicalUnequalTwoBranchObserverMemory : OriginalCalibratedBranchMemoryReadout where firstInputAmplitudeValue := 3 / 5 secondInputAmplitudeValue := 4 / 5 firstOutputAmplitudeValue := 3 / 5 secondOutputAmplitudeValue := 4 / 5 firstObjectOutcomeValue := 0 secondObjectOutcomeValue := 1 firstObserverRecordValue := 0 secondObserverRecordValue := 1 firstRepeatedRecordValue := 0 secondRepeatedRecordValue := 1 unmatchedRecordCountValue := 0 retainedBranchCountValue := 2 globallySelectedOutcomeCountValue := 0 firstBranchWeightValue := 9 / 25 secondBranchWeightValue := 16 / 25 phaseReversedFirstAmplitudeValue := -(3 / 5) phaseReversedFirstWeightValue := 9 / 25 theorem original_two_retained_observer_branches_have_unequal_phase_insensitive_weights : physicalUnequalTwoBranchObserverMemory |>.RetainsOriginalLinearBranchMemoryAndUnequalWeights := by norm_num [RetainsOriginalLinearBranchMemoryAndUnequalWeights, HasOriginalEigenstateCalibrationAndLinearCorrelation, HasOriginalRepeatedRelativeRecordsWithoutGlobalSelection, HasOriginalPhaseInsensitiveUnequalSquareAmplitudeWeights, physicalUnequalTwoBranchObserverMemory] rfl end OriginalCalibratedBranchMemoryReadout /-- Equations (33)-(34) give product measure rather than branch counting; positive-measure finite exceptional sequences are not deleted. -/ structure OriginalFiniteProductMeasureReadout where firstOutcomeWeightValue : Real secondOutcomeWeightValue : Real firstFirstSequenceWeightValue : Real firstSecondSequenceWeightValue : Real secondFirstSequenceWeightValue : Real secondSecondSequenceWeightValue : Real totalSequenceWeightValue : Real mixedSequenceWeightValue : Real totalSequenceCountValue : Nat mixedSequenceCountValue : Nat branchCountingMixedFractionValue : Real selectedSequenceLengthValue : Nat selectedFirstOutcomeCountValue : Nat selectedFirstOutcomeFrequencyValue : Real frequencyToleranceValue : Real finiteExceptionalSequenceCountValue : Nat finiteExceptionalMeasureValue : Real laterExceptionalMeasureValue : Real limitingExceptionalMeasureValue : Real exceptionalTailValueAt : Nat → Real namespace OriginalFiniteProductMeasureReadout def HasOriginalNormalizedTwoObservationProductMeasures (readout : OriginalFiniteProductMeasureReadout) : Prop := 0 < readout.firstOutcomeWeightValue ∧ 0 < readout.secondOutcomeWeightValue ∧ readout.firstOutcomeWeightValue + readout.secondOutcomeWeightValue = 1 ∧ readout.firstFirstSequenceWeightValue = readout.firstOutcomeWeightValue ^ 2 ∧ readout.firstSecondSequenceWeightValue = readout.firstOutcomeWeightValue * readout.secondOutcomeWeightValue ∧ readout.secondFirstSequenceWeightValue = readout.secondOutcomeWeightValue * readout.firstOutcomeWeightValue ∧ readout.secondSecondSequenceWeightValue = readout.secondOutcomeWeightValue ^ 2 ∧ readout.totalSequenceWeightValue = readout.firstFirstSequenceWeightValue + readout.firstSecondSequenceWeightValue + readout.secondFirstSequenceWeightValue + readout.secondSecondSequenceWeightValue ∧ readout.totalSequenceWeightValue = 1 def HasOriginalBranchMeasureDistinctFromBranchCounting (readout : OriginalFiniteProductMeasureReadout) : Prop := readout.totalSequenceCountValue = 4 ∧ readout.mixedSequenceCountValue = 2 ∧ readout.branchCountingMixedFractionValue = (readout.mixedSequenceCountValue : Real) / readout.totalSequenceCountValue ∧ readout.mixedSequenceWeightValue = readout.firstSecondSequenceWeightValue + readout.secondFirstSequenceWeightValue ∧ readout.mixedSequenceWeightValue ≠ readout.branchCountingMixedFractionValue /-- At the selected two-observation depth, only the all-first history lies outside the chosen frequency tolerance; the other three histories do not. -/ def HasOriginalTwoObservationExceptionalClassification (readout : OriginalFiniteProductMeasureReadout) : Prop := readout.selectedSequenceLengthValue = 2 ∧ |(0 : Real) - readout.firstOutcomeWeightValue| ≤ readout.frequencyToleranceValue ∧ |(1 : Real) / readout.selectedSequenceLengthValue - readout.firstOutcomeWeightValue| ≤ readout.frequencyToleranceValue ∧ readout.frequencyToleranceValue < |(readout.selectedSequenceLengthValue : Real) / readout.selectedSequenceLengthValue - readout.firstOutcomeWeightValue| ∧ readout.finiteExceptionalSequenceCountValue = 1 ∧ readout.finiteExceptionalMeasureValue = readout.firstFirstSequenceWeightValue def HasOriginalPositiveFiniteExceptionalSetAndZeroLimit (readout : OriginalFiniteProductMeasureReadout) : Prop := 0 < readout.selectedSequenceLengthValue ∧ readout.selectedFirstOutcomeFrequencyValue = (readout.selectedFirstOutcomeCountValue : Real) / readout.selectedSequenceLengthValue ∧ 0 < readout.frequencyToleranceValue ∧ readout.frequencyToleranceValue < |readout.selectedFirstOutcomeFrequencyValue - readout.firstOutcomeWeightValue| ∧ 0 < readout.finiteExceptionalSequenceCountValue ∧ 0 < readout.finiteExceptionalMeasureValue ∧ readout.finiteExceptionalMeasureValue = readout.firstFirstSequenceWeightValue ∧ 0 < readout.laterExceptionalMeasureValue ∧ readout.laterExceptionalMeasureValue < readout.finiteExceptionalMeasureValue ∧ readout.exceptionalTailValueAt 0 = readout.finiteExceptionalMeasureValue ∧ readout.exceptionalTailValueAt 1 = readout.laterExceptionalMeasureValue ∧ readout.limitingExceptionalMeasureValue = 0 ∧ readout.HasOriginalTwoObservationExceptionalClassification ∧ (∀ length : Nat, readout.exceptionalTailValueAt length = readout.firstOutcomeWeightValue ^ (length + readout.selectedSequenceLengthValue)) ∧ Filter.Tendsto readout.exceptionalTailValueAt Filter.atTop (nhds readout.limitingExceptionalMeasureValue) def RetainsOriginalProductMeasureFiniteExceptionsAndTypicalityLimit (readout : OriginalFiniteProductMeasureReadout) : Prop := readout.HasOriginalNormalizedTwoObservationProductMeasures ∧ readout.HasOriginalBranchMeasureDistinctFromBranchCounting ∧ readout.HasOriginalPositiveFiniteExceptionalSetAndZeroLimit noncomputable def physicalUnequalTwoObservationProductMeasure : OriginalFiniteProductMeasureReadout where firstOutcomeWeightValue := 9 / 25 secondOutcomeWeightValue := 16 / 25 firstFirstSequenceWeightValue := 81 / 625 firstSecondSequenceWeightValue := 144 / 625 secondFirstSequenceWeightValue := 144 / 625 secondSecondSequenceWeightValue := 256 / 625 totalSequenceWeightValue := 1 mixedSequenceWeightValue := 288 / 625 totalSequenceCountValue := 4 mixedSequenceCountValue := 2 branchCountingMixedFractionValue := 1 / 2 selectedSequenceLengthValue := 2 selectedFirstOutcomeCountValue := 2 selectedFirstOutcomeFrequencyValue := 1 frequencyToleranceValue := 1 / 2 finiteExceptionalSequenceCountValue := 1 finiteExceptionalMeasureValue := 81 / 625 laterExceptionalMeasureValue := 729 / 15625 limitingExceptionalMeasureValue := 0 exceptionalTailValueAt := fun length => (9 / 25 : Real) ^ (length + 2) theorem original_product_measure_differs_from_branch_counting_and_retains_finite_exceptions : physicalUnequalTwoObservationProductMeasure |>.RetainsOriginalProductMeasureFiniteExceptionsAndTypicalityLimit := by have exceptionalTailLimit : Filter.Tendsto (fun length : Nat => (9 / 25 : Real) ^ (length + 2)) Filter.atTop (nhds 0) := by have geometricLimit := tendsto_pow_atTop_nhds_zero_of_lt_one (show (0 : Real) ≤ 9 / 25 by norm_num) (show (9 / 25 : Real) < 1 by norm_num) have shiftedLimit := geometricLimit.mul (tendsto_const_nhds (x := (9 / 25 : Real) ^ 2)) simpa [pow_add] using shiftedLimit norm_num [RetainsOriginalProductMeasureFiniteExceptionsAndTypicalityLimit, HasOriginalNormalizedTwoObservationProductMeasures, HasOriginalBranchMeasureDistinctFromBranchCounting, HasOriginalTwoObservationExceptionalClassification, HasOriginalPositiveFiniteExceptionalSetAndZeroLimit, physicalUnequalTwoObservationProductMeasure, abs_of_pos] exact ⟨⟨rfl, rfl⟩, exceptionalTailLimit⟩ /-- The reconstructed exceptional tail genuinely converges to zero but remains strictly positive at every finite observation depth. -/ theorem original_selected_exceptional_tail_is_positive_at_every_finite_depth : ∀ length : Nat, 0 < physicalUnequalTwoObservationProductMeasure.exceptionalTailValueAt length := by intro length dsimp [physicalUnequalTwoObservationProductMeasure] positivity end OriginalFiniteProductMeasureReadout /-- Pages 461-462 distinguish ordinary observer agreement, disturbance by a noncommuting local observation, and an undisturbed remote intervention. -/ structure OriginalObserverInterventionReadout where firstCommunicatedRecordValue : Nat secondCommunicatedRecordValue : Nat uninterruptedFirstRecordValue : Nat uninterruptedRepeatedRecordValue : Nat localNoncommutingFirstRecordValue : Nat localNoncommutingRepeatedRecordValue : Nat localCommutatorResidualValue : Real remoteInteractionStrengthValue : Real remoteFirstRecordValue : Nat remoteRepeatedRecordValue : Nat namespace OriginalObserverInterventionReadout def HasOriginalCommunicatingObserverAgreement (readout : OriginalObserverInterventionReadout) : Prop := readout.firstCommunicatedRecordValue = readout.secondCommunicatedRecordValue ∧ readout.uninterruptedFirstRecordValue = readout.uninterruptedRepeatedRecordValue def HasOriginalNoncommutingLocalDisturbance (readout : OriginalObserverInterventionReadout) : Prop := readout.localCommutatorResidualValue ≠ 0 ∧ readout.localNoncommutingFirstRecordValue ≠ readout.localNoncommutingRepeatedRecordValue def HasOriginalRemoteNoninteractionAndUndisturbedRepeat (readout : OriginalObserverInterventionReadout) : Prop := readout.remoteInteractionStrengthValue = 0 ∧ readout.remoteFirstRecordValue = readout.remoteRepeatedRecordValue def RetainsOriginalAgreementLocalDisturbanceAndRemoteNoninteraction (readout : OriginalObserverInterventionReadout) : Prop := readout.HasOriginalCommunicatingObserverAgreement ∧ readout.HasOriginalNoncommutingLocalDisturbance ∧ readout.HasOriginalRemoteNoninteractionAndUndisturbedRepeat def physicalCommunicatingLocalAndRemoteObservers : OriginalObserverInterventionReadout where firstCommunicatedRecordValue := 1 secondCommunicatedRecordValue := 1 uninterruptedFirstRecordValue := 0 uninterruptedRepeatedRecordValue := 0 localNoncommutingFirstRecordValue := 0 localNoncommutingRepeatedRecordValue := 1 localCommutatorResidualValue := 1 remoteInteractionStrengthValue := 0 remoteFirstRecordValue := 0 remoteRepeatedRecordValue := 0 theorem original_noncommuting_observation_disturbs_local_repeat_but_remote_observation_does_not : physicalCommunicatingLocalAndRemoteObservers |>.RetainsOriginalAgreementLocalDisturbanceAndRemoteNoninteraction := by norm_num [RetainsOriginalAgreementLocalDisturbanceAndRemoteNoninteraction, HasOriginalCommunicatingObserverAgreement, HasOriginalNoncommutingLocalDisturbance, HasOriginalRemoteNoninteractionAndUndisturbedRepeat, physicalCommunicatingLocalAndRemoteObservers] end OriginalObserverInterventionReadout /-- Original 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 SquareAmplitudeFormulaReadout where normalizationConstantValue : Real selectedAmplitudeSquaredValue : Real selectedMeasureValue : Real firstComponentAmplitudeSquaredValue : Real secondComponentAmplitudeSquaredValue : Real compositeAmplitudeSquaredValue : Real firstComponentMeasureValue : Real secondComponentMeasureValue : Real compositeMeasureValue : Real namespace SquareAmplitudeFormulaReadout /-- The 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. -/ def FormulaDomainAt (readout : SquareAmplitudeFormulaReadout) : Prop := 0 < readout.normalizationConstantValue /\ 0 <= readout.selectedAmplitudeSquaredValue /\ 0 <= readout.firstComponentAmplitudeSquaredValue /\ 0 <= readout.secondComponentAmplitudeSquaredValue /\ 0 <= readout.compositeAmplitudeSquaredValue /\ readout.compositeAmplitudeSquaredValue = readout.firstComponentAmplitudeSquaredValue + readout.secondComponentAmplitudeSquaredValue /-- The p. 460 additivity equation represented by equations (27)-(30): the measure of the composite orthogonal component is the sum of the component measures. -/ def EquationTwentySevenAdditivityAt (readout : SquareAmplitudeFormulaReadout) : Prop := readout.compositeMeasureValue = readout.firstComponentMeasureValue + readout.secondComponentMeasureValue /-- Journal p. 460, equation (31), retained for the selected coefficient and the two component coefficients used in the additivity step: `m(a) = c |a|^2`. -/ def EquationThirtyOneSquareAmplitudeAt (readout : SquareAmplitudeFormulaReadout) : Prop := readout.selectedMeasureValue = readout.normalizationConstantValue * readout.selectedAmplitudeSquaredValue /\ readout.firstComponentMeasureValue = readout.normalizationConstantValue * readout.firstComponentAmplitudeSquaredValue /\ readout.secondComponentMeasureValue = readout.normalizationConstantValue * readout.secondComponentAmplitudeSquaredValue /\ readout.compositeMeasureValue = readout.normalizationConstantValue * readout.compositeAmplitudeSquaredValue def SourceFormulaAt (readout : SquareAmplitudeFormulaReadout) : Prop := readout.FormulaDomainAt /\ readout.EquationTwentySevenAdditivityAt /\ readout.EquationThirtyOneSquareAmplitudeAt /-- Equations (27)-(31) retain both the orthogonal additivity equation and the square-amplitude value assigned to the selected coefficient. -/ theorem equations_twenty_seven_through_thirty_one_retain_square_amplitude_additivity (readout : SquareAmplitudeFormulaReadout) (formulas : readout.SourceFormulaAt) : readout.compositeMeasureValue = readout.firstComponentMeasureValue + readout.secondComponentMeasureValue /\ readout.selectedMeasureValue = readout.normalizationConstantValue * readout.selectedAmplitudeSquaredValue := by rcases formulas with ⟨_domain, additivity, squareAmplitude⟩ exact ⟨additivity, squareAmplitude.1⟩ noncomputable def physicalUnequalNormalizedSquareAmplitudeMeasure : SquareAmplitudeFormulaReadout where normalizationConstantValue := 1 selectedAmplitudeSquaredValue := 9 / 25 selectedMeasureValue := 9 / 25 firstComponentAmplitudeSquaredValue := 9 / 25 secondComponentAmplitudeSquaredValue := 16 / 25 compositeAmplitudeSquaredValue := 1 firstComponentMeasureValue := 9 / 25 secondComponentMeasureValue := 16 / 25 compositeMeasureValue := 1 theorem original_normalized_square_amplitude_measure_has_unequal_branch_weights : physicalUnequalNormalizedSquareAmplitudeMeasure.SourceFormulaAt ∧ physicalUnequalNormalizedSquareAmplitudeMeasure.firstComponentMeasureValue ≠ physicalUnequalNormalizedSquareAmplitudeMeasure.secondComponentMeasureValue := by norm_num [SourceFormulaAt, FormulaDomainAt, EquationTwentySevenAdditivityAt, EquationThirtyOneSquareAmplitudeAt, physicalUnequalNormalizedSquareAmplitudeMeasure] rfl namespace Countermodels def NamedSquareAmplitudeMeasureAt (readout : SquareAmplitudeFormulaReadout) : Prop := 0 < readout.normalizationConstantValue ∧ 0 ≤ readout.selectedAmplitudeSquaredValue ∧ 0 ≤ readout.selectedMeasureValue ∧ readout.compositeMeasureValue = readout.firstComponentMeasureValue + readout.secondComponentMeasureValue def wrongNamedSquareAmplitudeMeasure : SquareAmplitudeFormulaReadout where normalizationConstantValue := 1 selectedAmplitudeSquaredValue := 1 selectedMeasureValue := 0 firstComponentAmplitudeSquaredValue := 1 secondComponentAmplitudeSquaredValue := 1 compositeAmplitudeSquaredValue := 2 firstComponentMeasureValue := 1 secondComponentMeasureValue := 1 compositeMeasureValue := 2 /-- A 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. -/ theorem named_square_amplitude_measure_does_not_supply_equations_twenty_seven_through_thirty_one : NamedSquareAmplitudeMeasureAt wrongNamedSquareAmplitudeMeasure /\ wrongNamedSquareAmplitudeMeasure.EquationTwentySevenAdditivityAt /\ ¬wrongNamedSquareAmplitudeMeasure.SourceFormulaAt := by refine ⟨?_, ?_, ?_⟩ · norm_num [NamedSquareAmplitudeMeasureAt, wrongNamedSquareAmplitudeMeasure] · norm_num [EquationTwentySevenAdditivityAt, wrongNamedSquareAmplitudeMeasure] intro formulas have squareAmplitude := formulas.2.2.1 norm_num [EquationThirtyOneSquareAmplitudeAt, wrongNamedSquareAmplitudeMeasure] at squareAmplitude end Countermodels end SquareAmplitudeFormulaReadout /-- Paper-local semantic vocabulary. Fields are physical data or proposition-valued relations; none supplies a proof of a desired conclusion. -/ structure RelativeStateFramework (T : EverettTypes) where universalDescription : T.Description externalObserverDescription : T.Description processTwoDynamics : T.Dynamics universeSystem : T.System compositeSystem : T.System objectSystem : T.System observerSystem : T.System secondObserverSystem : T.System remoteSystem : T.System measurementInteraction : T.Interaction repeatInteraction : T.Interaction communicationInteraction : T.Interaction noncommutingIntervention : T.Interaction remoteMeasurementInteraction : T.Interaction initialCompositeState : T.State initialObjectState : T.State firstEigenstate : T.State secondEigenstate : T.State initialObserverState : T.State firstObserverState : T.State secondObserverState : T.State correlatedMeasurementState : T.State repeatedMeasurementState : T.State multipleObserverState : T.State firstBranch : T.Branch secondBranch : T.Branch firstRecord : T.Record secondRecord : T.Record firstRepeatedRecord : T.Record secondRepeatedRecord : T.Record selectedObservable : T.Observable noncommutingObservable : T.Observable firstValue : T.Value secondValue : T.Value universalObservableSector : T.Observable → Prop firstCoefficient : T.Coefficient secondCoefficient : T.Coefficient selectedMeasure : T.BranchMeasure firstMemorySequence : T.MemorySequence secondMemorySequence : T.MemorySequence exceptionalSequences : T.SequenceSet squareAmplitudeFormulaReadout : SquareAmplitudeFormulaReadout originalRelativeSubsystemReadout : OriginalRelativeSubsystemReadout originalCalibratedBranchMemoryReadout : OriginalCalibratedBranchMemoryReadout originalFiniteProductMeasureReadout : OriginalFiniteProductMeasureReadout originalObserverInterventionReadout : OriginalObserverInterventionReadout objectAmplitudesAt : T.State -> Bool -> Complex measuredRecordCoefficientsAt : T.State -> CoherentRecordMeasurement.JointState Bool comparedRecordCoefficientsAt : T.State -> CoherentRecordMeasurement.ComparedState Bool recordMeasurementMapAt : T.Interaction -> (Bool -> Complex) →ₗ[Complex] CoherentRecordMeasurement.JointState Bool recordCommunicationMapAt : T.Interaction -> CoherentRecordMeasurement.JointState Bool →ₗ[Complex] CoherentRecordMeasurement.ComparedState Bool selectedComparisonConfiguration : Bool × Bool × Bool squareAmplitudeFormulaRepresentsAt : SquareAmplitudeFormulaReadout -> T.Coefficient -> T.Coefficient -> T.BranchMeasure -> T.Value -> T.Value -> Prop closedRegime : T.Regime measurementRegime : T.Regime repeatedObservationRegime : T.Regime asymptoticRegime : T.Regime multipleObserverRegime : T.Regime isolatedSystem : T.System → T.Regime → Prop systemContainsObserver : T.System → T.System → T.Regime → Prop externalObservationAvailable : T.System → T.Regime → Prop processOneApplicable : T.System → T.Regime → Prop approximateMeasurementCoveredGenerally : T.Description → T.Regime → Prop closedUniverseCoveredBy : T.Description → T.Regime → Prop waveFunctionDescribes : T.Description → T.System → T.Regime → Prop obeysLinearWaveEquation : T.Dynamics → T.Regime → Prop stateFunctionEvolvesContinuouslyAt : T.Description → T.Dynamics → T.System → T.Regime → Prop completeMathematicalModelFor : T.Description → T.System → T.Regime → Prop externalSystemEmbeddedInLargerIsolatedSystem : T.System → T.Regime → Prop compositeStateOf : T.State → T.System → T.Regime → Prop subsystemOf : T.System → T.System → Prop absoluteStateAssigned : T.State → T.System → T.State → T.Regime → Prop relativeStateAssigned : T.State → T.System → T.State → T.System → T.State → T.Regime → Prop relativeStateUnique : T.State → T.System → T.State → T.System → T.Regime → Prop subsystemStatesCorrelated : T.State → T.System → T.System → T.Regime → Prop calibratedOn : T.Interaction → T.State → T.State → T.State → T.Record → T.Branch → T.Regime → Prop inputSuperposes : T.State → T.State → T.State → T.Regime → Prop linearEvolutionApplies : T.Dynamics → T.Interaction → T.Regime → Prop stateContainsBranch : T.State → T.Branch → T.Regime → Prop branchCorrelates : T.State → T.Branch → T.State → T.State → T.Record → T.Regime → Prop recordDefiniteRelativeTo : T.Record → T.State → T.Branch → T.Regime → Prop globallySelectsSingleOutcome : T.State → T.Regime → Prop secondObservationOfSameQuantity : T.Interaction → T.Observable → T.System → T.Regime → Prop recordSequenceInBranch : T.Record → T.Record → T.Branch → T.State → T.Regime → Prop recordsAgreeWithinBranch : T.Record → T.Record → T.Branch → T.Regime → Prop observerMemoryFormsBranchingTree : T.System → T.State → T.Regime → Prop allBranchesSimultaneouslyRetained : T.State → T.Regime → Prop possibleToActualTransitionOccurs : T.State → T.Regime → Prop measurePositive : T.BranchMeasure → Prop measurePhaseInsensitive : T.BranchMeasure → Prop measureAdditiveOnOrthogonalComponents : T.BranchMeasure → Prop measureConservedUnderBranching : T.BranchMeasure → Prop measureIsSquareAmplitude : T.BranchMeasure → Prop coefficientHasMeasure : T.Coefficient → T.BranchMeasure → T.Value → Prop sequenceMeasureIsProduct : T.MemorySequence → T.BranchMeasure → Prop processOneIndependentWeightsRecovered : T.BranchMeasure → T.Regime → Prop exceptionalSetHasMeasureTendingToZero : T.SequenceSet → T.BranchMeasure → T.Regime → Prop processOneAveragesHoldOutside : T.SequenceSet → T.BranchMeasure → T.Regime → Prop sequenceOutsideExceptionalSet : T.MemorySequence → T.SequenceSet → Prop processOneAveragesHoldFor : T.MemorySequence → T.BranchMeasure → T.Regime → Prop processOneStatisticsAppearValidToObserver : T.System → T.BranchMeasure → T.Regime → Prop separatelyObservesSameQuantity : T.System → T.System → T.Observable → T.Regime → Prop observersCommunicate : T.Interaction → T.System → T.System → T.Regime → Prop interveningObservationNoncommutes : T.Interaction → T.Observable → T.Observable → T.Regime → Prop repeatCorrelationPreserved : T.System → T.Observable → T.Regime → Prop systemsCorrelatedButNoninteracting : T.System → T.System → T.Regime → Prop remoteObservationChangesLocalRepeatResult : T.Interaction → T.System → T.System → T.Regime → Prop physicallyAdmissible : T.State → T.Regime → Prop representedBy : T.Description → T.State → T.Regime → Prop physicalSystem : T.System → Prop observerSystemPredicate : T.System → Prop governs : T.Dynamics → T.System → T.Regime → Prop linearEvolution : T.Dynamics → T.Regime → Prop fundamentalCollapse : T.Dynamics → T.Regime → Prop branchComponent : T.Branch → T.Description → T.Regime → Prop branchRetained : T.Branch → T.Description → T.Regime → Prop systemInBranch : T.System → T.Branch → T.Description → T.Regime → Prop recordInBranch : T.Record → T.Branch → T.Description → T.Regime → Prop recordDefiniteFor : T.Record → T.System → T.Regime → Prop inductive EverettRelativeMeasurementTheory where | universalProcessTwoMeasurement deriving DecidableEq, Repr inductive EverettRelativeMeasurementWorld where | selectedObserverMeasurement deriving DecidableEq, Repr namespace RelativeStateFramework def recordProcess {T : EverettTypes} (framework : RelativeStateFramework T) : CoherentRecordMeasurement.Process Bool where inputAmplitude := framework.objectAmplitudesAt framework.initialObjectState measurement := framework.recordMeasurementMapAt framework.measurementInteraction communication := framework.recordCommunicationMapAt framework.communicationInteraction /-- Agreement is a property of the computed supported record configurations, not a supplied observer-agreement predicate. -/ def observerRecordsAgree {T : EverettTypes} (framework : RelativeStateFramework T) (first second : T.System) (observable : T.Observable) (regime : T.Regime) : Prop := first = framework.observerSystem ∧ second = framework.secondObserverSystem ∧ observable = framework.selectedObservable ∧ regime = framework.multipleObserverRegime ∧ framework.measuredRecordCoefficientsAt framework.correlatedMeasurementState = framework.recordProcess.measuredState ∧ framework.comparedRecordCoefficientsAt framework.multipleObserverState = framework.recordProcess.comparedState ∧ framework.recordProcess.NonvacuousRecordComparisonAt variable {T : EverettTypes} def toLinearRelativeStateContext (framework : RelativeStateFramework T) : LinearRelativeStateContext T.Description T.State T.Dynamics T.System T.Branch T.Record T.Regime where completeness := { physicallyAdmissible := framework.physicallyAdmissible representedBy := framework.representedBy } physicalSystem := framework.physicalSystem observerSystem := framework.observerSystemPredicate governs := framework.governs linearEvolution := framework.linearEvolution fundamentalCollapse := framework.fundamentalCollapse branchComponent := framework.branchComponent branchRetained := framework.branchRetained systemInBranch := framework.systemInBranch recordInBranch := framework.recordInBranch recordDefiniteFor := framework.recordDefiniteFor /-- Pages 455 and 457 use physical systems with memory. Their physical observer role does not require a separate classification of consciousness. -/ def observerRoleContext (framework : RelativeStateFramework T) : PhysicsLogic.Philosophy.Observer.PhysicalObserverRoleContext T.System Unit where physicalSystemAt := fun system _ => framework.physicalSystem system observerSystemAt := fun system _ => framework.observerSystemPredicate system theorem physical_observer_role_iff_declared_role_and_physical_system (framework : RelativeStateFramework T) (observer : T.System) : framework.observerRoleContext.PhysicalObserverAt observer () ↔ framework.observerSystemPredicate observer ∧ framework.physicalSystem observer := Iff.rfl def ExternalObservationProblemSetup (framework : RelativeStateFramework T) : Prop := framework.isolatedSystem framework.universeSystem framework.closedRegime ∧ framework.systemContainsObserver framework.universeSystem framework.observerSystem framework.closedRegime ∧ framework.observerSystemPredicate framework.observerSystem ∧ framework.physicalSystem framework.observerSystem theorem closed_system_setup_realizes_physical_observer_role (framework : RelativeStateFramework T) (setup : framework.ExternalObservationProblemSetup) : framework.observerRoleContext.PhysicalObserverAt framework.observerSystem () := ⟨setup.2.2.1, setup.2.2.2⟩ def ExternalObservationLimitation (framework : RelativeStateFramework T) : Prop := framework.ExternalObservationProblemSetup → ¬framework.externalObservationAvailable framework.universeSystem framework.closedRegime ∧ ¬framework.processOneApplicable framework.universeSystem framework.closedRegime ∧ ¬framework.approximateMeasurementCoveredGenerally framework.externalObserverDescription framework.closedRegime ∧ ¬framework.closedUniverseCoveredBy framework.externalObserverDescription framework.closedRegime theorem external_observation_formulation_does_not_cover_closed_observer_systems (framework : RelativeStateFramework T) (setup : framework.ExternalObservationProblemSetup) (limitation : framework.ExternalObservationLimitation) : ¬framework.externalObservationAvailable framework.universeSystem framework.closedRegime ∧ ¬framework.processOneApplicable framework.universeSystem framework.closedRegime ∧ ¬framework.approximateMeasurementCoveredGenerally framework.externalObserverDescription framework.closedRegime ∧ ¬framework.closedUniverseCoveredBy framework.externalObserverDescription framework.closedRegime := limitation setup def PureWaveTheorySetup (framework : RelativeStateFramework T) : Prop := framework.waveFunctionDescribes framework.universalDescription framework.universeSystem framework.closedRegime ∧ framework.obeysLinearWaveEquation framework.processTwoDynamics framework.closedRegime ∧ framework.externalSystemEmbeddedInLargerIsolatedSystem framework.compositeSystem framework.closedRegime def PureWaveCompletionCalculation (framework : RelativeStateFramework T) : Prop := framework.PureWaveTheorySetup → framework.completeMathematicalModelFor framework.universalDescription framework.universeSystem framework.closedRegime ∧ framework.toLinearRelativeStateContext.completeness.CompleteAt framework.universalDescription framework.closedRegime ∧ framework.linearEvolution framework.processTwoDynamics framework.closedRegime ∧ framework.toLinearRelativeStateContext.UniversalDynamicsAt framework.processTwoDynamics framework.closedRegime ∧ ¬framework.fundamentalCollapse framework.processTwoDynamics framework.closedRegime theorem pure_process_two_supplies_the_internal_closed_system_theory (framework : RelativeStateFramework T) (setup : framework.PureWaveTheorySetup) (calculation : framework.PureWaveCompletionCalculation) : framework.completeMathematicalModelFor framework.universalDescription framework.universeSystem framework.closedRegime ∧ framework.toLinearRelativeStateContext.completeness.CompleteAt framework.universalDescription framework.closedRegime ∧ framework.linearEvolution framework.processTwoDynamics framework.closedRegime ∧ framework.toLinearRelativeStateContext.UniversalDynamicsAt framework.processTwoDynamics framework.closedRegime ∧ ¬framework.fundamentalCollapse framework.processTwoDynamics framework.closedRegime := calculation setup def RelativeStateSetup (framework : RelativeStateFramework T) : Prop := framework.compositeStateOf framework.initialCompositeState framework.compositeSystem framework.closedRegime ∧ framework.subsystemOf framework.objectSystem framework.compositeSystem ∧ framework.subsystemOf framework.observerSystem framework.compositeSystem def RelativeStateCalculation (framework : RelativeStateFramework T) : Prop := framework.RelativeStateSetup → ¬framework.absoluteStateAssigned framework.initialCompositeState framework.objectSystem framework.initialObjectState framework.closedRegime ∧ framework.relativeStateAssigned framework.initialCompositeState framework.objectSystem framework.firstEigenstate framework.observerSystem framework.firstObserverState framework.closedRegime ∧ framework.relativeStateUnique framework.initialCompositeState framework.objectSystem framework.firstEigenstate framework.observerSystem framework.closedRegime ∧ framework.subsystemStatesCorrelated framework.initialCompositeState framework.objectSystem framework.observerSystem framework.closedRegime ∧ (framework.originalRelativeSubsystemReadout |>.RetainsOriginalCompositeExpansionAndRelativeSubsystemStates) theorem composite_formalism_yields_unique_relative_not_absolute_subsystem_state (framework : RelativeStateFramework T) (setup : framework.RelativeStateSetup) (calculation : framework.RelativeStateCalculation) : ¬framework.absoluteStateAssigned framework.initialCompositeState framework.objectSystem framework.initialObjectState framework.closedRegime ∧ framework.relativeStateAssigned framework.initialCompositeState framework.objectSystem framework.firstEigenstate framework.observerSystem framework.firstObserverState framework.closedRegime ∧ framework.relativeStateUnique framework.initialCompositeState framework.objectSystem framework.firstEigenstate framework.observerSystem framework.closedRegime ∧ framework.subsystemStatesCorrelated framework.initialCompositeState framework.objectSystem framework.observerSystem framework.closedRegime ∧ (framework.originalRelativeSubsystemReadout |>.RetainsOriginalCompositeExpansionAndRelativeSubsystemStates) := calculation setup /-- The p. 456 source route retains the actual normalized coefficient array and both different conditioned subsystem vectors. -/ theorem relative_state_route_retains_original_normalized_conditional_coefficients (framework : RelativeStateFramework T) (setup : framework.RelativeStateSetup) (calculation : framework.RelativeStateCalculation) : framework.originalRelativeSubsystemReadout |>.RetainsOriginalCompositeExpansionAndRelativeSubsystemStates := (calculation setup).2.2.2.2 def GoodMeasurementSetup (framework : RelativeStateFramework T) : Prop := framework.firstEigenstate ≠ framework.secondEigenstate ∧ framework.firstObserverState ≠ framework.secondObserverState ∧ framework.firstRecord ≠ framework.secondRecord ∧ framework.firstBranch ≠ framework.secondBranch ∧ framework.calibratedOn framework.measurementInteraction framework.firstEigenstate framework.initialObserverState framework.firstObserverState framework.firstRecord framework.firstBranch framework.measurementRegime ∧ framework.calibratedOn framework.measurementInteraction framework.secondEigenstate framework.initialObserverState framework.secondObserverState framework.secondRecord framework.secondBranch framework.measurementRegime ∧ framework.inputSuperposes framework.initialObjectState framework.firstEigenstate framework.secondEigenstate framework.measurementRegime ∧ framework.linearEvolutionApplies framework.processTwoDynamics framework.measurementInteraction framework.measurementRegime def LinearMeasurementCalculation (framework : RelativeStateFramework T) : Prop := framework.GoodMeasurementSetup → framework.stateContainsBranch framework.correlatedMeasurementState framework.firstBranch framework.measurementRegime ∧ framework.stateContainsBranch framework.correlatedMeasurementState framework.secondBranch framework.measurementRegime ∧ framework.branchCorrelates framework.correlatedMeasurementState framework.firstBranch framework.firstEigenstate framework.firstObserverState framework.firstRecord framework.measurementRegime ∧ framework.branchCorrelates framework.correlatedMeasurementState framework.secondBranch framework.secondEigenstate framework.secondObserverState framework.secondRecord framework.measurementRegime ∧ (framework.originalCalibratedBranchMemoryReadout |>.RetainsOriginalLinearBranchMemoryAndUnequalWeights) def RelativeRecordInterpretation (framework : RelativeStateFramework T) : Prop := framework.GoodMeasurementSetup → framework.branchCorrelates framework.correlatedMeasurementState framework.firstBranch framework.firstEigenstate framework.firstObserverState framework.firstRecord framework.measurementRegime → framework.branchCorrelates framework.correlatedMeasurementState framework.secondBranch framework.secondEigenstate framework.secondObserverState framework.secondRecord framework.measurementRegime → framework.recordDefiniteRelativeTo framework.firstRecord framework.firstObserverState framework.firstBranch framework.measurementRegime ∧ framework.recordDefiniteRelativeTo framework.secondRecord framework.secondObserverState framework.secondBranch framework.measurementRegime ∧ ¬framework.globallySelectsSingleOutcome framework.correlatedMeasurementState framework.measurementRegime theorem linear_measurement_produces_correlated_relative_records_without_selection (framework : RelativeStateFramework T) (setup : framework.GoodMeasurementSetup) (calculation : framework.LinearMeasurementCalculation) (interpretation : framework.RelativeRecordInterpretation) : framework.stateContainsBranch framework.correlatedMeasurementState framework.firstBranch framework.measurementRegime ∧ framework.stateContainsBranch framework.correlatedMeasurementState framework.secondBranch framework.measurementRegime ∧ framework.recordDefiniteRelativeTo framework.firstRecord framework.firstObserverState framework.firstBranch framework.measurementRegime ∧ framework.recordDefiniteRelativeTo framework.secondRecord framework.secondObserverState framework.secondBranch framework.measurementRegime ∧ ¬framework.globallySelectsSingleOutcome framework.correlatedMeasurementState framework.measurementRegime ∧ (framework.originalCalibratedBranchMemoryReadout |>.RetainsOriginalLinearBranchMemoryAndUnequalWeights) := by rcases calculation setup with ⟨firstContained, secondContained, firstCorrelation, secondCorrelation, sourceReadout⟩ rcases interpretation setup firstCorrelation secondCorrelation with ⟨firstDefinite, secondDefinite, noSelection⟩ exact ⟨firstContained, secondContained, firstDefinite, secondDefinite, noSelection, sourceReadout⟩ /-- The actual measurement route preserves both unequal amplitudes, both calibrated records, branch-relative repetition, and absence of selection. -/ theorem measurement_route_retains_original_unequal_relative_memory_branches (framework : RelativeStateFramework T) (setup : framework.GoodMeasurementSetup) (calculation : framework.LinearMeasurementCalculation) : framework.originalCalibratedBranchMemoryReadout |>.RetainsOriginalLinearBranchMemoryAndUnequalWeights := (calculation setup).2.2.2.2 /-! ## Operational observer adapter Everett's pages 455 and 457-458 define model observers as physical systems whose interaction with an object changes a memory into a record correlated with the object state. The adapter therefore realizes an observer role from physical status, calibrated interaction, produced correlation, and available record. It does not use consciousness or the bare `observerSystemPredicate` as sufficient evidence for observation. -/ /-- The 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. -/ def FirstCoherentRecordRealizationInputs (framework : RelativeStateFramework T) : Prop := framework.recordProcess.MeasurementCalibration ∧ framework.measuredRecordCoefficientsAt framework.correlatedMeasurementState = framework.recordProcess.measuredState ∧ framework.recordProcess.inputAmplitude false ≠ 0 def toOperationalObserverContext (framework : RelativeStateFramework T) : OperationalObserverContext T.System T.System T.Interaction T.Record T.Regime where physicalSystemAt := fun system _ => framework.physicalSystem system interactsWithAt := fun interaction observer target regime => framework.recordProcess.MeasurementCalibration ∧ observer = framework.observerSystem ∧ target = framework.objectSystem ∧ (framework.calibratedOn interaction framework.firstEigenstate framework.initialObserverState framework.firstObserverState framework.firstRecord framework.firstBranch regime ∨ framework.calibratedOn interaction framework.secondEigenstate framework.initialObserverState framework.secondObserverState framework.secondRecord framework.secondBranch regime) informationProducedByAt := fun interaction record regime => interaction = framework.measurementInteraction ∧ framework.measuredRecordCoefficientsAt framework.correlatedMeasurementState = framework.recordProcess.measuredState ∧ ((record = framework.firstRecord ∧ framework.branchCorrelates framework.correlatedMeasurementState framework.firstBranch framework.firstEigenstate framework.firstObserverState framework.firstRecord regime ∧ framework.recordProcess.measuredState (false, false) ≠ 0) ∨ (record = framework.secondRecord ∧ framework.branchCorrelates framework.correlatedMeasurementState framework.secondBranch framework.secondEigenstate framework.secondObserverState framework.secondRecord regime ∧ framework.recordProcess.measuredState (true, true) ≠ 0)) informationAvailableToAboutAt := fun record observer target regime => observer = framework.observerSystem ∧ target = framework.objectSystem ∧ ((record = framework.firstRecord ∧ framework.recordDefiniteRelativeTo framework.firstRecord framework.firstObserverState framework.firstBranch regime) ∨ (record = framework.secondRecord ∧ framework.recordDefiniteRelativeTo framework.secondRecord framework.secondObserverState framework.secondBranch regime)) theorem correlated_memory_record_realizes_operational_observer_role (framework : RelativeStateFramework T) (externalSetup : framework.ExternalObservationProblemSetup) (measurementSetup : framework.GoodMeasurementSetup) (calculation : framework.LinearMeasurementCalculation) (interpretation : framework.RelativeRecordInterpretation) (realization : framework.FirstCoherentRecordRealizationInputs) : framework.toOperationalObserverContext.OperationalObserverOfAt framework.observerSystem framework.objectSystem framework.measurementInteraction framework.firstRecord framework.measurementRegime := by have correlations := calculation measurementSetup have records := interpretation measurementSetup correlations.2.2.1 correlations.2.2.2.1 have supported : framework.recordProcess.measuredState (false, false) ≠ 0 := by rw [framework.recordProcess.calibration_derives_measured_coefficients realization.1] simpa [CoherentRecordMeasurement.diagonalState] using realization.2.2 exact ⟨externalSetup.2.2.2, ⟨realization.1, rfl, rfl, Or.inl measurementSetup.2.2.2.2.1⟩, ⟨rfl, realization.2.1, Or.inl ⟨rfl, correlations.2.2.1, supported⟩⟩, ⟨rfl, rfl, Or.inl ⟨rfl, records.1⟩⟩⟩ /-- A realized operational record has a nonempty pointer fiber whose compatible configurations all give the same object value. -/ theorem operational_observer_exposes_a_supported_pointer_record (framework : RelativeStateFramework T) (observer target : T.System) (interaction : T.Interaction) (record : T.Record) (regime : T.Regime) (role : framework.toOperationalObserverContext.OperationalObserverOfAt observer target interaction record regime) : ∃ outcome : Bool, record = (if outcome then framework.secondRecord else framework.firstRecord) ∧ framework.recordProcess.toCorrelationAccessContext.RecordDeterminesValueAt false (Sum.inr outcome) outcome := by have calibration := role.2.1.1 have diagonal := framework.recordProcess.calibration_derives_measured_coefficients calibration rcases role.2.2.1.2.2 with ⟨recordEq, _correlation, support⟩ | ⟨recordEq, _correlation, support⟩ · refine ⟨false, recordEq, ?_⟩ apply framework.recordProcess.pointer_record_determines_the_correlated_value calibration simpa [diagonal, CoherentRecordMeasurement.diagonalState] using support · refine ⟨true, recordEq, ?_⟩ apply framework.recordProcess.pointer_record_determines_the_correlated_value calibration simpa [diagonal, CoherentRecordMeasurement.diagonalState] using support /-- Retaining the paper's role labels and correlation predicates while replacing the coefficient dynamics by zero cannot realize a record. -/ theorem zero_output_measurement_cannot_realize_an_operational_observer (framework : RelativeStateFramework T) (observer target : T.System) (interaction : T.Interaction) (record : T.Record) (regime : T.Regime) : let changed := { framework with recordMeasurementMapAt := fun _ => 0 } ¬changed.toOperationalObserverContext.OperationalObserverOfAt observer target interaction record regime := by dsimp only intro role rcases role.2.2.1.2.2 with ⟨_, _, support⟩ | ⟨_, _, support⟩ · exact support rfl · exact support rfl /-- Calibration alone does not make the zero vector a record-bearing state. This input is not a normalized physical state; it tests nonvacuity. -/ theorem zero_input_preserves_calibration_but_cannot_realize_a_record (framework : RelativeStateFramework T) (calibration : framework.recordProcess.MeasurementCalibration) (observer target : T.System) (interaction : T.Interaction) (record : T.Record) (regime : T.Regime) : let changed := { framework with objectAmplitudesAt := fun _ _ => 0 } changed.recordProcess.MeasurementCalibration ∧ ¬changed.toOperationalObserverContext.OperationalObserverOfAt observer target interaction record regime := by dsimp only refine ⟨calibration, ?_⟩ intro role rcases role.2.2.1.2.2 with ⟨_, _, support⟩ | ⟨_, _, support⟩ · exact support (congrFun (map_zero (framework.recordMeasurementMapAt framework.measurementInteraction)) (false, false)) · exact support (congrFun (map_zero (framework.recordMeasurementMapAt framework.measurementInteraction)) (true, true)) def RepeatedObservationSetup (framework : RelativeStateFramework T) : Prop := framework.secondObservationOfSameQuantity framework.repeatInteraction framework.selectedObservable framework.objectSystem framework.repeatedObservationRegime ∧ framework.stateContainsBranch framework.correlatedMeasurementState framework.firstBranch framework.repeatedObservationRegime ∧ framework.stateContainsBranch framework.correlatedMeasurementState framework.secondBranch framework.repeatedObservationRegime def RepeatedObservationCalculation (framework : RelativeStateFramework T) : Prop := framework.RepeatedObservationSetup → framework.recordSequenceInBranch framework.firstRecord framework.firstRepeatedRecord framework.firstBranch framework.repeatedMeasurementState framework.repeatedObservationRegime ∧ framework.recordSequenceInBranch framework.secondRecord framework.secondRepeatedRecord framework.secondBranch framework.repeatedMeasurementState framework.repeatedObservationRegime ∧ framework.recordsAgreeWithinBranch framework.firstRecord framework.firstRepeatedRecord framework.firstBranch framework.repeatedObservationRegime ∧ framework.recordsAgreeWithinBranch framework.secondRecord framework.secondRepeatedRecord framework.secondBranch framework.repeatedObservationRegime ∧ framework.observerMemoryFormsBranchingTree framework.observerSystem framework.repeatedMeasurementState framework.repeatedObservationRegime ∧ framework.allBranchesSimultaneouslyRetained framework.repeatedMeasurementState framework.repeatedObservationRegime ∧ ¬framework.possibleToActualTransitionOccurs framework.repeatedMeasurementState framework.repeatedObservationRegime theorem repeated_observation_is_repeatable_within_every_retained_branch (framework : RelativeStateFramework T) (setup : framework.RepeatedObservationSetup) (calculation : framework.RepeatedObservationCalculation) : framework.recordsAgreeWithinBranch framework.firstRecord framework.firstRepeatedRecord framework.firstBranch framework.repeatedObservationRegime ∧ framework.recordsAgreeWithinBranch framework.secondRecord framework.secondRepeatedRecord framework.secondBranch framework.repeatedObservationRegime ∧ framework.observerMemoryFormsBranchingTree framework.observerSystem framework.repeatedMeasurementState framework.repeatedObservationRegime ∧ framework.allBranchesSimultaneouslyRetained framework.repeatedMeasurementState framework.repeatedObservationRegime ∧ ¬framework.possibleToActualTransitionOccurs framework.repeatedMeasurementState framework.repeatedObservationRegime := by have result := calculation setup exact ⟨result.2.2.1, result.2.2.2.1, result.2.2.2.2.1, result.2.2.2.2.2.1, result.2.2.2.2.2.2⟩ /-- The 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. -/ def EquationsTwentySevenThroughThirtyOneSquareAmplitudeFormulaAt (framework : RelativeStateFramework T) : Prop := framework.squareAmplitudeFormulaRepresentsAt framework.squareAmplitudeFormulaReadout framework.firstCoefficient framework.secondCoefficient framework.selectedMeasure framework.firstValue framework.secondValue /\ framework.squareAmplitudeFormulaReadout.SourceFormulaAt def MeasureAxioms (framework : RelativeStateFramework T) : Prop := framework.measurePositive framework.selectedMeasure ∧ framework.measurePhaseInsensitive framework.selectedMeasure ∧ framework.measureAdditiveOnOrthogonalComponents framework.selectedMeasure ∧ framework.measureConservedUnderBranching framework.selectedMeasure def MeasureUniquenessCalculation (framework : RelativeStateFramework T) : Prop := framework.MeasureAxioms → framework.measureIsSquareAmplitude framework.selectedMeasure ∧ framework.coefficientHasMeasure framework.firstCoefficient framework.selectedMeasure framework.firstValue ∧ framework.coefficientHasMeasure framework.secondCoefficient framework.selectedMeasure framework.secondValue ∧ framework.EquationsTwentySevenThroughThirtyOneSquareAmplitudeFormulaAt theorem additive_branch_conserved_measure_is_square_amplitude (framework : RelativeStateFramework T) (axioms : framework.MeasureAxioms) (calculation : framework.MeasureUniquenessCalculation) : framework.measureIsSquareAmplitude framework.selectedMeasure ∧ framework.coefficientHasMeasure framework.firstCoefficient framework.selectedMeasure framework.firstValue ∧ framework.coefficientHasMeasure framework.secondCoefficient framework.selectedMeasure framework.secondValue := by rcases calculation axioms with ⟨squareAmplitude, firstMeasure, secondMeasure, _formula⟩ exact ⟨squareAmplitude, firstMeasure, secondMeasure⟩ /-- The source-map square-amplitude result retains the generic measure conclusion beside Everett's literal equations-(27)-(31) readout. -/ def SquareAmplitudeMeasureResult (framework : RelativeStateFramework T) : Prop := (framework.measureIsSquareAmplitude framework.selectedMeasure ∧ framework.coefficientHasMeasure framework.firstCoefficient framework.selectedMeasure framework.firstValue ∧ framework.coefficientHasMeasure framework.secondCoefficient framework.selectedMeasure framework.secondValue) ∧ framework.EquationsTwentySevenThroughThirtyOneSquareAmplitudeFormulaAt theorem additive_branch_conserved_measure_retains_equations_twenty_seven_through_thirty_one (framework : RelativeStateFramework T) (axioms : framework.MeasureAxioms) (calculation : framework.MeasureUniquenessCalculation) : framework.SquareAmplitudeMeasureResult := by rcases calculation axioms with ⟨squareAmplitude, firstMeasure, secondMeasure, formula⟩ exact ⟨⟨squareAmplitude, firstMeasure, secondMeasure⟩, formula⟩ theorem square_amplitude_measure_result_retains_equations_twenty_seven_through_thirty_one (framework : RelativeStateFramework T) (result : framework.SquareAmplitudeMeasureResult) : framework.EquationsTwentySevenThroughThirtyOneSquareAmplitudeFormulaAt := result.2 def StatisticalTypicalitySetup (framework : RelativeStateFramework T) : Prop := framework.measureIsSquareAmplitude framework.selectedMeasure ∧ framework.sequenceMeasureIsProduct framework.firstMemorySequence framework.selectedMeasure ∧ framework.sequenceMeasureIsProduct framework.secondMemorySequence framework.selectedMeasure ∧ (framework.originalFiniteProductMeasureReadout |>.RetainsOriginalProductMeasureFiniteExceptionsAndTypicalityLimit) def MemorySequenceProductMeasures (framework : RelativeStateFramework T) : Prop := framework.sequenceMeasureIsProduct framework.firstMemorySequence framework.selectedMeasure ∧ framework.sequenceMeasureIsProduct framework.secondMemorySequence framework.selectedMeasure ∧ (framework.originalFiniteProductMeasureReadout |>.RetainsOriginalProductMeasureFiniteExceptionsAndTypicalityLimit) theorem square_amplitude_result_and_product_measures_establish_typicality_setup (framework : RelativeStateFramework T) (measureResult : framework.measureIsSquareAmplitude framework.selectedMeasure ∧ framework.coefficientHasMeasure framework.firstCoefficient framework.selectedMeasure framework.firstValue ∧ framework.coefficientHasMeasure framework.secondCoefficient framework.selectedMeasure framework.secondValue) (productMeasures : framework.MemorySequenceProductMeasures) : framework.StatisticalTypicalitySetup := ⟨measureResult.1, productMeasures.1, productMeasures.2.1, productMeasures.2.2⟩ def StatisticalTypicalityCalculation (framework : RelativeStateFramework T) : Prop := framework.StatisticalTypicalitySetup → framework.processOneIndependentWeightsRecovered framework.selectedMeasure framework.asymptoticRegime ∧ framework.exceptionalSetHasMeasureTendingToZero framework.exceptionalSequences framework.selectedMeasure framework.asymptoticRegime ∧ framework.processOneAveragesHoldOutside framework.exceptionalSequences framework.selectedMeasure framework.asymptoticRegime ∧ framework.processOneStatisticsAppearValidToObserver framework.observerSystem framework.selectedMeasure framework.asymptoticRegime /-- The 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. -/ def toTypicalitySelectionContext (framework : RelativeStateFramework T) : TypicalitySelectionContext T.MemorySequence T.Regime T.BranchMeasure where typical := fun measure sequence => measure = framework.selectedMeasure ∧ framework.sequenceOutsideExceptionalSet sequence framework.exceptionalSequences hasProperty := fun sequence regime => framework.processOneAveragesHoldFor sequence framework.selectedMeasure regime propertyTypicalFor := fun measure regime => measure = framework.selectedMeasure ∧ regime = framework.asymptoticRegime ∧ framework.exceptionalSetHasMeasureTendingToZero framework.exceptionalSequences measure regime ∧ framework.processOneAveragesHoldOutside framework.exceptionalSequences measure regime /-- The paper-local bridge from membership outside the exceptional set to the corresponding assertion about an individual memory sequence. -/ def MemorySequenceTypicalityBridge (framework : RelativeStateFramework T) : Prop := ∀ sequence, framework.sequenceOutsideExceptionalSet sequence framework.exceptionalSequences → framework.processOneAveragesHoldFor sequence framework.selectedMeasure framework.asymptoticRegime theorem memory_sequence_bridge_realizes_shared_typical_property_bridge (framework : RelativeStateFramework T) (bridge : framework.MemorySequenceTypicalityBridge) : framework.toTypicalitySelectionContext.TypicalPropertyBridge := by intro measure regime propertyTypical sequence typical rcases propertyTypical with ⟨rfl, rfl, _smallExceptionalSet, _bulkStatement⟩ exact bridge sequence typical.2 theorem product_measure_and_limit_recover_process_one_statistics_almost_everywhere (framework : RelativeStateFramework T) (setup : framework.StatisticalTypicalitySetup) (calculation : framework.StatisticalTypicalityCalculation) : framework.processOneIndependentWeightsRecovered framework.selectedMeasure framework.asymptoticRegime ∧ framework.exceptionalSetHasMeasureTendingToZero framework.exceptionalSequences framework.selectedMeasure framework.asymptoticRegime ∧ framework.processOneAveragesHoldOutside framework.exceptionalSequences framework.selectedMeasure framework.asymptoticRegime ∧ framework.processOneStatisticsAppearValidToObserver framework.observerSystem framework.selectedMeasure framework.asymptoticRegime ∧ (framework.originalFiniteProductMeasureReadout |>.RetainsOriginalProductMeasureFiniteExceptionsAndTypicalityLimit) := by rcases calculation setup with ⟨weights, exceptionalLimit, outsideAverages, observerStatistics⟩ exact ⟨weights, exceptionalLimit, outsideAverages, observerStatistics, setup.2.2.2⟩ /-- Equations (33)-(34) remain product weights rather than equal branch counting, and the finite exceptional set remains nonempty before the limit. -/ theorem statistical_route_retains_original_product_measure_and_finite_exceptions (framework : RelativeStateFramework T) (setup : framework.StatisticalTypicalitySetup) (calculation : framework.StatisticalTypicalityCalculation) : framework.originalFiniteProductMeasureReadout |>.RetainsOriginalProductMeasureFiniteExceptionsAndTypicalityLimit := (framework |>.product_measure_and_limit_recover_process_one_statistics_almost_everywhere setup calculation).2.2.2.2 /-- A chosen product-history weight and the entire exceptional-set measure are distinct limits; the second still needs the imported typicality result. -/ theorem statistical_route_distinguishes_selected_history_from_exceptional_set_limit (framework : RelativeStateFramework T) (setup : framework.StatisticalTypicalitySetup) (calculation : framework.StatisticalTypicalityCalculation) : Filter.Tendsto framework.originalFiniteProductMeasureReadout.exceptionalTailValueAt Filter.atTop (nhds 0) ∧ framework.exceptionalSetHasMeasureTendingToZero framework.exceptionalSequences framework.selectedMeasure framework.asymptoticRegime := by have result := framework |>.product_measure_and_limit_recover_process_one_statistics_almost_everywhere setup calculation rcases result.2.2.2.2.2.2 with ⟨_length, _frequency, _tolerance, _deviation, _exceptionCount, _positiveFinite, _finiteWeight, _positiveLater, _decreasing, _initialTail, _laterTail, zeroLimit, _classification, _productHistory, selectedLimit⟩ exact ⟨zeroLimit ▸ selectedLimit, result.2.1⟩ theorem statistical_limit_realizes_shared_typical_property (framework : RelativeStateFramework T) (setup : framework.StatisticalTypicalitySetup) (calculation : framework.StatisticalTypicalityCalculation) : framework.toTypicalitySelectionContext.propertyTypicalFor framework.selectedMeasure framework.asymptoticRegime := by have result := framework |>.product_measure_and_limit_recover_process_one_statistics_almost_everywhere setup calculation exact ⟨rfl, rfl, result.2.1, result.2.2.1⟩ /-- Everett 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. -/ theorem typical_memory_sequence_inherits_process_one_averages (framework : RelativeStateFramework T) (setup : framework.StatisticalTypicalitySetup) (calculation : framework.StatisticalTypicalityCalculation) (sequence : T.MemorySequence) (typical : framework.toTypicalitySelectionContext.typical framework.selectedMeasure sequence) (bridge : framework.MemorySequenceTypicalityBridge) : framework.processOneAveragesHoldFor sequence framework.selectedMeasure framework.asymptoticRegime := by exact typical_state_has_typical_property_through_bridge framework.toTypicalitySelectionContext framework.selectedMeasure sequence framework.asymptoticRegime (framework.statistical_limit_realizes_shared_typical_property setup calculation) typical (framework.memory_sequence_bridge_realizes_shared_typical_property_bridge bridge) def MultipleObserverSetup (framework : RelativeStateFramework T) : Prop := framework.observerSystem ≠ framework.secondObserverSystem ∧ framework.separatelyObservesSameQuantity framework.observerSystem framework.secondObserverSystem framework.selectedObservable framework.multipleObserverRegime ∧ framework.observersCommunicate framework.communicationInteraction framework.observerSystem framework.secondObserverSystem framework.multipleObserverRegime ∧ framework.interveningObservationNoncommutes framework.noncommutingIntervention framework.selectedObservable framework.noncommutingObservable framework.multipleObserverRegime ∧ framework.systemsCorrelatedButNoninteracting framework.objectSystem framework.remoteSystem framework.multipleObserverRegime /-- The old numerical readout is attached to one supported configuration of the actual comparison. Its record equality is not an input. -/ def OriginalObserverInterventionSourceInputs (framework : RelativeStateFramework T) : Prop := let readout := framework.originalObserverInterventionReadout let configuration := framework.selectedComparisonConfiguration framework.measuredRecordCoefficientsAt framework.correlatedMeasurementState = framework.recordProcess.measuredState ∧ framework.comparedRecordCoefficientsAt framework.multipleObserverState = framework.recordProcess.comparedState ∧ framework.recordProcess.comparedState configuration ≠ 0 ∧ readout.firstCommunicatedRecordValue = configuration.2.1.toNat ∧ readout.secondCommunicatedRecordValue = configuration.2.2.toNat ∧ readout.uninterruptedFirstRecordValue = readout.uninterruptedRepeatedRecordValue ∧ readout.HasOriginalNoncommutingLocalDisturbance ∧ readout.HasOriginalRemoteNoninteractionAndUndisturbedRepeat def MultipleObserverCalculation (framework : RelativeStateFramework T) : Prop := framework.MultipleObserverSetup → framework.recordProcess.ComparisonInputs ∧ ¬framework.repeatCorrelationPreserved framework.observerSystem framework.selectedObservable framework.multipleObserverRegime ∧ ¬framework.remoteObservationChangesLocalRepeatResult framework.remoteMeasurementInteraction framework.remoteSystem framework.objectSystem framework.multipleObserverRegime ∧ framework.OriginalObserverInterventionSourceInputs theorem multiple_observers_agree_with_the_qualified_intervention_rules (framework : RelativeStateFramework T) (setup : framework.MultipleObserverSetup) (calculation : framework.MultipleObserverCalculation) : framework.observerRecordsAgree framework.observerSystem framework.secondObserverSystem framework.selectedObservable framework.multipleObserverRegime ∧ ¬framework.repeatCorrelationPreserved framework.observerSystem framework.selectedObservable framework.multipleObserverRegime ∧ ¬framework.remoteObservationChangesLocalRepeatResult framework.remoteMeasurementInteraction framework.remoteSystem framework.objectSystem framework.multipleObserverRegime ∧ (framework.originalObserverInterventionReadout |>.RetainsOriginalAgreementLocalDisturbanceAndRemoteNoninteraction) := by obtain ⟨inputs, localDisturbance, remoteStability, readoutInputs⟩ := calculation setup obtain ⟨measuredRepresentation, comparedRepresentation, support, firstRecord, secondRecord, repeated, localInput, remoteInput⟩ := readoutInputs have recordIndices := framework.recordProcess.supported_compared_records_match_the_system inputs.1.2 inputs.2 framework.selectedComparisonConfiguration support have agreement := framework.recordProcess.comparison_inputs_derive_nonvacuous_record_result inputs refine ⟨⟨rfl, rfl, rfl, rfl, measuredRepresentation, comparedRepresentation, agreement⟩, localDisturbance, remoteStability, ⟨?_, repeated⟩, localInput, remoteInput⟩ rw [firstRecord, secondRecord, recordIndices.2] theorem observer_comparison_derives_actual_record_access (framework : RelativeStateFramework T) (setup : framework.MultipleObserverSetup) (calculation : framework.MultipleObserverCalculation) : framework.recordProcess.NonvacuousRecordComparisonAt := (framework.multiple_observers_agree_with_the_qualified_intervention_rules setup calculation).1.2.2.2.2.2.2 /-- The observer route distinguishes local noncommuting disturbance from a remote observation of a correlated but noninteracting system. -/ theorem observer_route_retains_original_local_disturbance_and_remote_stability (framework : RelativeStateFramework T) (setup : framework.MultipleObserverSetup) (calculation : framework.MultipleObserverCalculation) : framework.originalObserverInterventionReadout |>.RetainsOriginalAgreementLocalDisturbanceAndRemoteNoninteraction := (framework.multiple_observers_agree_with_the_qualified_intervention_rules setup calculation).2.2.2 def UniversalRelativeStateRealization (framework : RelativeStateFramework T) : Prop := framework.toLinearRelativeStateContext.completeness.CompleteAt framework.universalDescription framework.closedRegime ∧ framework.linearEvolution framework.processTwoDynamics framework.closedRegime ∧ framework.stateFunctionEvolvesContinuouslyAt framework.universalDescription framework.processTwoDynamics framework.compositeSystem framework.closedRegime ∧ framework.toLinearRelativeStateContext.UniversalDynamicsAt framework.processTwoDynamics framework.closedRegime ∧ ¬framework.fundamentalCollapse framework.processTwoDynamics framework.closedRegime ∧ framework.toLinearRelativeStateContext.AllBranchesRetainedAt framework.universalDescription framework.closedRegime ∧ framework.toLinearRelativeStateContext.BranchRelativeDefinitenessAt framework.universalDescription framework.closedRegime ∧ framework.physicalSystem framework.observerSystem ∧ framework.branchComponent framework.firstBranch framework.universalDescription framework.closedRegime theorem paper_commitments_realize_universal_linear_relative_state (framework : RelativeStateFramework T) (realization : framework.UniversalRelativeStateRealization) : framework.toLinearRelativeStateContext.UniversalLinearRelativeStateAt framework.universalDescription framework.processTwoDynamics framework.closedRegime := by rcases realization with ⟨complete, linear, _continuous, universal, noCollapse, retained, definite, physicalObserver, branchComponent⟩ exact ⟨⟨complete, linear, universal, noCollapse, retained, definite⟩, ⟨⟨framework.observerSystem, physicalObserver⟩, ⟨framework.firstBranch, branchComponent⟩⟩⟩ def QualifiedConclusionSetup (framework : RelativeStateFramework T) : Prop := framework.UniversalRelativeStateRealization ∧ framework.processOneStatisticsAppearValidToObserver framework.observerSystem framework.selectedMeasure framework.asymptoticRegime ∧ framework.observerRecordsAgree framework.observerSystem framework.secondObserverSystem framework.selectedObservable framework.multipleObserverRegime def QualifiedUniversalRealizationBridge (framework : RelativeStateFramework T) : Prop := framework.stateFunctionEvolvesContinuouslyAt framework.universalDescription framework.processTwoDynamics framework.compositeSystem framework.closedRegime ∧ framework.toLinearRelativeStateContext.AllBranchesRetainedAt framework.universalDescription framework.closedRegime ∧ framework.toLinearRelativeStateContext.BranchRelativeDefinitenessAt framework.universalDescription framework.closedRegime ∧ framework.physicalSystem framework.observerSystem ∧ framework.branchComponent framework.firstBranch framework.universalDescription framework.closedRegime theorem prior_outputs_and_universal_bridge_establish_qualified_conclusion_setup (framework : RelativeStateFramework T) (pureResult : framework.completeMathematicalModelFor framework.universalDescription framework.universeSystem framework.closedRegime ∧ framework.toLinearRelativeStateContext.completeness.CompleteAt framework.universalDescription framework.closedRegime ∧ framework.linearEvolution framework.processTwoDynamics framework.closedRegime ∧ framework.toLinearRelativeStateContext.UniversalDynamicsAt framework.processTwoDynamics framework.closedRegime ∧ ¬framework.fundamentalCollapse framework.processTwoDynamics framework.closedRegime) (typicalityResult : framework.processOneIndependentWeightsRecovered framework.selectedMeasure framework.asymptoticRegime ∧ framework.exceptionalSetHasMeasureTendingToZero framework.exceptionalSequences framework.selectedMeasure framework.asymptoticRegime ∧ framework.processOneAveragesHoldOutside framework.exceptionalSequences framework.selectedMeasure framework.asymptoticRegime ∧ framework.processOneStatisticsAppearValidToObserver framework.observerSystem framework.selectedMeasure framework.asymptoticRegime ∧ (framework.originalFiniteProductMeasureReadout |>.RetainsOriginalProductMeasureFiniteExceptionsAndTypicalityLimit)) (observersResult : framework.observerRecordsAgree framework.observerSystem framework.secondObserverSystem framework.selectedObservable framework.multipleObserverRegime ∧ ¬framework.repeatCorrelationPreserved framework.observerSystem framework.selectedObservable framework.multipleObserverRegime ∧ ¬framework.remoteObservationChangesLocalRepeatResult framework.remoteMeasurementInteraction framework.remoteSystem framework.objectSystem framework.multipleObserverRegime ∧ (framework.originalObserverInterventionReadout |>.RetainsOriginalAgreementLocalDisturbanceAndRemoteNoninteraction)) (bridge : framework.QualifiedUniversalRealizationBridge) : framework.QualifiedConclusionSetup := by have realization : framework.UniversalRelativeStateRealization := ⟨pureResult.2.1, pureResult.2.2.1, bridge.1, pureResult.2.2.2.1, pureResult.2.2.2.2, bridge.2.1, bridge.2.2.1, bridge.2.2.2.1, bridge.2.2.2.2⟩ exact ⟨realization, typicalityResult.2.2.2.1, observersResult.1⟩ def QualifiedConclusionResult (framework : RelativeStateFramework T) : Prop := framework.toLinearRelativeStateContext.UniversalLinearRelativeStateAt framework.universalDescription framework.processTwoDynamics framework.closedRegime ∧ framework.stateFunctionEvolvesContinuouslyAt framework.universalDescription framework.processTwoDynamics framework.compositeSystem framework.closedRegime ∧ framework.processOneStatisticsAppearValidToObserver framework.observerSystem framework.selectedMeasure framework.asymptoticRegime ∧ framework.observerRecordsAgree framework.observerSystem framework.secondObserverSystem framework.selectedObservable framework.multipleObserverRegime def QualifiedConclusionCalculation (framework : RelativeStateFramework T) : Prop := framework.QualifiedConclusionSetup → framework.toLinearRelativeStateContext.UniversalLinearRelativeStateAt framework.universalDescription framework.processTwoDynamics framework.closedRegime ∧ framework.processOneStatisticsAppearValidToObserver framework.observerSystem framework.selectedMeasure framework.asymptoticRegime ∧ framework.observerRecordsAgree framework.observerSystem framework.secondObserverSystem framework.selectedObservable framework.multipleObserverRegime theorem relative_state_formulation_has_the_paper_s_qualified_scope (framework : RelativeStateFramework T) (setup : framework.QualifiedConclusionSetup) (calculation : framework.QualifiedConclusionCalculation) : framework.QualifiedConclusionResult := by have assessed := calculation setup have continuousEvolution := setup.1.2.2.1 exact ⟨assessed.1, continuousEvolution, assessed.2.1, assessed.2.2⟩ theorem qualified_conclusion_retains_continuous_state_evolution (framework : RelativeStateFramework T) (result : framework.QualifiedConclusionResult) : framework.stateFunctionEvolvesContinuouslyAt framework.universalDescription framework.processTwoDynamics framework.compositeSystem framework.closedRegime := result.2.1 theorem everett_route_recovers_orthodox_statistics_without_process_one_dynamics (framework : RelativeStateFramework T) (pureSetup : framework.PureWaveTheorySetup) (pureCalculation : framework.PureWaveCompletionCalculation) (measurementSetup : framework.GoodMeasurementSetup) (measurementCalculation : framework.LinearMeasurementCalculation) (relativeInterpretation : framework.RelativeRecordInterpretation) (measureAxioms : framework.MeasureAxioms) (measureCalculation : framework.MeasureUniquenessCalculation) (typicalityCalculation : framework.StatisticalTypicalityCalculation) (productMeasures : framework.MemorySequenceProductMeasures) : ¬framework.fundamentalCollapse framework.processTwoDynamics framework.closedRegime ∧ ¬framework.globallySelectsSingleOutcome framework.correlatedMeasurementState framework.measurementRegime ∧ framework.measureIsSquareAmplitude framework.selectedMeasure ∧ framework.processOneStatisticsAppearValidToObserver framework.observerSystem framework.selectedMeasure framework.asymptoticRegime := by have pureResult := pureCalculation pureSetup have measurementResult := framework.linear_measurement_produces_correlated_relative_records_without_selection measurementSetup measurementCalculation relativeInterpretation have measureResult := measureCalculation measureAxioms have typicalitySetup : framework.StatisticalTypicalitySetup := ⟨measureResult.1, productMeasures.1, productMeasures.2.1, productMeasures.2.2⟩ have typicalityResult := typicalityCalculation typicalitySetup exact ⟨pureResult.2.2.2.2, measurementResult.2.2.2.2.1, measureResult.1, typicalityResult.2.2.2⟩ def toLinearRelativeStateMeasurementContext (framework : RelativeStateFramework T) : LinearRelativeStateMeasurementContext T.State T.State T.State T.Record T.Branch T.Interaction T.Regime where selectedInputState := framework.initialObjectState selectedFinalState := framework.correlatedMeasurementState selectedFirstSystemState := framework.firstEigenstate selectedSecondSystemState := framework.secondEigenstate selectedInitialObserverState := framework.initialObserverState selectedFirstObserverState := framework.firstObserverState selectedSecondObserverState := framework.secondObserverState selectedFirstRecord := framework.firstRecord selectedSecondRecord := framework.secondRecord selectedFirstBranch := framework.firstBranch selectedSecondBranch := framework.secondBranch selectedInteraction := framework.measurementInteraction selectedRegime := framework.measurementRegime calibratedOn := framework.calibratedOn inputSuperposes := framework.inputSuperposes linearEvolutionApplies := fun interaction regime => framework.linearEvolutionApplies framework.processTwoDynamics interaction regime containsBranch := framework.stateContainsBranch branchCorrelates := framework.branchCorrelates recordDefiniteRelativeTo := framework.recordDefiniteRelativeTo globallySelectsSingleOutcome := framework.globallySelectsSingleOutcome def relativeMeasurementModel (framework : RelativeStateFramework T) : LinearRelativeStateMeasurementModel T.State T.State T.State T.Record T.Branch T.Interaction T.Regime := framework.toLinearRelativeStateMeasurementContext.selectedModel theorem linear_relative_state_measurement_model_retains_paper_semantics (framework : RelativeStateFramework T) : framework.toLinearRelativeStateMeasurementContext |>.SelectedLinearRelativeStateMeasurementSemanticsAt framework.relativeMeasurementModel := rfl theorem good_measurement_realizes_shared_calibrated_setup (framework : RelativeStateFramework T) (setup : framework.GoodMeasurementSetup) : framework.toLinearRelativeStateMeasurementContext |>.CalibratedSuperpositionSetupAt framework.relativeMeasurementModel := by rcases setup with ⟨systemsDistinct, observersDistinct, recordsDistinct, branchesDistinct, firstCalibration, secondCalibration, superposition, linearity⟩ exact ⟨framework.linear_relative_state_measurement_model_retains_paper_semantics, ⟨systemsDistinct, observersDistinct, recordsDistinct, branchesDistinct⟩, firstCalibration, secondCalibration, superposition, linearity⟩ theorem linear_calculation_realizes_shared_branch_correlation (framework : RelativeStateFramework T) (calculation : framework.LinearMeasurementCalculation) : framework.toLinearRelativeStateMeasurementContext |>.LinearCorrelationCalculationAt framework.relativeMeasurementModel := by intro sharedSetup rcases sharedSetup with ⟨_selected, ⟨systemsDistinct, observersDistinct, recordsDistinct, branchesDistinct⟩, firstCalibration, secondCalibration, superposition, linearity⟩ have source := calculation ⟨systemsDistinct, observersDistinct, recordsDistinct, branchesDistinct, firstCalibration, secondCalibration, superposition, linearity⟩ exact ⟨source.1, source.2.1, source.2.2.1, source.2.2.2.1⟩ theorem relative_records_realize_shared_interpretation (framework : RelativeStateFramework T) (interpretation : framework.RelativeRecordInterpretation) : framework.toLinearRelativeStateMeasurementContext |>.RelativeRecordInterpretationAt framework.relativeMeasurementModel := by intro sharedSetup firstCorrelation secondCorrelation rcases sharedSetup with ⟨_selected, ⟨systemsDistinct, observersDistinct, recordsDistinct, branchesDistinct⟩, firstCalibration, secondCalibration, superposition, linearity⟩ exact interpretation ⟨systemsDistinct, observersDistinct, recordsDistinct, branchesDistinct, firstCalibration, secondCalibration, superposition, linearity⟩ firstCorrelation secondCorrelation /-- Everett's Process-2 route from calibrated observation to memory records. -/ inductive EverettLinearRelativeStateMeasurementDerivation where | processTwoSuperpositionAndRelativeMemoryRecords deriving DecidableEq, Repr /-- Raw 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. -/ def everettLinearRelativeStateMeasurementDerivationObtains (framework : RelativeStateFramework T) : EverettLinearRelativeStateMeasurementDerivation → Prop | .processTwoSuperpositionAndRelativeMemoryRecords => framework.GoodMeasurementSetup ∧ framework.LinearMeasurementCalculation ∧ framework.RelativeRecordInterpretation theorem everett_source_inputs_make_shared_relative_measurement_route_applicable (framework : RelativeStateFramework T) (source : framework.everettLinearRelativeStateMeasurementDerivationObtains .processTwoSuperpositionAndRelativeMemoryRecords) : framework.toLinearRelativeStateMeasurementContext |>.LinearRelativeStateMeasurementRouteApplicableAt framework.relativeMeasurementModel := by rcases source with ⟨setup, calculation, interpretation⟩ apply framework.toLinearRelativeStateMeasurementContext |>.setup_calculation_and_interpretation_make_relative_measurement_applicable · exact framework.good_measurement_realizes_shared_calibrated_setup setup · exact framework.linear_calculation_realizes_shared_branch_correlation calculation · exact framework.relative_records_realize_shared_interpretation interpretation theorem everett_source_inputs_realize_structural_linear_relative_state_measurement_explanation (framework : RelativeStateFramework T) (source : framework.everettLinearRelativeStateMeasurementDerivationObtains .processTwoSuperpositionAndRelativeMemoryRecords) : framework.toLinearRelativeStateMeasurementContext |>.DirectStructuralLinearRelativeStateMeasurementExplanationAt framework.relativeMeasurementModel := framework.toLinearRelativeStateMeasurementContext |>.applicable_route_realizes_structural_linear_relative_state_measurement_explanation (framework |>.everett_source_inputs_make_shared_relative_measurement_route_applicable source) theorem everett_source_inputs_realize_source_structural_linear_relative_state_measurement_explanation (framework : RelativeStateFramework T) (source : framework.everettLinearRelativeStateMeasurementDerivationObtains .processTwoSuperpositionAndRelativeMemoryRecords) : framework.toLinearRelativeStateMeasurementContext |>.DirectSourceStructuralLinearRelativeStateMeasurementExplanationAt framework.relativeMeasurementModel .processTwoSuperpositionAndRelativeMemoryRecords framework.everettLinearRelativeStateMeasurementDerivationObtains := framework.toLinearRelativeStateMeasurementContext |>.source_derivation_and_applicable_route_realize_source_structural_linear_relative_state_measurement_explanation .processTwoSuperpositionAndRelativeMemoryRecords framework.everettLinearRelativeStateMeasurementDerivationObtains source (framework |>.everett_source_inputs_make_shared_relative_measurement_route_applicable source) /-- Everett 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. -/ theorem everett_inputs_make_shared_relative_measurement_route_applicable (framework : RelativeStateFramework T) (setup : framework.GoodMeasurementSetup) (calculation : framework.LinearMeasurementCalculation) (interpretation : framework.RelativeRecordInterpretation) : framework.toLinearRelativeStateMeasurementContext |>.LinearRelativeStateMeasurementRouteApplicableAt framework.relativeMeasurementModel := by apply framework.toLinearRelativeStateMeasurementContext |>.setup_calculation_and_interpretation_make_relative_measurement_applicable · exact framework.good_measurement_realizes_shared_calibrated_setup setup · exact framework.linear_calculation_realizes_shared_branch_correlation calculation · exact framework.relative_records_realize_shared_interpretation interpretation theorem everett_measurement_realizes_shared_relative_state_measurement (framework : RelativeStateFramework T) (setup : framework.GoodMeasurementSetup) (calculation : framework.LinearMeasurementCalculation) (interpretation : framework.RelativeRecordInterpretation) : framework.toLinearRelativeStateMeasurementContext |>.EstablishedLinearRelativeStateMeasurementAt framework.relativeMeasurementModel := framework.toLinearRelativeStateMeasurementContext |>.applicable_route_establishes_linear_relative_state_measurement (framework.everett_inputs_make_shared_relative_measurement_route_applicable setup calculation interpretation) /-- Everett 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. -/ theorem everett_measurement_exhibits_nonvacuous_shared_two_branch_route (framework : RelativeStateFramework T) (setup : framework.GoodMeasurementSetup) (calculation : framework.LinearMeasurementCalculation) (interpretation : framework.RelativeRecordInterpretation) : framework.relativeMeasurementModel |>.NonvacuousLinearRelativeStateMeasurementAt := framework.toLinearRelativeStateMeasurementContext |>.established_measurement_exhibits_nonvacuous_two_branch_route (framework.everett_measurement_realizes_shared_relative_state_measurement setup calculation interpretation) /-- Everett's physical-system and memory semantics connect the first realized shared branch to the neutral operational-observer conditions. -/ theorem first_shared_relative_record_realizes_operational_observer_bridge (framework : RelativeStateFramework T) (externalSetup : framework.ExternalObservationProblemSetup) (realization : framework.FirstCoherentRecordRealizationInputs) : framework.relativeMeasurementModel.OperationalObserverBridgeAt framework.toOperationalObserverContext framework.observerSystem framework.objectSystem framework.firstEigenstate framework.firstObserverState framework.firstRecord framework.firstBranch := by refine ⟨externalSetup.2.2.2, ?_, ?_, ?_⟩ · intro calibration exact ⟨realization.1, rfl, rfl, Or.inl calibration⟩ · intro correlation refine ⟨rfl, realization.2.1, Or.inl ⟨rfl, correlation, ?_⟩⟩ rw [framework.recordProcess.calibration_derives_measured_coefficients realization.1] simpa [CoherentRecordMeasurement.diagonalState] using realization.2.2 · intro definite exact ⟨rfl, rfl, Or.inl ⟨rfl, definite⟩⟩ /-- The established shared relative-state route realizes Everett's operational observer role only through the paper-local physical-memory bridge. -/ theorem shared_relative_measurement_realizes_operational_observer_role (framework : RelativeStateFramework T) (externalSetup : framework.ExternalObservationProblemSetup) (setup : framework.GoodMeasurementSetup) (calculation : framework.LinearMeasurementCalculation) (interpretation : framework.RelativeRecordInterpretation) (realization : framework.FirstCoherentRecordRealizationInputs) : framework.toOperationalObserverContext.OperationalObserverOfAt framework.observerSystem framework.objectSystem framework.measurementInteraction framework.firstRecord framework.measurementRegime := framework.toLinearRelativeStateMeasurementContext |>.established_measurement_and_first_observer_bridge_realize_operational_observer framework.toOperationalObserverContext (framework.everett_measurement_realizes_shared_relative_state_measurement setup calculation interpretation) (framework.first_shared_relative_record_realizes_operational_observer_bridge externalSetup realization) def toLinearRelativeStateMeasurementInterpretation (framework : RelativeStateFramework T) : LinearRelativeStateMeasurementInterpretation EverettRelativeMeasurementTheory EverettRelativeMeasurementWorld T.State T.State T.State T.Record T.Branch T.Interaction T.Regime where theoryUsesMeasurementModel := fun theory model => theory = .universalProcessTwoMeasurement ∧ model = framework.relativeMeasurementModel ∧ (framework.toLinearRelativeStateMeasurementContext |>.SelectedLinearRelativeStateMeasurementSemanticsAt model) measurementModelRepresentsWorld := fun model world => world = .selectedObserverMeasurement ∧ model = framework.relativeMeasurementModel ∧ (framework.toLinearRelativeStateMeasurementContext |>.SelectedLinearRelativeStateMeasurementSemanticsAt model) theoryClaim := fun _ model claim => framework.toLinearRelativeStateMeasurementContext |>.LinearRelativeStateMeasurementClaimHoldsAt model claim physicalClaim := fun _ model claim => framework.toLinearRelativeStateMeasurementContext |>.LinearRelativeStateMeasurementClaimHoldsAt model claim theorem everett_measurement_model_inputs_establish_theory_model_grounding (framework : RelativeStateFramework T) (setup : framework.GoodMeasurementSetup) : framework.toLinearRelativeStateMeasurementContext.TheoryModelGroundingAt framework.toLinearRelativeStateMeasurementInterpretation .universalProcessTwoMeasurement .selectedObserverMeasurement framework.relativeMeasurementModel := by apply framework.toLinearRelativeStateMeasurementContext |>.theory_model_inputs_establish_grounding framework.toLinearRelativeStateMeasurementInterpretation · exact framework.good_measurement_realizes_shared_calibrated_setup setup · exact ⟨rfl, rfl, framework.linear_relative_state_measurement_model_retains_paper_semantics⟩ · exact ⟨rfl, rfl, framework.linear_relative_state_measurement_model_retains_paper_semantics⟩ · intro _claim modelClaim exact modelClaim · intro _claim modelClaim exact modelClaim theorem everett_measurement_establishes_grounded_shared_relative_measurement (framework : RelativeStateFramework T) (setup : framework.GoodMeasurementSetup) (calculation : framework.LinearMeasurementCalculation) (interpretation : framework.RelativeRecordInterpretation) : framework.toLinearRelativeStateMeasurementContext |>.TheoryModelGroundedLinearRelativeStateMeasurementAt framework.toLinearRelativeStateMeasurementInterpretation .universalProcessTwoMeasurement .selectedObserverMeasurement framework.relativeMeasurementModel := framework.toLinearRelativeStateMeasurementContext |>.established_measurement_and_grounding_establish_grounded_measurement (framework.everett_measurement_realizes_shared_relative_state_measurement setup calculation interpretation) (framework |>.everett_measurement_model_inputs_establish_theory_model_grounding setup) theorem grounded_everett_measurement_transfers_every_shared_claim (framework : RelativeStateFramework T) (grounded : framework.toLinearRelativeStateMeasurementContext |>.TheoryModelGroundedLinearRelativeStateMeasurementAt framework.toLinearRelativeStateMeasurementInterpretation .universalProcessTwoMeasurement .selectedObserverMeasurement framework.relativeMeasurementModel) : ∀ claim, (framework.toLinearRelativeStateMeasurementContext |>.toTheoryModelContext framework.toLinearRelativeStateMeasurementInterpretation |>.theoryEntails (PhysicsLogic.Framework.LinearRelativeStateMeasurementContext.measurementTheoryAt EverettRelativeMeasurementTheory.universalProcessTwoMeasurement framework.relativeMeasurementModel) claim ()) ∧ (framework.toLinearRelativeStateMeasurementContext |>.toTheoryModelContext framework.toLinearRelativeStateMeasurementInterpretation |>.trueIn (PhysicsLogic.Framework.LinearRelativeStateMeasurementContext.measurementWorldAt EverettRelativeMeasurementWorld.selectedObserverMeasurement framework.relativeMeasurementModel) claim ()) := framework.toLinearRelativeStateMeasurementContext |>.grounded_measurement_transfers_all_claims_to_theory_and_world grounded namespace Countermodels structure ReducedClosedSystemReadout where observerSystemCount : Nat isolatedObserverSystemCount : Nat availableExternalObserverCount : Nat externalObservationRunCount : Nat processOneCoveredSystemCount : Nat waveRepresentedSystemCount : Nat linearlyEvolvedStateCount : Nat completeInternalModelCount : Nat def ReducedClosedSystemReadout.HasExternalObservationProblem (readout : ReducedClosedSystemReadout) : Prop := 0 < readout.observerSystemCount ∧ 0 < readout.isolatedObserverSystemCount def ReducedClosedSystemReadout.HasExternalObservationLimitation (readout : ReducedClosedSystemReadout) : Prop := readout.availableExternalObserverCount = 0 ∧ readout.externalObservationRunCount = 0 ∧ readout.processOneCoveredSystemCount = 0 def ReducedClosedSystemReadout.HasPureWaveCompletion (readout : ReducedClosedSystemReadout) : Prop := 0 < readout.waveRepresentedSystemCount ∧ 0 < readout.linearlyEvolvedStateCount ∧ 0 < readout.completeInternalModelCount def closedObserverSystemWithoutPureWaveCompletion : ReducedClosedSystemReadout where observerSystemCount := 1 isolatedObserverSystemCount := 1 availableExternalObserverCount := 0 externalObservationRunCount := 0 processOneCoveredSystemCount := 0 waveRepresentedSystemCount := 0 linearlyEvolvedStateCount := 0 completeInternalModelCount := 0 theorem closed_system_limitation_does_not_supply_pure_wave_completion : closedObserverSystemWithoutPureWaveCompletion.HasExternalObservationProblem ∧ closedObserverSystemWithoutPureWaveCompletion.HasExternalObservationLimitation ∧ ¬closedObserverSystemWithoutPureWaveCompletion.HasPureWaveCompletion := by norm_num [ReducedClosedSystemReadout.HasExternalObservationProblem, ReducedClosedSystemReadout.HasExternalObservationLimitation, ReducedClosedSystemReadout.HasPureWaveCompletion, closedObserverSystemWithoutPureWaveCompletion] def calibratedBranchesWithoutSelection := LinearRelativeStateMeasurementContext.Countermodels.selectedMeasurementSemanticsModel theorem two_correlated_branches_do_not_select_one_global_outcome : calibratedBranchesWithoutSelection.calibratedOn false false false false false false false ∧ calibratedBranchesWithoutSelection.calibratedOn false true false true true true false ∧ calibratedBranchesWithoutSelection.containsBranch false false false ∧ calibratedBranchesWithoutSelection.containsBranch false true false ∧ calibratedBranchesWithoutSelection.branchCorrelates false false false false false false ∧ calibratedBranchesWithoutSelection.branchCorrelates false true true true true false ∧ ¬calibratedBranchesWithoutSelection.globallySelectsSingleOutcome false false := by simp [calibratedBranchesWithoutSelection, LinearRelativeStateMeasurementContext.Countermodels.selectedMeasurementSemanticsModel, LinearRelativeStateMeasurementContext.Countermodels.selectedMeasurementSemanticsContext, LinearRelativeStateMeasurementContext.selectedModel, LinearRelativeStateMeasurementContext.calculationModelAt] structure ReducedBranchMeasureReadout where normalizationConstantValue : Real firstAmplitudeSquaredValue : Real secondAmplitudeSquaredValue : Real firstBranchMeasureValue : Real secondBranchMeasureValue : Real totalBranchMeasureValue : Real def ReducedBranchMeasureReadout.HasPositiveNormalizedMeasure (readout : ReducedBranchMeasureReadout) : Prop := 0 < readout.normalizationConstantValue ∧ 0 < readout.firstBranchMeasureValue ∧ 0 < readout.secondBranchMeasureValue ∧ readout.totalBranchMeasureValue = readout.firstBranchMeasureValue + readout.secondBranchMeasureValue ∧ readout.totalBranchMeasureValue = 1 def ReducedBranchMeasureReadout.HasSquareAmplitudeMeasure (readout : ReducedBranchMeasureReadout) : Prop := readout.firstBranchMeasureValue = readout.normalizationConstantValue * readout.firstAmplitudeSquaredValue ∧ readout.secondBranchMeasureValue = readout.normalizationConstantValue * readout.secondAmplitudeSquaredValue noncomputable def positiveNormalizedMeasureWithoutSquareAmplitude : ReducedBranchMeasureReadout where normalizationConstantValue := 1 firstAmplitudeSquaredValue := 1 / 4 secondAmplitudeSquaredValue := 3 / 4 firstBranchMeasureValue := 1 / 2 secondBranchMeasureValue := 1 / 2 totalBranchMeasureValue := 1 theorem positivity_alone_does_not_identify_square_amplitude : positiveNormalizedMeasureWithoutSquareAmplitude.HasPositiveNormalizedMeasure ∧ ¬positiveNormalizedMeasureWithoutSquareAmplitude.HasSquareAmplitudeMeasure := by norm_num [ReducedBranchMeasureReadout.HasPositiveNormalizedMeasure, ReducedBranchMeasureReadout.HasSquareAmplitudeMeasure, positiveNormalizedMeasureWithoutSquareAmplitude] structure ReducedFiniteSequenceReadout where firstOutcomeWeight : Real secondOutcomeWeight : Real selectedSequenceLength : Nat selectedFirstOutcomeCount : Nat selectedSecondOutcomeCount : Nat selectedSequenceMeasure : Real exceptionalMeasureAt : Nat → Real def ReducedFiniteSequenceReadout.HasFiniteProductMeasure (readout : ReducedFiniteSequenceReadout) : Prop := 0 < readout.firstOutcomeWeight ∧ 0 < readout.secondOutcomeWeight ∧ readout.firstOutcomeWeight + readout.secondOutcomeWeight = 1 ∧ 0 < readout.selectedSequenceLength ∧ readout.selectedFirstOutcomeCount + readout.selectedSecondOutcomeCount = readout.selectedSequenceLength ∧ readout.selectedSequenceMeasure = readout.firstOutcomeWeight ^ readout.selectedFirstOutcomeCount * readout.secondOutcomeWeight ^ readout.selectedSecondOutcomeCount def ReducedFiniteSequenceReadout.HasVanishingExceptionalMeasure (readout : ReducedFiniteSequenceReadout) : Prop := ∀ tolerance : Real, 0 < tolerance → ∃ cutoff : Nat, ∀ length : Nat, cutoff ≤ length → readout.exceptionalMeasureAt length < tolerance noncomputable def finiteProductSequenceWithoutAsymptoticLimit : ReducedFiniteSequenceReadout where firstOutcomeWeight := 1 / 2 secondOutcomeWeight := 1 / 2 selectedSequenceLength := 2 selectedFirstOutcomeCount := 1 selectedSecondOutcomeCount := 1 selectedSequenceMeasure := 1 / 4 exceptionalMeasureAt := fun _ => 1 / 2 theorem finite_sequence_data_does_not_supply_the_asymptotic_limit : finiteProductSequenceWithoutAsymptoticLimit.HasFiniteProductMeasure ∧ ¬finiteProductSequenceWithoutAsymptoticLimit.HasVanishingExceptionalMeasure := by constructor · norm_num [ReducedFiniteSequenceReadout.HasFiniteProductMeasure, finiteProductSequenceWithoutAsymptoticLimit] intro vanishing rcases vanishing (1 / 4) (by norm_num) with ⟨cutoff, bound⟩ have contradiction := bound cutoff (Nat.le_refl cutoff) norm_num [finiteProductSequenceWithoutAsymptoticLimit] at contradiction /-- Even the exact Born-product weight of a selected exceptional history can decay while the independently supplied measure of the whole set does not. -/ noncomputable def geometricHistoryWithNonvanishingExceptionalSet : ReducedFiniteSequenceReadout where firstOutcomeWeight := 9 / 25 secondOutcomeWeight := 16 / 25 selectedSequenceLength := 2 selectedFirstOutcomeCount := 2 selectedSecondOutcomeCount := 0 selectedSequenceMeasure := 81 / 625 exceptionalMeasureAt := fun _ => 1 / 2 theorem a_vanishing_selected_product_history_does_not_make_the_whole_exceptional_set_vanish : (geometricHistoryWithNonvanishingExceptionalSet.HasFiniteProductMeasure ∧ Filter.Tendsto (fun length : Nat => geometricHistoryWithNonvanishingExceptionalSet.firstOutcomeWeight ^ (length + geometricHistoryWithNonvanishingExceptionalSet.selectedSequenceLength)) Filter.atTop (nhds 0)) ∧ ¬geometricHistoryWithNonvanishingExceptionalSet.HasVanishingExceptionalMeasure := by constructor · constructor · norm_num [ReducedFiniteSequenceReadout.HasFiniteProductMeasure, geometricHistoryWithNonvanishingExceptionalSet] rfl · have geometricLimit := tendsto_pow_atTop_nhds_zero_of_lt_one (show (0 : Real) ≤ 9 / 25 by norm_num) (show (9 / 25 : Real) < 1 by norm_num) have shiftedLimit := geometricLimit.mul (tendsto_const_nhds (x := (9 / 25 : Real) ^ 2)) simpa [geometricHistoryWithNonvanishingExceptionalSet, pow_add] using shiftedLimit · intro vanishing rcases vanishing (1 / 4) (by norm_num) with ⟨cutoff, bound⟩ have contradiction := bound cutoff (Nat.le_refl cutoff) norm_num [geometricHistoryWithNonvanishingExceptionalSet] at contradiction structure ReducedTypicalSequenceReadout where selectedSequenceLength : Nat selectedFirstOutcomeCount : Nat selectedSecondOutcomeCount : Nat expectedFirstOutcomeWeight : Real observedFirstOutcomeFrequency : Real frequencyTolerance : Real exceptionalSetMeasure : Real selectedExceptionalMembership : Nat def ReducedTypicalSequenceReadout.HasAggregateTypicality (readout : ReducedTypicalSequenceReadout) : Prop := 0 < readout.selectedSequenceLength ∧ readout.selectedFirstOutcomeCount + readout.selectedSecondOutcomeCount = readout.selectedSequenceLength ∧ readout.observedFirstOutcomeFrequency = (readout.selectedFirstOutcomeCount : Real) / readout.selectedSequenceLength ∧ 0 < readout.expectedFirstOutcomeWeight ∧ readout.expectedFirstOutcomeWeight < 1 ∧ 0 < readout.frequencyTolerance ∧ 0 ≤ readout.exceptionalSetMeasure ∧ readout.exceptionalSetMeasure < readout.frequencyTolerance def ReducedTypicalSequenceReadout.SelectedSequenceOutsideExceptionalSet (readout : ReducedTypicalSequenceReadout) : Prop := readout.selectedExceptionalMembership = 0 def ReducedTypicalSequenceReadout.HasIndividualFrequencyBridge (readout : ReducedTypicalSequenceReadout) : Prop := readout.SelectedSequenceOutsideExceptionalSet → |readout.observedFirstOutcomeFrequency - readout.expectedFirstOutcomeWeight| ≤ readout.frequencyTolerance noncomputable def bulkTypicalityWithoutIndividualFrequencyBridge : ReducedTypicalSequenceReadout where selectedSequenceLength := 4 selectedFirstOutcomeCount := 0 selectedSecondOutcomeCount := 4 expectedFirstOutcomeWeight := 1 / 2 observedFirstOutcomeFrequency := 0 frequencyTolerance := 1 / 4 exceptionalSetMeasure := 0 selectedExceptionalMembership := 0 theorem bulk_typicality_does_not_supply_the_individual_sequence_bridge : bulkTypicalityWithoutIndividualFrequencyBridge.HasAggregateTypicality ∧ bulkTypicalityWithoutIndividualFrequencyBridge.SelectedSequenceOutsideExceptionalSet ∧ ¬bulkTypicalityWithoutIndividualFrequencyBridge.HasIndividualFrequencyBridge := by norm_num [ReducedTypicalSequenceReadout.HasAggregateTypicality, ReducedTypicalSequenceReadout.SelectedSequenceOutsideExceptionalSet, ReducedTypicalSequenceReadout.HasIndividualFrequencyBridge, bulkTypicalityWithoutIndividualFrequencyBridge] structure ReducedDynamicsReadout where admittedCompositeStateCount : Nat linearlyEvolvedStateCount : Nat sampledEvolutionTimeCount : Nat continuousStateHistoryCount : Nat def ReducedDynamicsReadout.HasUniversalLinearEvolution (readout : ReducedDynamicsReadout) : Prop := 0 < readout.admittedCompositeStateCount ∧ readout.linearlyEvolvedStateCount = readout.admittedCompositeStateCount def ReducedDynamicsReadout.HasContinuousStateEvolution (readout : ReducedDynamicsReadout) : Prop := 1 < readout.sampledEvolutionTimeCount ∧ readout.continuousStateHistoryCount = readout.linearlyEvolvedStateCount def universalLinearEvolutionWithoutContinuousHistory : ReducedDynamicsReadout where admittedCompositeStateCount := 2 linearlyEvolvedStateCount := 2 sampledEvolutionTimeCount := 2 continuousStateHistoryCount := 0 theorem universal_linear_dynamics_labels_do_not_supply_continuous_state_evolution : universalLinearEvolutionWithoutContinuousHistory.HasUniversalLinearEvolution ∧ ¬universalLinearEvolutionWithoutContinuousHistory.HasContinuousStateEvolution := by norm_num [ReducedDynamicsReadout.HasUniversalLinearEvolution, ReducedDynamicsReadout.HasContinuousStateEvolution, universalLinearEvolutionWithoutContinuousHistory] open OriginalRelativeSubsystemReadout open OriginalCalibratedBranchMemoryReadout open OriginalFiniteProductMeasureReadout open OriginalObserverInterventionReadout noncomputable def nonzeroCoefficientWithWrongRelativeNormalization : OriginalRelativeSubsystemReadout := { physicalThreeFifthsFourFifthsRelativeStates with firstRelativeNormalizationValue := 1 } theorem a_nonzero_composite_coefficient_does_not_fix_relative_state_normalization : 0 < nonzeroCoefficientWithWrongRelativeNormalization.firstFirstCoefficientValue ∧ ¬(nonzeroCoefficientWithWrongRelativeNormalization.firstRelativeNormalizationValue ^ 2 = nonzeroCoefficientWithWrongRelativeNormalization.firstFirstCoefficientValue ^ 2 + nonzeroCoefficientWithWrongRelativeNormalization.firstSecondCoefficientValue ^ 2) := by norm_num [nonzeroCoefficientWithWrongRelativeNormalization, physicalThreeFifthsFourFifthsRelativeStates] noncomputable def normalizedFactorizedCompositeState : OriginalRelativeSubsystemReadout := { physicalThreeFifthsFourFifthsRelativeStates with firstFirstCoefficientValue := 1 secondSecondCoefficientValue := 0 } theorem normalization_does_not_make_a_composite_state_nonfactorizable : normalizedFactorizedCompositeState.firstFirstCoefficientValue ^ 2 + normalizedFactorizedCompositeState.firstSecondCoefficientValue ^ 2 + normalizedFactorizedCompositeState.secondFirstCoefficientValue ^ 2 + normalizedFactorizedCompositeState.secondSecondCoefficientValue ^ 2 = 1 ∧ ¬(normalizedFactorizedCompositeState.firstFirstCoefficientValue * normalizedFactorizedCompositeState.secondSecondCoefficientValue - normalizedFactorizedCompositeState.firstSecondCoefficientValue * normalizedFactorizedCompositeState.secondFirstCoefficientValue ≠ 0) := by norm_num [normalizedFactorizedCompositeState, physicalThreeFifthsFourFifthsRelativeStates] noncomputable def firstRelativeStateWithWrongSecondRelativeState : OriginalRelativeSubsystemReadout := { physicalThreeFifthsFourFifthsRelativeStates with secondRelativeFirstComponentValue := 1 } theorem the_first_conditioned_subsystem_state_does_not_fix_the_second : firstRelativeStateWithWrongSecondRelativeState.firstRelativeFirstComponentValue = firstRelativeStateWithWrongSecondRelativeState.firstFirstCoefficientValue / firstRelativeStateWithWrongSecondRelativeState.firstRelativeNormalizationValue ∧ ¬(firstRelativeStateWithWrongSecondRelativeState.secondRelativeFirstComponentValue = firstRelativeStateWithWrongSecondRelativeState.secondFirstCoefficientValue / firstRelativeStateWithWrongSecondRelativeState.secondRelativeNormalizationValue) := by norm_num [firstRelativeStateWithWrongSecondRelativeState, physicalThreeFifthsFourFifthsRelativeStates] theorem distinct_relative_states_do_not_supply_an_independent_absolute_state : physicalThreeFifthsFourFifthsRelativeStates.firstRelativeFirstComponentValue ≠ physicalThreeFifthsFourFifthsRelativeStates.secondRelativeFirstComponentValue ∧ ¬(0 < physicalThreeFifthsFourFifthsRelativeStates.independentlyAssignedAbsoluteStateCountValue) := by norm_num [physicalThreeFifthsFourFifthsRelativeStates] noncomputable def firstCalibrationWithoutSecondCalibration : OriginalCalibratedBranchMemoryReadout := { physicalUnequalTwoBranchObserverMemory with secondObserverRecordValue := 0 } theorem calibration_of_one_eigenstate_does_not_calibrate_the_other : firstCalibrationWithoutSecondCalibration.firstObserverRecordValue = firstCalibrationWithoutSecondCalibration.firstObjectOutcomeValue ∧ ¬(firstCalibrationWithoutSecondCalibration.secondObserverRecordValue = firstCalibrationWithoutSecondCalibration.secondObjectOutcomeValue) := by norm_num [firstCalibrationWithoutSecondCalibration, physicalUnequalTwoBranchObserverMemory] noncomputable def firstLinearAmplitudeWithoutSecondAmplitude : OriginalCalibratedBranchMemoryReadout := { physicalUnequalTwoBranchObserverMemory with secondOutputAmplitudeValue := 0 } theorem preserving_one_superposition_coefficient_does_not_preserve_the_other : firstLinearAmplitudeWithoutSecondAmplitude.firstOutputAmplitudeValue = firstLinearAmplitudeWithoutSecondAmplitude.firstInputAmplitudeValue ∧ ¬(firstLinearAmplitudeWithoutSecondAmplitude.secondOutputAmplitudeValue = firstLinearAmplitudeWithoutSecondAmplitude.secondInputAmplitudeValue) := by norm_num [firstLinearAmplitudeWithoutSecondAmplitude, physicalUnequalTwoBranchObserverMemory] theorem two_retained_relative_branches_do_not_select_one_global_outcome : physicalUnequalTwoBranchObserverMemory.retainedBranchCountValue = 2 ∧ ¬(physicalUnequalTwoBranchObserverMemory.globallySelectedOutcomeCountValue = 1) := by norm_num [physicalUnequalTwoBranchObserverMemory] theorem one_definite_relative_memory_does_not_delete_the_other_branch : physicalUnequalTwoBranchObserverMemory.firstObserverRecordValue = physicalUnequalTwoBranchObserverMemory.firstObjectOutcomeValue ∧ ¬(physicalUnequalTwoBranchObserverMemory.retainedBranchCountValue = 1) := by norm_num [physicalUnequalTwoBranchObserverMemory] theorem two_equally_counted_branches_do_not_have_equal_square_amplitude_weight : physicalUnequalTwoBranchObserverMemory.retainedBranchCountValue = 2 ∧ ¬(physicalUnequalTwoBranchObserverMemory.firstBranchWeightValue = physicalUnequalTwoBranchObserverMemory.secondBranchWeightValue) := by norm_num [physicalUnequalTwoBranchObserverMemory] theorem an_amplitude_phase_reversal_does_not_preserve_the_signed_amplitude : physicalUnequalTwoBranchObserverMemory.phaseReversedFirstWeightValue = physicalUnequalTwoBranchObserverMemory.firstBranchWeightValue ∧ ¬(physicalUnequalTwoBranchObserverMemory.phaseReversedFirstAmplitudeValue = physicalUnequalTwoBranchObserverMemory.firstInputAmplitudeValue) := by norm_num [physicalUnequalTwoBranchObserverMemory] noncomputable def firstBranchRepeatWithoutSecondBranchRepeat : OriginalCalibratedBranchMemoryReadout := { physicalUnequalTwoBranchObserverMemory with secondRepeatedRecordValue := 0 } theorem repeatability_in_one_relative_branch_does_not_prove_the_other_branch : firstBranchRepeatWithoutSecondBranchRepeat.firstRepeatedRecordValue = firstBranchRepeatWithoutSecondBranchRepeat.firstObserverRecordValue ∧ ¬(firstBranchRepeatWithoutSecondBranchRepeat.secondRepeatedRecordValue = firstBranchRepeatWithoutSecondBranchRepeat.secondObserverRecordValue) := by norm_num [firstBranchRepeatWithoutSecondBranchRepeat, physicalUnequalTwoBranchObserverMemory] noncomputable def singleOutcomeWeightsWithoutMixedProduct : OriginalFiniteProductMeasureReadout := { physicalUnequalTwoObservationProductMeasure with firstSecondSequenceWeightValue := 1 / 2 } theorem normalized_single_observation_weights_do_not_supply_a_sequence_product : singleOutcomeWeightsWithoutMixedProduct.firstOutcomeWeightValue + singleOutcomeWeightsWithoutMixedProduct.secondOutcomeWeightValue = 1 ∧ ¬(singleOutcomeWeightsWithoutMixedProduct.firstSecondSequenceWeightValue = singleOutcomeWeightsWithoutMixedProduct.firstOutcomeWeightValue * singleOutcomeWeightsWithoutMixedProduct.secondOutcomeWeightValue) := by norm_num [singleOutcomeWeightsWithoutMixedProduct, physicalUnequalTwoObservationProductMeasure] rfl noncomputable def firstProductWithoutReversedSequenceProduct : OriginalFiniteProductMeasureReadout := { physicalUnequalTwoObservationProductMeasure with secondFirstSequenceWeightValue := 143 / 625 } theorem one_sequence_product_does_not_fix_the_reverse_sequence_weight : firstProductWithoutReversedSequenceProduct.firstSecondSequenceWeightValue = firstProductWithoutReversedSequenceProduct.firstOutcomeWeightValue * firstProductWithoutReversedSequenceProduct.secondOutcomeWeightValue ∧ ¬(firstProductWithoutReversedSequenceProduct.secondFirstSequenceWeightValue = firstProductWithoutReversedSequenceProduct.secondOutcomeWeightValue * firstProductWithoutReversedSequenceProduct.firstOutcomeWeightValue) := by norm_num [firstProductWithoutReversedSequenceProduct, physicalUnequalTwoObservationProductMeasure] theorem counting_mixed_branches_does_not_give_their_square_amplitude_measure : physicalUnequalTwoObservationProductMeasure.branchCountingMixedFractionValue = (physicalUnequalTwoObservationProductMeasure.mixedSequenceCountValue : Real) / physicalUnequalTwoObservationProductMeasure.totalSequenceCountValue ∧ ¬(physicalUnequalTwoObservationProductMeasure.mixedSequenceWeightValue = physicalUnequalTwoObservationProductMeasure.branchCountingMixedFractionValue) := by norm_num [physicalUnequalTwoObservationProductMeasure] theorem a_normalized_product_measure_does_not_remove_positive_measure_finite_exceptions : physicalUnequalTwoObservationProductMeasure.totalSequenceWeightValue = 1 ∧ ¬(physicalUnequalTwoObservationProductMeasure.finiteExceptionalMeasureValue = 0) := by norm_num [physicalUnequalTwoObservationProductMeasure] theorem a_vanishing_asymptotic_exceptional_measure_does_not_vanish_at_finite_length : Filter.Tendsto physicalUnequalTwoObservationProductMeasure.exceptionalTailValueAt Filter.atTop (nhds 0) ∧ ¬(physicalUnequalTwoObservationProductMeasure.finiteExceptionalMeasureValue = 0) := by have source := original_product_measure_differs_from_branch_counting_and_retains_finite_exceptions rcases source.2.2 with ⟨_length, _frequency, _tolerance, _deviation, _exceptionCount, _positiveFinite, _finiteWeight, _positiveLater, _decreasing, _initialTail, _laterTail, _zeroLimit, _classification, _productHistory, convergence⟩ constructor · simpa [physicalUnequalTwoObservationProductMeasure] using convergence · norm_num [physicalUnequalTwoObservationProductMeasure] theorem a_decreasing_exceptional_tail_does_not_remove_the_next_finite_exception : physicalUnequalTwoObservationProductMeasure.laterExceptionalMeasureValue < physicalUnequalTwoObservationProductMeasure.finiteExceptionalMeasureValue ∧ ¬(physicalUnequalTwoObservationProductMeasure.laterExceptionalMeasureValue = 0) := by norm_num [physicalUnequalTwoObservationProductMeasure] theorem one_finite_memory_sequence_need_not_have_the_born_frequency : physicalUnequalTwoObservationProductMeasure.selectedFirstOutcomeFrequencyValue = (physicalUnequalTwoObservationProductMeasure.selectedFirstOutcomeCountValue : Real) / physicalUnequalTwoObservationProductMeasure.selectedSequenceLengthValue ∧ ¬(physicalUnequalTwoObservationProductMeasure.selectedFirstOutcomeFrequencyValue = physicalUnequalTwoObservationProductMeasure.firstOutcomeWeightValue) := by norm_num [physicalUnequalTwoObservationProductMeasure] theorem a_small_finite_exceptional_measure_does_not_eliminate_exceptional_sequences : physicalUnequalTwoObservationProductMeasure.finiteExceptionalMeasureValue < physicalUnequalTwoObservationProductMeasure.frequencyToleranceValue ∧ ¬(physicalUnequalTwoObservationProductMeasure.finiteExceptionalSequenceCountValue = 0) := by norm_num [physicalUnequalTwoObservationProductMeasure] noncomputable def correctSelectedProductWithWrongTotalNormalization : OriginalFiniteProductMeasureReadout := { physicalUnequalTwoObservationProductMeasure with totalSequenceWeightValue := 0 } theorem one_correct_sequence_product_does_not_normalize_all_memory_sequences : correctSelectedProductWithWrongTotalNormalization.firstFirstSequenceWeightValue = correctSelectedProductWithWrongTotalNormalization.firstOutcomeWeightValue ^ 2 ∧ ¬(correctSelectedProductWithWrongTotalNormalization.totalSequenceWeightValue = 1) := by norm_num [correctSelectedProductWithWrongTotalNormalization, physicalUnequalTwoObservationProductMeasure] theorem observer_agreement_does_not_prevent_a_noncommuting_local_disturbance : physicalCommunicatingLocalAndRemoteObservers.firstCommunicatedRecordValue = physicalCommunicatingLocalAndRemoteObservers.secondCommunicatedRecordValue ∧ ¬(physicalCommunicatingLocalAndRemoteObservers.localNoncommutingFirstRecordValue = physicalCommunicatingLocalAndRemoteObservers.localNoncommutingRepeatedRecordValue) := by norm_num [physicalCommunicatingLocalAndRemoteObservers] theorem a_noncommuting_local_disturbance_does_not_disturb_a_remote_repeat : physicalCommunicatingLocalAndRemoteObservers.localNoncommutingFirstRecordValue ≠ physicalCommunicatingLocalAndRemoteObservers.localNoncommutingRepeatedRecordValue ∧ ¬(physicalCommunicatingLocalAndRemoteObservers.remoteFirstRecordValue ≠ physicalCommunicatingLocalAndRemoteObservers.remoteRepeatedRecordValue) := by norm_num [physicalCommunicatingLocalAndRemoteObservers] theorem remote_noninteraction_does_not_make_local_observables_commute : physicalCommunicatingLocalAndRemoteObservers.remoteInteractionStrengthValue = 0 ∧ ¬(physicalCommunicatingLocalAndRemoteObservers.localCommutatorResidualValue = 0) := by norm_num [physicalCommunicatingLocalAndRemoteObservers] theorem uninterrupted_repeatability_does_not_survive_a_noncommuting_intervention : physicalCommunicatingLocalAndRemoteObservers.uninterruptedFirstRecordValue = physicalCommunicatingLocalAndRemoteObservers.uninterruptedRepeatedRecordValue ∧ ¬(physicalCommunicatingLocalAndRemoteObservers.localNoncommutingFirstRecordValue = physicalCommunicatingLocalAndRemoteObservers.localNoncommutingRepeatedRecordValue) := by norm_num [physicalCommunicatingLocalAndRemoteObservers] namespace PhysicalRecords open CoherentRecordMeasurement noncomputable def unequalComplexProcess : Process Bool where inputAmplitude := fun outcome => if outcome then Complex.mk 0 (4 / 5) else Complex.mk (3 / 5) 0 measurement := recordingMap communication := communicationMap theorem unequal_complex_process_has_actual_calibrated_inputs : unequalComplexProcess.ComparisonInputs := by refine ⟨⟨?_, recording_map_is_calibrated⟩, communication_map_is_calibrated⟩ norm_num [Process.NormalizedInput, unequalComplexProcess, Fintype.sum_bool, Complex.normSq_apply] rfl theorem unequal_complex_process_retains_two_nonzero_amplitudes : unequalComplexProcess.inputAmplitude false ≠ 0 ∧ unequalComplexProcess.inputAmplitude true ≠ 0 := by norm_num [unequalComplexProcess, Complex.ext_iff] theorem actual_communication_derives_record_agreement : unequalComplexProcess.NonvacuousRecordComparisonAt := unequalComplexProcess.comparison_inputs_derive_nonvacuous_record_result unequal_complex_process_has_actual_calibrated_inputs theorem record_agreement_does_not_produce_a_single_outcome_state : unequalComplexProcess.NonvacuousRecordComparisonAt ∧ ¬∃ outcome, unequalComplexProcess.HasCertainComparedOutcome outcome := by refine ⟨actual_communication_derives_record_agreement, ?_⟩ rintro ⟨outcome, certain⟩ have inputs := unequal_complex_process_has_actual_calibrated_inputs have supports := unequal_complex_process_retains_two_nonzero_amplitudes exact unequalComplexProcess.two_supported_alternatives_exclude_certain_compared_outcome inputs.1.2 inputs.2 false true (by decide) supports.1 supports.2 outcome certain /-- Padding a ready register is an isometric embedding, not a communication. -/ def unreadRegisterMap : JointState Bool →ₗ[Complex] ComparedState Bool where toFun := fun state triple => if triple.2.2 then 0 else state (triple.1, triple.2.1) map_add' := by intros; ext triple; cases h : triple.2.2 <;> simp [h] map_smul' := by intros; ext triple; cases h : triple.2.2 <;> simp [h] noncomputable def uncommunicatedProcess : Process Bool := { unequalComplexProcess with communication := unreadRegisterMap } theorem unread_register_keeps_the_actual_norm : squaredNorm uncommunicatedProcess.comparedState = 1 := by norm_num [squaredNorm, Process.comparedState, Process.measuredState, uncommunicatedProcess, unequalComplexProcess, unreadRegisterMap, recordingMap, diagonalState, Fintype.sum_prod_type, Fintype.sum_bool, Complex.normSq_apply] rfl theorem correlated_measurement_does_not_supply_communication : (uncommunicatedProcess.MeasurementInputs ∧ HasCertainCorrelation uncommunicatedProcess.measuredState ∧ squaredNorm uncommunicatedProcess.comparedState = 1) ∧ ¬uncommunicatedProcess.NonvacuousRecordComparisonAt := by have inputs : uncommunicatedProcess.MeasurementInputs := unequal_complex_process_has_actual_calibrated_inputs.1 refine ⟨⟨inputs, uncommunicatedProcess.measured_state_has_certain_correlation inputs, unread_register_keeps_the_actual_norm⟩, ?_⟩ intro agreement have supported : uncommunicatedProcess.comparedState (true, true, false) ≠ 0 := by norm_num [Process.comparedState, Process.measuredState, uncommunicatedProcess, unequalComplexProcess, unreadRegisterMap, recordingMap, diagonalState, Complex.ext_iff] have incompatible := agreement.1.2.2 (true, true, false) supported change true = false at incompatible cases incompatible noncomputable def retainedInterbranchCoherence : Complex := unequalComplexProcess.comparedState (false, false, false) * star (unequalComplexProcess.comparedState (true, true, true)) theorem actual_records_retain_complex_interbranch_coherence : retainedInterbranchCoherence = Complex.mk 0 (-12 / 25) := by apply Complex.ext <;> norm_num [retainedInterbranchCoherence, Process.comparedState, Process.measuredState, unequalComplexProcess, recordingMap, communicationMap, diagonalState, communicatedState] rfl theorem communicating_records_do_not_remove_global_coherence : unequalComplexProcess.NonvacuousRecordComparisonAt ∧ ¬retainedInterbranchCoherence = 0 := by refine ⟨actual_communication_derives_record_agreement, ?_⟩ rw [actual_records_retain_complex_interbranch_coherence] norm_num [Complex.ext_iff] end PhysicalRecords end Countermodels end RelativeStateFramework end PhysicsLogic.Papers.Everett1957