import PhysicsLogic.Philosophy.DescriptiveCompleteness import PhysicsLogic.Philosophy.EpistemicStatus import PhysicsLogic.Framework.DeterministicLocalResponse import PhysicsLogic.Framework.RemoteCorrelationPrediction import PhysicsLogic.Framework.Entanglement import PhysicsLogic.Paradigm.Locality import Mathlib.Analysis.SpecialFunctions.Pow.Real import Mathlib.Data.Real.Sqrt import Mathlib.Tactic.Linarith import Mathlib.Tactic.NormNum /-! # Formal Logic of Bell's 1964 No-Go Argument This file formalizes Bell's deductive structure. Lean checks the dichotomic algebra deriving the 1964 inequality from explicit hidden-average laws. The quantum correlation calculation and the remaining physical bridge principles stay explicit hypotheses. -/ set_option autoImplicit false noncomputable section namespace PhysicsLogic.Papers.Bell1964 open PhysicsLogic.Philosophy.DescriptiveCompleteness open PhysicsLogic.Philosophy.EpistemicStatus open PhysicsLogic.Framework universe u v w x y z inductive Outcome where | plus | minus deriving DecidableEq, Repr inductive BellRemoteTheory where | singletQuantumDescription inductive BellRemoteWorld where | separatedSpinPairExperiment inductive BellLocalResponseTheory where | candidateDeterministicCompletion /-- Typed token for Bell's section-II deterministic local-response derivation. The constructor records the complete-state reading of `lambda`; the raw source relation below supplies the actual proposition-valued premises. -/ inductive BellDeterministicLocalResponseDerivation where | completeStateLocalResponseFunctions deriving DecidableEq, Repr /-- Bell-local predetermined responses `A(a, lambda)` and `B(b, lambda)`. -/ abbrev LocalResponses (Setting : Type u) (HiddenState : Type v) := PhysicsLogic.Framework.DeterministicLocalResponse.LocalResponses Setting HiddenState Outcome /-- Predetermined bipartite responses before locality is imposed. Each wing may depend on both apparatus settings and the shared hidden state. -/ abbrev BipartiteResponses (Setting : Type u) (HiddenState : Type v) := PhysicsLogic.Framework.DeterministicLocalResponse.BipartiteResponses Setting HiddenState Outcome /-- Operations needed to state Bell's original inequality abstractly. -/ structure CorrelationOrder (Value : Type x) where one : Value add : Value → Value → Value sub : Value → Value → Value mul : Value → Value → Value neg : Value → Value magnitude : Value → Value le : Value → Value → Prop lt : Value → Value → Prop namespace CorrelationOrder def Consistent {Value : Type x} (order : CorrelationOrder Value) : Prop := ∀ left right, order.le left right → ¬order.lt right left end CorrelationOrder /-- A spatial Stern-Gerlach orientation. -/ structure SpinDirection where x : Real y : Real z : Real /-- Bell's section-III single-spin hidden-variable construction. The data retain the physical choices in equations (4)-(7): a pure-state polarization, a hidden direction distributed on its positive hemisphere, a measurement-dependent rotated direction, a dichotomic sign response, and the average used to compare with the quantum expectation. Uniformity and the integral calculation are propositions below rather than baked into the data. -/ structure SingleSpinIllustrationData where polarization : SpinDirection rotatedDirection : SpinDirection → SpinDirection angleToPolarization : SpinDirection → Real rotatedAngleToPolarization : SpinDirection → Real response : SpinDirection → SpinDirection → Outcome average : (SpinDirection → Real) → Real uniformOn : (SpinDirection → Prop) → Prop /-- The operational procedure Bell uses to predict a remote spin component: measure that same component on the opposite member of the singlet pair. -/ structure MatchingSpinMeasurement (Setting : Type u) where component : Setting /-- The physical system selected in Bell's section-II EPR step: two spin-one-half particles prepared with total spin zero. Spins are stored in twice-spin units so the paper-local data remain exact natural numbers without importing additional mathematical representation. Primary-source anchor: section II, pp. 195-196. -/ structure BellSingletExperiment where particleCount : Nat constituentTwiceSpin : Nat totalTwiceSpin : Nat deriving DecidableEq, Repr /-- The two distinct members of Bell's separated spin pair. -/ inductive BellParticle where | first | second deriving DecidableEq, Repr /-- Stages distinguished by Bell's preparation-and-separation argument. Primary-source anchor: section II, pp. 195-196. -/ inductive BellCorrelationStage where | commonPreparation | separatedMeasurement deriving DecidableEq, Repr /-- Typed token for Bell's section-II remote-prediction derivation. -/ inductive BellRemoteCorrelationDerivation where | singletAnticorrelationMatchingMeasurementAndOperationalLocality deriving DecidableEq, Repr /-- Bell's selected two-particle spin singlet. -/ def selectedBellSingletExperiment : BellSingletExperiment where particleCount := 2 constituentTwiceSpin := 1 totalTwiceSpin := 0 /-- The remote-prediction route is evaluated after the pair is separated. -/ def selectedBellCorrelationStage : BellCorrelationStage := .separatedMeasurement namespace SpinDirection def dot (left right : SpinDirection) : Real := left.x * right.x + left.y * right.y + left.z * right.z def normSquared (direction : SpinDirection) : Real := direction.dot direction def IsUnit (direction : SpinDirection) : Prop := direction.normSquared = 1 end SpinDirection def orderedRingCorrelationOrder (Value : Type x) [Ring Value] [LinearOrder Value] [IsStrictOrderedRing Value] : CorrelationOrder Value := { one := 1 add := (· + ·) sub := (· - ·) mul := (· * ·) neg := (- ·) magnitude := abs le := (· ≤ ·) lt := (· < ·) } def realCorrelationOrder : CorrelationOrder Real := orderedRingCorrelationOrder Real def singletCorrelation (left right : SpinDirection) : Real := -(left.dot right) /-- The temporal and one-dimensional spatial displacement from the setting event to the remote reading event in a chosen inertial frame. -/ structure InfluenceSeparation where temporal : Real spatial : Real private def inverseSqrtTwo : Real := Real.sqrt 2 / 2 /-- Bell's settings with `a·c=0` and `a·b=b·c=1/sqrt(2)`. -/ def bellDirectionA : SpinDirection := { x := inverseSqrtTwo, y := inverseSqrtTwo, z := 0 } def bellDirectionB : SpinDirection := { x := 1, y := 0, z := 0 } def bellDirectionC : SpinDirection := { x := inverseSqrtTwo, y := -inverseSqrtTwo, z := 0 } theorem bell_directions_are_unit : bellDirectionA.IsUnit ∧ bellDirectionB.IsUnit ∧ bellDirectionC.IsUnit := by have squareRoot : (Real.sqrt 2) ^ 2 = 2 := Real.sq_sqrt (by norm_num) constructor · unfold SpinDirection.IsUnit SpinDirection.normSquared simp [SpinDirection.dot, bellDirectionA, inverseSqrtTwo] nlinarith · constructor · norm_num [SpinDirection.IsUnit, SpinDirection.normSquared, SpinDirection.dot, bellDirectionB] · unfold SpinDirection.IsUnit SpinDirection.normSquared simp [SpinDirection.dot, bellDirectionC, inverseSqrtTwo] nlinarith theorem bell_directions_have_paper_dot_products : bellDirectionA.dot bellDirectionC = 0 ∧ bellDirectionA.dot bellDirectionB = inverseSqrtTwo ∧ bellDirectionB.dot bellDirectionC = inverseSqrtTwo := by have squareRoot : (Real.sqrt 2) ^ 2 = 2 := Real.sq_sqrt (by norm_num) constructor · simp [SpinDirection.dot, bellDirectionA, bellDirectionC, inverseSqrtTwo] · constructor <;> simp [SpinDirection.dot, bellDirectionA, bellDirectionB, bellDirectionC, inverseSqrtTwo] /-- Paper-local semantic framework for Bell's models and correlations. -/ structure BellFramework (Setting : Type u) (HiddenState : Type v) (Model : Type w) (Value : Type x) (Error : Type y) where order : CorrelationOrder Value bipartiteResponses : Model → BipartiteResponses Setting HiddenState modelCorrelation : Model → Setting → Setting → Value quantumCorrelation : Setting → Setting → Value settingDotProduct : Setting → Setting → Value correlationIsPerfectlyAnticorrelatedAtEqualSettings : (Setting → Setting → Value) → Prop hiddenStateDistributionIsNormalized : Model → Prop correlationIsAverageOfResponses : LocalResponses Setting HiddenState → (Setting → Setting → Value) → Prop correlationIsAverageOfBipartiteResponses : BipartiteResponses Setting HiddenState → (Setting → Setting → Value) → Prop responsesAreOppositeAlmostEverywhere : LocalResponses Setting HiddenState → Prop correlationHasSingleResponseForm : LocalResponses Setting HiddenState → (Setting → Setting → Value) → Prop uniformlyApproximates : (Setting → Setting → Value) → (Setting → Setting → Value) → Error → Prop errorMagnitude : Error → Real angularAverageAt : (Setting → Setting → Value) → (Setting → Setting → Value) → Error → Prop averagedLocalResponseBoundsAt : Model → (Setting → Setting → Value) → Error → Prop averagedUniformErrorBoundAt : (Setting → Setting → Value) → (Setting → Setting → Value) → Error → Prop equalSettingAveragedAnticorrelationEstimateAt : Model → (Setting → Setting → Value) → Error → Error → Prop threeSettingAveragedDifferenceEstimateAt : Model → (Setting → Setting → Value) → Error → Error → Prop singleParticleHiddenVariableAccount : Model → Prop singleParticleIllustration : Model → SingleSpinIllustrationData restrictedBipartiteLocalAccount : Model → Prop influenceSeparation : Model → InfluenceSeparation lorentzInvariant : Model → Prop namespace BellFramework variable {Setting : Type u} {HiddenState : Type v} {Model : Type w} {Value : Type x} {Error : Type y} /-- Bell's error scales have physically positive real magnitude. -/ def positiveError (framework : BellFramework Setting HiddenState Model Value Error) (error : Error) : Prop := 0 < framework.errorMagnitude error def Correlation (Setting : Type u) (Value : Type x) : Type (max u x) := Setting → Setting → Value /-- The selected data of Bell's equations (16)-(22). The same angular window is used to average both the local and quantum correlations, while the selected positive error is the epsilon challenged by the final lower bound. Primary-source anchor: section IV, pp. 198-199. -/ structure AveragedSettingAnalysis (Setting : Type u) (Value : Type x) (Error : Type y) where angularWindow : Error approximationError : Error averagedModelCorrelation : Correlation Setting Value averagedQuantumCorrelation : Correlation Setting Value /-- The hidden-state average in Bell's equation (14). The operator is data. `BellResponseAverageLaws` below restricts its required laws to the response products used in equation (15). The stronger all-function laws below remain available, but are not required of a general probability integral. -/ structure HiddenAverage (HiddenState : Type v) (Value : Type x) where value : (HiddenState → Value) → Value namespace HiddenAverage variable {HiddenState : Type v} {Value : Type x} def PreservesSubtraction (average : HiddenAverage HiddenState Value) (sub : Value → Value → Value) : Prop := ∀ left right, average.value (fun hiddenState => sub (left hiddenState) (right hiddenState)) = sub (average.value left) (average.value right) def PreservesConstants (average : HiddenAverage HiddenState Value) : Prop := ∀ constant, average.value (fun _ => constant) = constant def SatisfiesAbsoluteBound (average : HiddenAverage HiddenState Value) (magnitude : Value → Value) (le : Value → Value → Prop) : Prop := ∀ integrand, le (magnitude (average.value integrand)) (average.value (fun hiddenState => magnitude (integrand hiddenState))) end HiddenAverage def outcomeValue (order : CorrelationOrder Value) (outcome : Outcome) : Value := match outcome with | .plus => order.one | .minus => order.neg order.one /-- The numerical value of Bell's single-spin sign response. -/ def singleSpinOutcomeValue (outcome : Outcome) : Real := match outcome with | .plus => 1 | .minus => -1 theorem singleSpinOutcomeValue_preserves_generic_encoding : singleSpinOutcomeValue = outcomeValue realCorrelationOrder := by funext outcome cases outcome <;> rfl namespace SingleSpinIllustrationData /-- The positive unit hemisphere selected by the pure-state polarization. -/ def PolarizedHemisphere (data : SingleSpinIllustrationData) (hiddenDirection : SpinDirection) : Prop := hiddenDirection.IsUnit ∧ 0 < hiddenDirection.dot data.polarization /-- The physical geometry of Bell's pure spin state and the two angles used in equations (5)-(7). -/ def HasPolarizedPureSpinGeometry (data : SingleSpinIllustrationData) : Prop := data.polarization.IsUnit ∧ ∀ measurementDirection, measurementDirection.IsUnit → (data.rotatedDirection measurementDirection).IsUnit ∧ measurementDirection.dot data.polarization = Real.cos (data.angleToPolarization measurementDirection) ∧ (data.rotatedDirection measurementDirection).dot data.polarization = Real.cos (data.rotatedAngleToPolarization measurementDirection) /-- Bell's hidden direction has the uniform law on the selected hemisphere. -/ def HasUniformPolarizedHemisphereLaw (data : SingleSpinIllustrationData) : Prop := data.uniformOn (PolarizedHemisphere data) /-- Equation (4), away from the zero-dot-product boundary whose probability Bell sets aside separately. -/ def ResponseUsesRotatedSignAwayFromBoundary (data : SingleSpinIllustrationData) : Prop := ∀ measurementDirection hiddenDirection, (0 < hiddenDirection.dot (data.rotatedDirection measurementDirection) → data.response measurementDirection hiddenDirection = .plus) ∧ (hiddenDirection.dot (data.rotatedDirection measurementDirection) < 0 → data.response measurementDirection hiddenDirection = .minus) /-- The unresolved sign boundary in equation (4) has zero probability. -/ def BoundaryHasZeroAverageWeight (data : SingleSpinIllustrationData) : Prop := ∀ measurementDirection, data.average (fun hiddenDirection => if hiddenDirection.dot (data.rotatedDirection measurementDirection) = 0 then 1 else 0) = 0 /-- The hemisphere average evaluated in Bell's equation (5). -/ def HasHemisphereSignAverage (data : SingleSpinIllustrationData) : Prop := ∀ measurementDirection, measurementDirection.IsUnit → data.average (fun hiddenDirection => singleSpinOutcomeValue (data.response measurementDirection hiddenDirection)) = 1 - 2 * data.rotatedAngleToPolarization measurementDirection / Real.pi /-- The imported spherical-average calculation: the uniform hemisphere law, sign rule, and zero-weight boundary imply equation (5). -/ def UniformHemisphereSignAveragePrinciple (data : SingleSpinIllustrationData) : Prop := HasUniformPolarizedHemisphereLaw data → ResponseUsesRotatedSignAwayFromBoundary data → BoundaryHasZeroAverageWeight data → HasHemisphereSignAverage data /-- Bell's rotated-direction calibration, equation (6). -/ def HasRotationCalibration (data : SingleSpinIllustrationData) : Prop := ∀ measurementDirection, measurementDirection.IsUnit → 1 - 2 * data.rotatedAngleToPolarization measurementDirection / Real.pi = Real.cos (data.angleToPolarization measurementDirection) /-- The final single-spin quantum expectation, equation (7). -/ def ReproducesPureSpinExpectation (data : SingleSpinIllustrationData) : Prop := ∀ measurementDirection, measurementDirection.IsUnit → data.average (fun hiddenDirection => singleSpinOutcomeValue (data.response measurementDirection hiddenDirection)) = Real.cos (data.angleToPolarization measurementDirection) /-- All source-level clauses of Bell's section-III single-spin construction. -/ def SingleParticleConstructionComplete (data : SingleSpinIllustrationData) : Prop := HasPolarizedPureSpinGeometry data ∧ HasUniformPolarizedHemisphereLaw data ∧ ResponseUsesRotatedSignAwayFromBoundary data ∧ BoundaryHasZeroAverageWeight data ∧ HasHemisphereSignAverage data ∧ HasRotationCalibration data ∧ ReproducesPureSpinExpectation data end SingleSpinIllustrationData /-- Equations (5) and (6) alone compose to Bell's equation (7). -/ theorem single_spin_average_and_rotation_calibration_reproduce_quantum_expectation (data : SingleSpinIllustrationData) (averageLaw : SingleSpinIllustrationData.HasHemisphereSignAverage data) (calibration : SingleSpinIllustrationData.HasRotationCalibration data) : SingleSpinIllustrationData.ReproducesPureSpinExpectation data := by intro measurementDirection unitDirection rw [averageLaw measurementDirection unitDirection] exact calibration measurementDirection unitDirection /-- Equations (5) and (6) imply equation (7), with the spherical integral kept as an explicit imported calculation. -/ theorem single_spin_hemisphere_rotation_reproduces_quantum_expectation (data : SingleSpinIllustrationData) (hemisphereLaw : SingleSpinIllustrationData.HasUniformPolarizedHemisphereLaw data) (signRule : SingleSpinIllustrationData.ResponseUsesRotatedSignAwayFromBoundary data) (boundary : SingleSpinIllustrationData.BoundaryHasZeroAverageWeight data) (averagePrinciple : SingleSpinIllustrationData.UniformHemisphereSignAveragePrinciple data) (calibration : SingleSpinIllustrationData.HasRotationCalibration data) : SingleSpinIllustrationData.ReproducesPureSpinExpectation data := by have averageLaw := averagePrinciple hemisphereLaw signRule boundary exact single_spin_average_and_rotation_calibration_reproduce_quantum_expectation data averageLaw calibration def responseProduct (order : CorrelationOrder Value) (responses : LocalResponses Setting HiddenState) (left right : Setting) (hiddenState : HiddenState) : Value := order.mul (outcomeValue order (responses.left left hiddenState)) (outcomeValue order (responses.left right hiddenState)) /-- The exact averaging laws used in equation (15), not linearity on every hidden-state function. Only response-product differences, their absolute values, the constant one, and one minus a response product occur here. -/ def BellResponseAverageLaws (order : CorrelationOrder Value) (average : HiddenAverage HiddenState Value) (responses : LocalResponses Setting HiddenState) : Prop := (∀ a b c, average.value (fun state => order.sub (responseProduct order responses a c state) (responseProduct order responses a b state)) = order.sub (average.value (responseProduct order responses a c)) (average.value (responseProduct order responses a b))) ∧ average.value (fun _ => order.one) = order.one ∧ (∀ a b c, order.le (order.magnitude (average.value (fun state => order.sub (responseProduct order responses a c state) (responseProduct order responses a b state)))) (average.value (fun state => order.magnitude (order.sub (responseProduct order responses a c state) (responseProduct order responses a b state))))) ∧ (∀ b c, average.value (fun state => order.sub order.one (responseProduct order responses b c state)) = order.sub (average.value (fun _ => order.one)) (average.value (responseProduct order responses b c))) def IsSingleResponseAverage (order : CorrelationOrder Value) (average : HiddenAverage HiddenState Value) (responses : LocalResponses Setting HiddenState) (correlation : Correlation Setting Value) : Prop := ∀ left right, correlation left right = order.neg (average.value (responseProduct order responses left right)) /-- Bell's original inequality, eq. (15). -/ def SatisfiesBell1964Inequality (order : CorrelationOrder Value) (correlation : Correlation Setting Value) : Prop := ∀ a b c, order.le (order.magnitude (order.sub (correlation a b) (correlation a c))) (order.add order.one (correlation b c)) /-- A correlation violates Bell's original inequality for some three settings. -/ def ViolatesBell1964Inequality (order : CorrelationOrder Value) (correlation : Correlation Setting Value) : Prop := ∃ a b c, order.lt (order.add order.one (correlation b c)) (order.magnitude (order.sub (correlation a b) (correlation a c))) /-- Bell's own setting geometry gives a concrete violation of the original three-setting inequality for `P(a,b) = -a dot b`. -/ theorem singlet_correlation_violates_at_bell_directions : 1 + singletCorrelation bellDirectionB bellDirectionC < |singletCorrelation bellDirectionA bellDirectionB - singletCorrelation bellDirectionA bellDirectionC| := by rcases bell_directions_have_paper_dot_products with ⟨dotAC, dotAB, dotBC⟩ have inverseSqrtTwoNonnegative : 0 ≤ inverseSqrtTwo := by unfold inverseSqrtTwo exact div_nonneg (Real.sqrt_nonneg _) (by norm_num) have squareRoot : (Real.sqrt 2) ^ 2 = 2 := Real.sq_sqrt (by norm_num) have inverseSqrtTwoGreaterHalf : (1 : Real) / 2 < inverseSqrtTwo := by unfold inverseSqrtTwo have squareRootNonnegative : 0 ≤ Real.sqrt 2 := Real.sqrt_nonneg _ nlinarith change 1 + singletCorrelation bellDirectionB bellDirectionC < abs (singletCorrelation bellDirectionA bellDirectionB - singletCorrelation bellDirectionA bellDirectionC) simp only [singletCorrelation] rw [dotBC, dotAB, dotAC] simp only [neg_zero, sub_zero, abs_neg, abs_of_nonneg inverseSqrtTwoNonnegative] linarith theorem concrete_singlet_correlation_violates_bell_1964 : ViolatesBell1964Inequality realCorrelationOrder singletCorrelation := by exact ⟨bellDirectionA, bellDirectionB, bellDirectionC, singlet_correlation_violates_at_bell_directions⟩ /-- A model reproduces every quantum correlation in the scenario. -/ def ReproducesQuantumCorrelation (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) : Prop := ∀ a b, framework.modelCorrelation model a b = framework.quantumCorrelation a b /-- The singlet prediction has perfect anticorrelation at equal settings. -/ def QuantumPerfectAnticorrelation (framework : BellFramework Setting HiddenState Model Value Error) : Prop := framework.correlationIsPerfectlyAnticorrelatedAtEqualSettings framework.quantumCorrelation /-- Every spin component in Bell's EPR argument has an available same-component measurement procedure on the opposite wing. -/ def MatchingSpinMeasurementsAvailable (procedureAvailable : MatchingSpinMeasurement Setting → Prop) : Prop := ∀ component, procedureAvailable ⟨component⟩ /-- For every chosen remote component, its same-component procedure predicts the result with certainty. -/ def EveryChosenRemoteSpinResultPredictable (reality : RealityCriterionContext Setting (MatchingSpinMeasurement Setting) BellCorrelationStage) : Prop := ∀ component, reality.predictableWithCertainty ⟨component⟩ component selectedBellCorrelationStage /-- For every chosen remote component, the same-component procedure leaves that remote component undisturbed in Bell's separated experiment. -/ def EveryChosenRemoteSpinResultUndisturbed (reality : RealityCriterionContext Setting (MatchingSpinMeasurement Setting) BellCorrelationStage) : Prop := ∀ component, reality.leavesUndisturbed ⟨component⟩ component selectedBellCorrelationStage /-- The separated Stern-Gerlach arrangement includes an implementable same-component procedure for every selected spin direction. -/ def ExperimentProvidesMatchingSpinMeasurements (experimentSetup : Prop) (procedureAvailable : MatchingSpinMeasurement Setting → Prop) : Prop := experimentSetup → MatchingSpinMeasurementsAvailable procedureAvailable /-- Bell's singlet prediction `P(a,b) = -a dot b`, equation (3). -/ def QuantumSingletCorrelationFormula (framework : BellFramework Setting HiddenState Model Value Error) : Prop := ∀ left right, framework.quantumCorrelation left right = framework.order.neg (framework.settingDotProduct left right) /-- The quantum spin calculation supplies a violating triple for equation (15). Its exact input is the represented singlet correlation formula. -/ def QuantumSingletViolationCalculation (framework : BellFramework Setting HiddenState Model Value Error) : Prop := framework.QuantumSingletCorrelationFormula → ViolatesBell1964Inequality framework.order framework.quantumCorrelation /-- Specializing the singlet formula to equal settings gives anticorrelation. -/ def SingletFormulaGivesPerfectAnticorrelation (framework : BellFramework Setting HiddenState Model Value Error) : Prop := framework.QuantumSingletCorrelationFormula → framework.QuantumPerfectAnticorrelation /-- The unrestricted bipartite responses factor through Bell-local response functions: the left result is independent of the right setting and conversely. -/ def LocalResponsesFactorize (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (localResponses : LocalResponses Setting HiddenState) : Prop := PhysicsLogic.Framework.DeterministicLocalResponse.Factorizes (framework.bipartiteResponses model) localResponses /-- The deterministic paper-local response functions induce the generic joint possibility relation used by the paradigm layer. -/ def responsePossibility (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) : PhysicsLogic.Paradigm.Locality.BipartiteResponse Setting Outcome HiddenState := PhysicsLogic.Framework.DeterministicLocalResponse.responsePossibility (framework.bipartiteResponses model) /-- An explicit Bell-local response representation realizes the complete shared deterministic-local-response result, including generic factorization at every hidden state. -/ theorem bell_local_responses_make_factorization_route_applicable (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (localResponses : LocalResponses Setting HiddenState) (factorizes : framework.LocalResponsesFactorize model localResponses) : PhysicsLogic.Framework.DeterministicLocalResponse.FactorizationRouteApplicable (framework.bipartiteResponses model) localResponses := PhysicsLogic.Framework.DeterministicLocalResponse.factorization_makes_route_applicable (framework.bipartiteResponses model) localResponses factorizes theorem bell_local_responses_establish_deterministic_local_response (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (localResponses : LocalResponses Setting HiddenState) (factorizes : framework.LocalResponsesFactorize model localResponses) (domain : PhysicsLogic.Framework.DeterministicLocalResponse.NontrivialResponseDomain Setting HiddenState) : PhysicsLogic.Framework.DeterministicLocalResponse.EstablishedDeterministicLocalResponse (framework.bipartiteResponses model) localResponses := PhysicsLogic.Framework.DeterministicLocalResponse.applicable_route_establishes_deterministic_local_response (framework.bipartiteResponses model) localResponses domain (framework.bell_local_responses_make_factorization_route_applicable model localResponses factorizes) /-- Bell's exact local functional form and a nontrivial response domain realize the ordinary shared structural explanation. This remains a support-level statement and does not consume the hidden-state average or Bell inequality. -/ theorem bell_local_responses_realize_structural_deterministic_local_response_explanation (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (localResponses : LocalResponses Setting HiddenState) (factorizes : framework.LocalResponsesFactorize model localResponses) (domain : PhysicsLogic.Framework.DeterministicLocalResponse.NontrivialResponseDomain Setting HiddenState) : PhysicsLogic.Framework.DeterministicLocalResponse.DirectStructuralDeterministicLocalResponseExplanationAt (framework.bipartiteResponses model) localResponses := PhysicsLogic.Framework.DeterministicLocalResponse.factorization_and_domain_realize_structural_deterministic_local_response_explanation (framework.bipartiteResponses model) localResponses domain (framework.bell_local_responses_make_factorization_route_applicable model localResponses factorizes) theorem bell_local_responses_realize_every_shared_claim (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (localResponses : LocalResponses Setting HiddenState) (factorizes : framework.LocalResponsesFactorize model localResponses) (domain : PhysicsLogic.Framework.DeterministicLocalResponse.NontrivialResponseDomain Setting HiddenState) : ∀ claim, PhysicsLogic.Framework.DeterministicLocalResponse.DeterministicLocalResponseClaimHoldsAt (PhysicsLogic.Framework.DeterministicLocalResponse.deterministicLocalResponseCalculationModelAt (framework.bipartiteResponses model) localResponses) claim := PhysicsLogic.Framework.DeterministicLocalResponse.established_response_realizes_every_shared_claim (framework.bell_local_responses_establish_deterministic_local_response model localResponses factorizes domain) /-- Bell's local functional form realizes generic bipartite factorization at each hidden state. This bridge does not identify Bell locality with every other notion called locality. -/ theorem local_responses_realize_generic_factorization (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (localResponses : LocalResponses Setting HiddenState) (factorizes : framework.LocalResponsesFactorize model localResponses) (domain : PhysicsLogic.Framework.DeterministicLocalResponse.NontrivialResponseDomain Setting HiddenState) (hiddenState : HiddenState) : (framework.responsePossibility model).FactorizesAt hiddenState := PhysicsLogic.Framework.DeterministicLocalResponse.established_response_exposes_generic_factorization (framework.bipartiteResponses model) localResponses (framework.bell_local_responses_establish_deterministic_local_response model localResponses factorizes domain) hiddenState /-- Sections I-II, pp. 195-196: Bell's `lambda` is a more complete state specification, may represent initial values of variables, and supplies both local response functions in equation (1). At fixed settings, an explicitly supplied hidden-state value therefore support-screens the two outcomes. This is a support-level consequence, not a probability-factorization claim about the normalized hidden-state distribution. -/ theorem bell_hidden_state_realizes_common_cause_support_screening (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (localResponses : LocalResponses Setting HiddenState) (factorizes : framework.LocalResponsesFactorize model localResponses) (domain : PhysicsLogic.Framework.DeterministicLocalResponse.NontrivialResponseDomain Setting HiddenState) (hiddenState : HiddenState) (leftSetting rightSetting : Setting) : (PhysicsLogic.Framework.DeterministicLocalResponse.supportScreeningContext (framework.bipartiteResponses model) localResponses |>.HasSupportScreenedCommonCauseAt (leftSetting, rightSetting)) := PhysicsLogic.Framework.DeterministicLocalResponse.established_response_exposes_common_cause_support_screening (framework.bipartiteResponses model) localResponses (framework.bell_local_responses_establish_deterministic_local_response model localResponses factorizes domain) hiddenState leftSetting rightSetting theorem bell_local_responses_have_rectangular_joint_support (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (localResponses : LocalResponses Setting HiddenState) (factorizes : framework.LocalResponsesFactorize model localResponses) (domain : PhysicsLogic.Framework.DeterministicLocalResponse.NontrivialResponseDomain Setting HiddenState) (hiddenState : HiddenState) : (framework.responsePossibility model).RectangularAt hiddenState := PhysicsLogic.Framework.DeterministicLocalResponse.established_response_has_rectangular_joint_support (framework.bipartiteResponses model) localResponses (framework.bell_local_responses_establish_deterministic_local_response model localResponses factorizes domain) hiddenState /-- Section II, pp. 195-196: Bell-local deterministic responses have total joint support and are no-signalling at the level of possible outcomes. This is a consequence of, not a replacement for, Bell's stronger factorization premise. -/ theorem bell_local_responses_realize_total_no_signalling_support (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (localResponses : LocalResponses Setting HiddenState) (factorizes : framework.LocalResponsesFactorize model localResponses) (domain : PhysicsLogic.Framework.DeterministicLocalResponse.NontrivialResponseDomain Setting HiddenState) (hiddenState : HiddenState) : (framework.responsePossibility model).TotalJointSupportAt hiddenState ∧ (framework.responsePossibility model).NoSignallingAt hiddenState := by let established := framework.bell_local_responses_establish_deterministic_local_response model localResponses factorizes domain exact ⟨PhysicsLogic.Framework.DeterministicLocalResponse.established_response_has_total_joint_support (framework.bipartiteResponses model) localResponses established hiddenState, PhysicsLogic.Framework.DeterministicLocalResponse.established_response_has_no_signalling_support (framework.bipartiteResponses model) localResponses established hiddenState⟩ /- Source: original paper pp. 195-196, especially equation (1) and the paragraph immediately below it. One actual pair of magnet settings, a distinct alternative setting, and one value of the complete-state parameter lambda exercise Bell's local functions; the theorem does not identify fixed-lambda support screening with averaged probabilistic conditional independence. -/ theorem bell_local_responses_exhibit_nonvacuous_shared_factorization (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (localResponses : LocalResponses Setting HiddenState) (factorizes : framework.LocalResponsesFactorize model localResponses) (leftSetting rightSetting : Setting) (alternativeSetting : Setting) (distinctSettings : leftSetting ≠ alternativeSetting) (hiddenState : HiddenState) : (PhysicsLogic.Framework.DeterministicLocalResponse.deterministicLocalResponseCalculationModelAt (framework.bipartiteResponses model) localResponses) |>.NonvacuousDeterministicLocalResponseAt := PhysicsLogic.Framework.DeterministicLocalResponse.established_response_with_witnesses_exhibits_nonvacuous_local_factorization (framework.bipartiteResponses model) localResponses (framework.bell_local_responses_establish_deterministic_local_response model localResponses factorizes ⟨⟨hiddenState⟩, leftSetting, alternativeSetting, distinctSettings⟩) leftSetting rightSetting alternativeSetting distinctSettings hiddenState /-- A model's represented correlation has Bell's local form, equation (2). -/ def HasLocalCorrelationForm (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) : Prop := ∃ localResponses, framework.LocalResponsesFactorize model localResponses ∧ framework.correlationIsAverageOfResponses localResponses (framework.modelCorrelation model) /-- A model is local when its normalized hidden-state account has local form. -/ def IsLocalHiddenVariableModel (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) : Prop := framework.hiddenStateDistributionIsNormalized model ∧ framework.HasLocalCorrelationForm model /-- The outcome functions have only Bell's two values, `+1` and `-1`. -/ def ResponsesAreDichotomic (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) : Prop := ∀ leftSetting rightSetting hiddenState, ((framework.bipartiteResponses model).left leftSetting rightSetting hiddenState = .plus ∨ (framework.bipartiteResponses model).left leftSetting rightSetting hiddenState = .minus) ∧ ((framework.bipartiteResponses model).right leftSetting rightSetting hiddenState = .plus ∨ (framework.bipartiteResponses model).right leftSetting rightSetting hiddenState = .minus) /-- The response representation has exactly Bell's local functional form: each wing receives only its own setting and the shared hidden state. -/ def ResponsesUseOnlyLocalSettingAndHiddenState (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) : Prop := ∃ localResponses, framework.LocalResponsesFactorize model localResponses /-- Raw source premises for Bell's deterministic local-response explanation. The local equation-(1) response form and nonvacuous domain are retained together with the dichotomic, normalized hidden-variable account in which Bell introduces the complete-state parameter. This relation stores no shared established endpoint, averaged correlation, inequality, or experimental verdict. -/ def bellDeterministicLocalResponseDerivationObtains (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (localResponses : LocalResponses Setting HiddenState) : BellDeterministicLocalResponseDerivation -> Prop | .completeStateLocalResponseFunctions => framework.LocalResponsesFactorize model localResponses ∧ PhysicsLogic.Framework.DeterministicLocalResponse.NontrivialResponseDomain Setting HiddenState ∧ framework.ResponsesAreDichotomic model ∧ framework.hiddenStateDistributionIsNormalized model /-- The typed complete-state source reconstructs the raw shared factorization route instead of storing a completed shared response endpoint. -/ theorem bell_deterministic_local_response_source_derivation_makes_shared_route_applicable (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (localResponses : LocalResponses Setting HiddenState) (source : framework.bellDeterministicLocalResponseDerivationObtains model localResponses .completeStateLocalResponseFunctions) : PhysicsLogic.Framework.DeterministicLocalResponse.FactorizationRouteApplicable (framework.bipartiteResponses model) localResponses := framework.bell_local_responses_make_factorization_route_applicable model localResponses source.1 /-- Bell's complete-state derivation realizes the source-sensitive shared explanation without consuming an established response wrapper. -/ theorem bell_source_inputs_realize_source_structural_deterministic_local_response_explanation (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (localResponses : LocalResponses Setting HiddenState) (source : framework.bellDeterministicLocalResponseDerivationObtains model localResponses .completeStateLocalResponseFunctions) : PhysicsLogic.Framework.DeterministicLocalResponse.DirectSourceStructuralDeterministicLocalResponseExplanationAt (framework.bipartiteResponses model) localResponses .completeStateLocalResponseFunctions (framework.bellDeterministicLocalResponseDerivationObtains model localResponses) := PhysicsLogic.Framework.DeterministicLocalResponse.source_derivation_factorization_and_domain_realize_source_structural_deterministic_local_response_explanation (framework.bipartiteResponses model) localResponses .completeStateLocalResponseFunctions (framework.bellDeterministicLocalResponseDerivationObtains model localResponses) source source.2.1 (framework |>.bell_deterministic_local_response_source_derivation_makes_shared_route_applicable model localResponses source) /-- The response calculation grounded below is exactly the candidate's unrestricted responses together with Bell's proposed local equation-(1) functions. -/ theorem deterministic_local_response_model_retains_paper_semantics (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (localResponses : LocalResponses Setting HiddenState) : PhysicsLogic.Framework.DeterministicLocalResponse.SelectedDeterministicLocalResponseModelAt (framework.bipartiteResponses model) localResponses (PhysicsLogic.Framework.DeterministicLocalResponse.deterministicLocalResponseCalculationModelAt (framework.bipartiteResponses model) localResponses) := rfl theorem bell_inputs_realize_selected_deterministic_response_setup (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (localResponses : LocalResponses Setting HiddenState) (domain : PhysicsLogic.Framework.DeterministicLocalResponse.NontrivialResponseDomain Setting HiddenState) : PhysicsLogic.Framework.DeterministicLocalResponse.SelectedDeterministicLocalResponseSetupAt (framework.bipartiteResponses model) localResponses (PhysicsLogic.Framework.DeterministicLocalResponse.deterministicLocalResponseCalculationModelAt (framework.bipartiteResponses model) localResponses) := ⟨framework.deterministic_local_response_model_retains_paper_semantics model localResponses, domain⟩ /-- Bell's paper-local interpretation distinguishes a candidate deterministic completion from its response-function calculation and from the represented separated spin-pair experiment. Dichotomic outcomes and normalization belong to the containing hidden-variable account; experimental separation and operational locality belong to the world-representation bridge. Primary-source anchors: sections I-II for predetermined dichotomic results, the normalized hidden-variable distribution, separated measurements, and the local functional form used in equation (2). -/ def toDeterministicLocalResponseInterpretation (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (_localResponses : LocalResponses Setting HiddenState) (experimentSetup operationalLocality : Prop) : PhysicsLogic.Framework.DeterministicLocalResponse.DeterministicLocalResponseInterpretation BellLocalResponseTheory BellRemoteWorld Setting HiddenState Outcome where theoryUsesDeterministicLocalResponseModel := fun theory _calculation => theory = .candidateDeterministicCompletion ∧ framework.ResponsesAreDichotomic model ∧ framework.hiddenStateDistributionIsNormalized model deterministicLocalResponseModelRepresentsWorld := fun _calculation world => world = .separatedSpinPairExperiment ∧ experimentSetup ∧ operationalLocality theoryClaim := fun _ calculation claim => PhysicsLogic.Framework.DeterministicLocalResponse.DeterministicLocalResponseClaimHoldsAt calculation claim physicalClaim := fun _ calculation claim => PhysicsLogic.Framework.DeterministicLocalResponse.DeterministicLocalResponseClaimHoldsAt calculation claim theorem bell_local_response_model_inputs_establish_theory_model_grounding (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (localResponses : LocalResponses Setting HiddenState) {experimentSetup operationalLocality : Prop} (domain : PhysicsLogic.Framework.DeterministicLocalResponse.NontrivialResponseDomain Setting HiddenState) (dichotomic : framework.ResponsesAreDichotomic model) (normalized : framework.hiddenStateDistributionIsNormalized model) (experiment : experimentSetup) (locality : operationalLocality) : PhysicsLogic.Framework.DeterministicLocalResponse.TheoryModelGroundingAt (framework.toDeterministicLocalResponseInterpretation model localResponses experimentSetup operationalLocality) .candidateDeterministicCompletion .separatedSpinPairExperiment (framework.bipartiteResponses model) localResponses := by let interpretation := framework.toDeterministicLocalResponseInterpretation model localResponses experimentSetup operationalLocality let calculation := PhysicsLogic.Framework.DeterministicLocalResponse.deterministicLocalResponseCalculationModelAt (framework.bipartiteResponses model) localResponses have theoryUse : interpretation.theoryUsesDeterministicLocalResponseModel .candidateDeterministicCompletion calculation := ⟨rfl, dichotomic, normalized⟩ have represents : interpretation.deterministicLocalResponseModelRepresentsWorld calculation .separatedSpinPairExperiment := ⟨rfl, experiment, locality⟩ apply PhysicsLogic.Framework.DeterministicLocalResponse.theory_model_inputs_establish_grounding interpretation .candidateDeterministicCompletion .separatedSpinPairExperiment (framework.bipartiteResponses model) localResponses calculation · exact framework.bell_inputs_realize_selected_deterministic_response_setup model localResponses domain · exact theoryUse · exact represents · intro _claim modelClaim exact modelClaim · intro _claim modelClaim exact modelClaim theorem bell_local_response_route_establishes_theory_model_grounded_response (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (localResponses : LocalResponses Setting HiddenState) {experimentSetup operationalLocality : Prop} (factorizes : framework.LocalResponsesFactorize model localResponses) (domain : PhysicsLogic.Framework.DeterministicLocalResponse.NontrivialResponseDomain Setting HiddenState) (dichotomic : framework.ResponsesAreDichotomic model) (normalized : framework.hiddenStateDistributionIsNormalized model) (experiment : experimentSetup) (locality : operationalLocality) : PhysicsLogic.Framework.DeterministicLocalResponse.TheoryModelGroundedDeterministicLocalResponseAt (framework.toDeterministicLocalResponseInterpretation model localResponses experimentSetup operationalLocality) .candidateDeterministicCompletion .separatedSpinPairExperiment (framework.bipartiteResponses model) localResponses := by exact PhysicsLogic.Framework.DeterministicLocalResponse.established_response_and_grounding_establish_grounded_response (framework.toDeterministicLocalResponseInterpretation model localResponses experimentSetup operationalLocality) (framework.bell_local_responses_establish_deterministic_local_response model localResponses factorizes domain) (framework.bell_local_response_model_inputs_establish_theory_model_grounding model localResponses domain dichotomic normalized experiment locality) theorem grounded_bell_local_response_transfers_every_shared_claim (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (localResponses : LocalResponses Setting HiddenState) {experimentSetup operationalLocality : Prop} (grounded : PhysicsLogic.Framework.DeterministicLocalResponse.TheoryModelGroundedDeterministicLocalResponseAt (framework.toDeterministicLocalResponseInterpretation model localResponses experimentSetup operationalLocality) .candidateDeterministicCompletion .separatedSpinPairExperiment (framework.bipartiteResponses model) localResponses) : ∀ claim, (PhysicsLogic.Framework.DeterministicLocalResponse.toTheoryModelContext (framework.toDeterministicLocalResponseInterpretation model localResponses experimentSetup operationalLocality) (framework.bipartiteResponses model) localResponses |>.theoryEntails (PhysicsLogic.Framework.DeterministicLocalResponse.deterministicLocalResponseTheoryAt BellLocalResponseTheory.candidateDeterministicCompletion (PhysicsLogic.Framework.DeterministicLocalResponse.deterministicLocalResponseCalculationModelAt (framework.bipartiteResponses model) localResponses)) claim ()) ∧ (PhysicsLogic.Framework.DeterministicLocalResponse.toTheoryModelContext (framework.toDeterministicLocalResponseInterpretation model localResponses experimentSetup operationalLocality) (framework.bipartiteResponses model) localResponses |>.trueIn (PhysicsLogic.Framework.DeterministicLocalResponse.deterministicLocalResponseWorldAt BellRemoteWorld.separatedSpinPairExperiment (PhysicsLogic.Framework.DeterministicLocalResponse.deterministicLocalResponseCalculationModelAt (framework.bipartiteResponses model) localResponses)) claim ()) := PhysicsLogic.Framework.DeterministicLocalResponse.grounded_response_transfers_all_claims grounded /-- A remote setting has physical outcome-level influence when changing it while holding the local setting and hidden state fixed changes the opposite result. -/ def DistantSettingInfluencesRemoteOutcome (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) : Prop := (∃ leftSetting rightSetting₁ rightSetting₂ hiddenState, (framework.bipartiteResponses model).left leftSetting rightSetting₁ hiddenState ≠ (framework.bipartiteResponses model).left leftSetting rightSetting₂ hiddenState) ∨ (∃ leftSetting₁ leftSetting₂ rightSetting hiddenState, (framework.bipartiteResponses model).right leftSetting₁ rightSetting hiddenState ≠ (framework.bipartiteResponses model).right leftSetting₂ rightSetting hiddenState) /-- The normalized deterministic supplement reproduces the quantum correlation function. This necessary part of full statistics does not constrain marginals. -/ def DeterministicSupplementReproducesQuantumCorrelations (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) : Prop := framework.hiddenStateDistributionIsNormalized model ∧ framework.correlationIsAverageOfBipartiteResponses (framework.bipartiteResponses model) (framework.modelCorrelation model) ∧ framework.ReproducesQuantumCorrelation model /-- Correlation-function equality transfers any equal-setting anticorrelation predicate. -/ theorem agreement_transfers_perfect_anticorrelation (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (agreement : framework.ReproducesQuantumCorrelation model) (quantumPerfect : framework.QuantumPerfectAnticorrelation) : framework.correlationIsPerfectlyAnticorrelatedAtEqualSettings (framework.modelCorrelation model) := by have same : framework.modelCorrelation model = framework.quantumCorrelation := funext fun a => funext fun b => agreement a b rw [same] exact quantumPerfect /-- Bell's eq. (13): perfect anticorrelation forces opposite responses. -/ def PerfectAnticorrelationForcesOppositeResponses (framework : BellFramework Setting HiddenState Model Value Error) : Prop := ∀ model localResponses, framework.hiddenStateDistributionIsNormalized model → framework.LocalResponsesFactorize model localResponses → framework.correlationIsAverageOfResponses localResponses (framework.modelCorrelation model) → framework.correlationIsPerfectlyAnticorrelatedAtEqualSettings (framework.modelCorrelation model) → framework.responsesAreOppositeAlmostEverywhere localResponses /-- Bell's eq. (14): opposite responses rewrite the local correlation. -/ def OppositeResponsesGiveSingleResponseForm (framework : BellFramework Setting HiddenState Model Value Error) : Prop := ∀ model localResponses, framework.correlationIsAverageOfResponses localResponses (framework.modelCorrelation model) → framework.responsesAreOppositeAlmostEverywhere localResponses → framework.correlationHasSingleResponseForm localResponses (framework.modelCorrelation model) /-- Equation (13) holds for one local representation of the model. -/ def HasOppositeLocalResponses (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) : Prop := ∃ localResponses, framework.LocalResponsesFactorize model localResponses ∧ framework.correlationIsAverageOfResponses localResponses (framework.modelCorrelation model) ∧ framework.responsesAreOppositeAlmostEverywhere localResponses /-- Equation (14) holds for one local representation of the model. -/ def HasSingleResponseCorrelationForm (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) : Prop := ∃ localResponses, framework.LocalResponsesFactorize model localResponses ∧ framework.correlationHasSingleResponseForm localResponses (framework.modelCorrelation model) /-- The algebraic integration of eq. (14) gives Bell's eq. (15). -/ def SingleResponseFormSatisfiesBellInequality (framework : BellFramework Setting HiddenState Model Value Error) : Prop := ∀ responses correlation, framework.correlationHasSingleResponseForm responses correlation → SatisfiesBell1964Inequality framework.order correlation /-- Equation (14) is represented by an actual hidden-state average. Its laws are restricted to the response expressions in equation (15), so a probability integral need not be linear on nonintegrable functions. -/ def SingleResponseFormHasAverageRepresentation (framework : BellFramework Setting HiddenState Model Value Error) : Prop := ∀ responses correlation, framework.correlationHasSingleResponseForm responses correlation → ∃ average : HiddenAverage HiddenState Value, BellResponseAverageLaws framework.order average responses ∧ IsSingleResponseAverage framework.order average responses correlation /-- Exact local hidden-variable reproduction of the quantum correlation. -/ def HasExactLocalRepresentation (framework : BellFramework Setting HiddenState Model Value Error) : Prop := ∃ model, framework.IsLocalHiddenVariableModel model ∧ framework.ReproducesQuantumCorrelation model /-- The technical local-model result derived in Bell's section IV. -/ def EveryLocalModelSatisfiesBellInequality (framework : BellFramework Setting HiddenState Model Value Error) : Prop := ∀ model, framework.IsLocalHiddenVariableModel model → SatisfiesBell1964Inequality framework.order (framework.modelCorrelation model) /-- Local models approximate the quantum correlation arbitrarily accurately. -/ def HasArbitrarilyAccurateLocalApproximation (framework : BellFramework Setting HiddenState Model Value Error) : Prop := ∀ error, framework.positiveError error → ∃ model, framework.IsLocalHiddenVariableModel model ∧ framework.uniformlyApproximates (framework.modelCorrelation model) framework.quantumCorrelation error /-- Bell's averaged-setting result supplies a positive uniform error gap. -/ def HasBellApproximationGap (framework : BellFramework Setting HiddenState Model Value Error) : Prop := ∃ gap, framework.positiveError gap ∧ ∀ model, framework.IsLocalHiddenVariableModel model → ¬framework.uniformlyApproximates (framework.modelCorrelation model) framework.quantumCorrelation gap /-- The two angular averages introduced before equation (16), using one selected finite window for both the local and quantum correlations. -/ def AveragedCorrelationConstructionAt (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (analysis : AveragedSettingAnalysis Setting Value Error) : Prop := framework.positiveError analysis.angularWindow ∧ framework.angularAverageAt (framework.modelCorrelation model) analysis.averagedModelCorrelation analysis.angularWindow ∧ framework.angularAverageAt framework.quantumCorrelation analysis.averagedQuantumCorrelation analysis.angularWindow /-- The concrete local approximation selected under the reductio supposition. This keeps the chosen model, positive epsilon, and uniform approximation together instead of treating "some approximation exists" as an inert label. -/ def SelectedUniformLocalApproximationAt (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (analysis : AveragedSettingAnalysis Setting Value Error) : Prop := framework.IsLocalHiddenVariableModel model ∧ framework.positiveError analysis.approximationError ∧ framework.uniformlyApproximates (framework.modelCorrelation model) framework.quantumCorrelation analysis.approximationError /-- The logical payload of equations (18)-(21): the original uniform error is transferred to the two angular averages, the averaged local responses remain bounded by one, equal-setting near-anticorrelation is controlled by epsilon and the angular window, and the three-setting estimate is obtained. -/ def AveragedApproximationEstimateAt (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (analysis : AveragedSettingAnalysis Setting Value Error) : Prop := framework.averagedUniformErrorBoundAt analysis.averagedModelCorrelation analysis.averagedQuantumCorrelation analysis.approximationError ∧ framework.averagedLocalResponseBoundsAt model analysis.averagedModelCorrelation analysis.angularWindow ∧ framework.equalSettingAveragedAnticorrelationEstimateAt model analysis.averagedModelCorrelation analysis.angularWindow analysis.approximationError ∧ framework.threeSettingAveragedDifferenceEstimateAt model analysis.averagedModelCorrelation analysis.angularWindow analysis.approximationError /-- Bell's original equation (22), after his three directions are inserted. -/ def PaperDirectionApproximationLowerBound (angularWindow approximationError : Real) : Prop := Real.sqrt 2 - 1 ≤ 4 * (approximationError + angularWindow) /-- A chosen positive window/error pair lies strictly below Bell's bound. -/ def PaperDirectionStrictlyBelowApproximationLowerBound (angularWindow approximationError : Real) : Prop := 4 * (approximationError + angularWindow) < Real.sqrt 2 - 1 /-- Bell's chosen positive error and window violate equation (22), while every local model approximating the singlet at that error would have to satisfy it. -/ def SelectedApproximationGapAt (framework : BellFramework Setting HiddenState Model Value Error) (analysis : AveragedSettingAnalysis Setting Value Error) : Prop := framework.positiveError analysis.angularWindow ∧ framework.positiveError analysis.approximationError ∧ PaperDirectionStrictlyBelowApproximationLowerBound (framework.errorMagnitude analysis.angularWindow) (framework.errorMagnitude analysis.approximationError) ∧ ∀ model, framework.IsLocalHiddenVariableModel model → framework.uniformlyApproximates (framework.modelCorrelation model) framework.quantumCorrelation analysis.approximationError → PaperDirectionApproximationLowerBound (framework.errorMagnitude analysis.angularWindow) (framework.errorMagnitude analysis.approximationError) /-- The selected no-go result retains both positive scales and Bell's bound. -/ theorem selected_approximation_gap_exposes_printed_threshold (framework : BellFramework Setting HiddenState Model Value Error) (analysis : AveragedSettingAnalysis Setting Value Error) (gap : framework.SelectedApproximationGapAt analysis) : 0 < framework.errorMagnitude analysis.angularWindow ∧ 0 < framework.errorMagnitude analysis.approximationError ∧ 4 * (framework.errorMagnitude analysis.approximationError + framework.errorMagnitude analysis.angularWindow) < Real.sqrt 2 - 1 := ⟨gap.1, gap.2.1, gap.2.2.1⟩ /-- A selected equation-(22) gap supplies the existential gap used below. -/ theorem selected_approximation_gap_supplies_bell_gap (framework : BellFramework Setting HiddenState Model Value Error) (analysis : AveragedSettingAnalysis Setting Value Error) (gap : framework.SelectedApproximationGapAt analysis) : framework.HasBellApproximationGap := by refine ⟨analysis.approximationError, gap.2.1, ?_⟩ intro model localModel approximation exact (not_le_of_gt gap.2.2.1) (gap.2.2.2 model localModel approximation) /-- Angular averaging is introduced from the local and quantum correlations, with the common positive window retained in the resulting proposition. -/ def AveragedCorrelationConstructionPrinciple (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (analysis : AveragedSettingAnalysis Setting Value Error) : Prop := framework.HasLocalCorrelationForm model → framework.QuantumSingletCorrelationFormula → framework.AveragedCorrelationConstructionAt model analysis /-- Equations (18)-(21) are the deferred averaged-setting calculation. -/ def AveragedApproximationEstimateCalculation (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (analysis : AveragedSettingAnalysis Setting Value Error) : Prop := framework.ResponsesAreDichotomic model → framework.hiddenStateDistributionIsNormalized model → framework.AveragedCorrelationConstructionAt model analysis → framework.SelectedUniformLocalApproximationAt model analysis → framework.AveragedApproximationEstimateAt model analysis /-- Equation (22) turns the structured averaged estimate into a selected gap. -/ def ApproximationGapCalculation (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (analysis : AveragedSettingAnalysis Setting Value Error) : Prop := framework.QuantumSingletCorrelationFormula → framework.AveragedApproximationEstimateAt model analysis → framework.SelectedApproximationGapAt analysis /-- Bell's predetermined responses require an actual complete-state value and genuinely alternative magnet settings, not functions on an empty domain. -/ def PredeterminedLocalResponses (Setting : Type u) (HiddenState : Type v) : Prop := PhysicsLogic.Framework.DeterministicLocalResponse.NontrivialResponseDomain Setting HiddenState ∧ Nonempty (LocalResponses Setting HiddenState) /-- The EPR inference is represented independently of the later inequality. -/ def EPRPredeterminationPrinciple (Setting : Type u) (HiddenState : Type v) (perfectPredictability operationalLocality : Prop) : Prop := perfectPredictability → operationalLocality → PredeterminedLocalResponses Setting HiddenState /-- Predetermined responses plus the wavefunction's failure to determine individual results require a more complete state specification. -/ def PredeterminationRequiresMoreCompleteState (Setting : Type u) (HiddenState : Type v) (wavefunctionDeterminesIndividualOutcomes moreCompleteStateSpecificationExists : Prop) : Prop := PredeterminedLocalResponses Setting HiddenState → ¬wavefunctionDeterminesIndividualOutcomes → moreCompleteStateSpecificationExists /-- Perfect singlet anticorrelation licenses prediction of the remote result only when the matching measurement procedure is operationally available. -/ def PerfectAnticorrelationGivesPredictability (framework : BellFramework Setting HiddenState Model Value Error) (reality : RealityCriterionContext Setting (MatchingSpinMeasurement Setting) BellCorrelationStage) (procedureAvailable : MatchingSpinMeasurement Setting → Prop) : Prop := framework.QuantumPerfectAnticorrelation → MatchingSpinMeasurementsAvailable procedureAvailable → EveryChosenRemoteSpinResultPredictable reality /-- The functions used by the candidate completion realize the outcomes inferred to be predetermined by the EPR argument. Bell's locality premise then makes those realized responses depend only on the local setting and shared hidden state. -/ def EPRPredeterminedResponsesRealizeLocalModel (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (operationalLocality : Prop) : Prop := PredeterminedLocalResponses Setting HiddenState → operationalLocality → framework.ResponsesAreDichotomic model → framework.ResponsesUseOnlyLocalSettingAndHiddenState model /-- Bell's operational locality premise supplies the no-disturbance half of the EPR criterion for every matching remote-spin procedure. -/ def OperationalLocalityGivesRemoteNonDisturbance (reality : RealityCriterionContext Setting (MatchingSpinMeasurement Setting) BellCorrelationStage) (operationalLocality : Prop) : Prop := operationalLocality → EveryChosenRemoteSpinResultUndisturbed reality /-- The narrow shared remote-correlation interface used by both EPR 1935 and Bell's section-II spin argument. Completeness is intentionally inert here: Bell uses the established remote predictions for predetermination rather than the two-quantity completeness reductio of the original EPR paper. -/ def toRemoteCorrelationPredictionContext (framework : BellFramework Setting HiddenState Model Value Error) (reality : RealityCriterionContext Setting (MatchingSpinMeasurement Setting) BellCorrelationStage) (procedureAvailable : MatchingSpinMeasurement Setting → Prop) (experimentSetup operationalLocality : Prop) : RemoteCorrelationPredictionContext BellSingletExperiment BellParticle Setting (MatchingSpinMeasurement Setting) BellCorrelationStage where observation := RemotePredictionObservationContext.ofRealityCriterion reality selectedExperiment := selectedBellSingletExperiment selectedLocalSubsystem := .first selectedRemoteSubsystem := .second selectedRegime := selectedBellCorrelationStage selectedQuantity := fun _ => True procedureFor := fun component => ⟨component⟩ experimentPreparedAt := fun experiment stage => experiment = selectedBellSingletExperiment ∧ stage = selectedBellCorrelationStage ∧ experimentSetup separatedAfterPreparationAt := fun experiment localSubsystem remoteSubsystem stage => experiment = selectedBellSingletExperiment ∧ localSubsystem = .first ∧ remoteSubsystem = .second ∧ stage = selectedBellCorrelationStage ∧ operationalLocality procedureAvailableAt := fun procedure localSubsystem experiment stage => experiment = selectedBellSingletExperiment ∧ localSubsystem = .first ∧ stage = selectedBellCorrelationStage ∧ procedureAvailable procedure remoteCorrelationCalculatedAt := fun procedure localSubsystem component remoteSubsystem experiment stage => experiment = selectedBellSingletExperiment ∧ localSubsystem = .first ∧ remoteSubsystem = .second ∧ procedure = ⟨component⟩ ∧ stage = selectedBellCorrelationStage ∧ framework.QuantumPerfectAnticorrelation /-- Bell's exact proof-free shared model for the selected singlet route. -/ def remoteCorrelationModel (framework : BellFramework Setting HiddenState Model Value Error) (reality : RealityCriterionContext Setting (MatchingSpinMeasurement Setting) BellCorrelationStage) (procedureAvailable : MatchingSpinMeasurement Setting → Prop) (experimentSetup operationalLocality : Prop) : RemoteCorrelationCalculationModel BellSingletExperiment BellParticle Setting (MatchingSpinMeasurement Setting) BellCorrelationStage := framework.toRemoteCorrelationPredictionContext reality procedureAvailable experimentSetup operationalLocality |>.selectedModel /-- The named Bell model retains the full paper-local semantics of matching measurements, perfect anticorrelation, preparation, and operational locality. -/ theorem remote_correlation_model_retains_paper_semantics (framework : BellFramework Setting HiddenState Model Value Error) (reality : RealityCriterionContext Setting (MatchingSpinMeasurement Setting) BellCorrelationStage) (procedureAvailable : MatchingSpinMeasurement Setting → Prop) (experimentSetup operationalLocality : Prop) : framework.toRemoteCorrelationPredictionContext reality procedureAvailable experimentSetup operationalLocality |>.SelectedRemoteCorrelationSemanticsAt (framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality) := rfl /-- Bell's singlet prediction model discards EPR's optional admissibility assignment before any source-specific predetermination inference. -/ theorem bell_remote_correlation_model_ignores_physical_admissibility (framework : BellFramework Setting HiddenState Model Value Error) (reality : RealityCriterionContext Setting (MatchingSpinMeasurement Setting) BellCorrelationStage) (admissibility : Setting -> BellCorrelationStage -> Prop) (procedureAvailable : MatchingSpinMeasurement Setting -> Prop) (experimentSetup operationalLocality : Prop) : framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality = framework.remoteCorrelationModel { reality with physicallyAdmissible := admissibility } procedureAvailable experimentSetup operationalLocality := rfl /-! Sections I-II, pp. 195-196: the source relation retains singlet preparation, operational separation, matching-spin availability, quantum perfect anticorrelation, its prediction bridge, and locality-based non-disturbance. It contains neither predetermined responses nor Bell's inequality. -/ def bellRemoteCorrelationDerivationObtains (framework : BellFramework Setting HiddenState Model Value Error) (reality : RealityCriterionContext Setting (MatchingSpinMeasurement Setting) BellCorrelationStage) (procedureAvailable : MatchingSpinMeasurement Setting -> Prop) (experimentSetup operationalLocality : Prop) : BellRemoteCorrelationDerivation -> Prop | .singletAnticorrelationMatchingMeasurementAndOperationalLocality => experimentSetup ∧ operationalLocality ∧ MatchingSpinMeasurementsAvailable procedureAvailable ∧ framework.QuantumPerfectAnticorrelation ∧ framework.PerfectAnticorrelationGivesPredictability reality procedureAvailable ∧ OperationalLocalityGivesRemoteNonDisturbance reality operationalLocality /-- One explicitly chosen spin component inhabits Bell's exact prepared and separated setup before perfect anticorrelation or either prediction bridge is used. -/ theorem bell_inputs_realize_selected_remote_correlation_setup (framework : BellFramework Setting HiddenState Model Value Error) (reality : RealityCriterionContext Setting (MatchingSpinMeasurement Setting) BellCorrelationStage) (procedureAvailable : MatchingSpinMeasurement Setting → Prop) (component : Setting) {experimentSetup operationalLocality : Prop} (experiment : experimentSetup) (locality : operationalLocality) (matchingMeasurements : MatchingSpinMeasurementsAvailable procedureAvailable) : framework.toRemoteCorrelationPredictionContext reality procedureAvailable experimentSetup operationalLocality |>.SelectedRemoteCorrelationSetupAt (framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality) := by let context := framework.toRemoteCorrelationPredictionContext reality procedureAvailable experimentSetup operationalLocality have setup : context.SetupAt (framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality) := ⟨⟨rfl, rfl, experiment⟩, by change BellParticle.first ≠ BellParticle.second decide, ⟨rfl, rfl, rfl, rfl, locality⟩, fun _ _ => ⟨rfl, rfl, rfl, matchingMeasurements _⟩⟩ exact ⟨framework.remote_correlation_model_retains_paper_semantics reality procedureAvailable experimentSetup operationalLocality, setup, ⟨component, trivial⟩⟩ /-- The shared calculation model retains Bell's selected two spin-one-half particles, their total-spin-zero preparation, and the separated-measurement stage as physical indices rather than collapsing them to anonymous values. Primary-source anchor: section II, pp. 195-196. -/ theorem remote_correlation_model_retains_singlet_experiment_and_stage_data (framework : BellFramework Setting HiddenState Model Value Error) (reality : RealityCriterionContext Setting (MatchingSpinMeasurement Setting) BellCorrelationStage) (procedureAvailable : MatchingSpinMeasurement Setting → Prop) (experimentSetup operationalLocality : Prop) : let model := framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality model.experiment.particleCount = 2 ∧ model.experiment.constituentTwiceSpin = 1 ∧ model.experiment.totalTwiceSpin = 0 ∧ model.localSubsystem = .first ∧ model.remoteSubsystem = .second ∧ model.regime = .separatedMeasurement := by exact ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩ /-- Bell's singlet correlation model is distinct from the quantum description using it and from the represented separated-spin experiment. Operational locality enters the world-representation bridge rather than being hidden in the perfect-anticorrelation calculation. Primary-source anchors: sections I-II for the singlet preparation, perfect anticorrelation, matching measurements, and locality-based non-disturbance. -/ def toRemoteCorrelationPredictionInterpretation (framework : BellFramework Setting HiddenState Model Value Error) (reality : RealityCriterionContext Setting (MatchingSpinMeasurement Setting) BellCorrelationStage) (procedureAvailable : MatchingSpinMeasurement Setting → Prop) (experimentSetup operationalLocality : Prop) : RemoteCorrelationPredictionInterpretation BellRemoteTheory BellRemoteWorld BellSingletExperiment BellParticle Setting (MatchingSpinMeasurement Setting) BellCorrelationStage where theoryUsesRemoteCorrelationModel := fun theory model => theory = .singletQuantumDescription ∧ model = framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality ∧ experimentSetup remoteCorrelationModelRepresentsWorld := fun model world => model = framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality ∧ world = .separatedSpinPairExperiment ∧ experimentSetup ∧ operationalLocality theoryClaim := fun theory model claim => theory = .singletQuantumDescription ∧ model = framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality ∧ (framework.toRemoteCorrelationPredictionContext reality procedureAvailable experimentSetup operationalLocality |>.ClaimHoldsAt model claim) physicalClaim := fun world model claim => world = .separatedSpinPairExperiment ∧ model = framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality ∧ (framework.toRemoteCorrelationPredictionContext reality procedureAvailable experimentSetup operationalLocality |>.ClaimHoldsAt model claim) /-- Equation (2) is formed from the local responses and normalized distribution. -/ def LocalCorrelationDefinitionPrinciple (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) : Prop := framework.ResponsesAreDichotomic model → framework.ResponsesUseOnlyLocalSettingAndHiddenState model → framework.hiddenStateDistributionIsNormalized model → framework.HasLocalCorrelationForm model /-- Before locality is imposed, deterministic bipartite responses and the normalized hidden-state distribution define the model correlation. -/ def BipartiteCorrelationDefinitionPrinciple (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) : Prop := framework.ResponsesAreDichotomic model → framework.hiddenStateDistributionIsNormalized model → framework.correlationIsAverageOfBipartiteResponses (framework.bipartiteResponses model) (framework.modelCorrelation model) /-- The correlation requirement retained from the source's broader demand to preserve statistical predictions. It does not assert the full joint law. -/ def CompletionRetainsQuantumCorrelationsPrinciple (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (moreCompleteStateSpecificationExists : Prop) : Prop := moreCompleteStateSpecificationExists → framework.ReproducesQuantumCorrelation model /-- Bell's section III single-particle hidden-variable illustration exists. -/ def HasSingleParticleHiddenVariableAccount (framework : BellFramework Setting HiddenState Model Value Error) : Prop := ∃ model, framework.singleParticleHiddenVariableAccount model ∧ SingleSpinIllustrationData.SingleParticleConstructionComplete (framework.singleParticleIllustration model) /-- A local model exists for Bell's restricted bipartite correlations. -/ def HasRestrictedBipartiteLocalAccount (framework : BellFramework Setting HiddenState Model Value Error) : Prop := ∃ model, framework.restrictedBipartiteLocalAccount model ∧ framework.IsLocalHiddenVariableModel model /-- The full singlet correlation can be represented if nonlocal dependence is allowed. -/ def HasNonlocalSingletCorrelationAccount (framework : BellFramework Setting HiddenState Model Value Error) : Prop := ∃ model, framework.DeterministicSupplementReproducesQuantumCorrelations model ∧ framework.DistantSettingInfluencesRemoteOutcome model /-- The source-level section-III clauses exhibit a complete single-spin account. -/ theorem single_spin_construction_exhibits_hidden_variable_account (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (account : framework.singleParticleHiddenVariableAccount model) (geometry : SingleSpinIllustrationData.HasPolarizedPureSpinGeometry (framework.singleParticleIllustration model)) (hemisphereLaw : SingleSpinIllustrationData.HasUniformPolarizedHemisphereLaw (framework.singleParticleIllustration model)) (signRule : SingleSpinIllustrationData.ResponseUsesRotatedSignAwayFromBoundary (framework.singleParticleIllustration model)) (boundary : SingleSpinIllustrationData.BoundaryHasZeroAverageWeight (framework.singleParticleIllustration model)) (averagePrinciple : SingleSpinIllustrationData.UniformHemisphereSignAveragePrinciple (framework.singleParticleIllustration model)) (calibration : SingleSpinIllustrationData.HasRotationCalibration (framework.singleParticleIllustration model)) : framework.HasSingleParticleHiddenVariableAccount := by let data := framework.singleParticleIllustration model have averageLaw : SingleSpinIllustrationData.HasHemisphereSignAverage data := averagePrinciple hemisphereLaw signRule boundary have expectation : SingleSpinIllustrationData.ReproducesPureSpinExpectation data := single_spin_hemisphere_rotation_reproduces_quantum_expectation data hemisphereLaw signRule boundary averagePrinciple calibration exact ⟨model, account, geometry, hemisphereLaw, signRule, boundary, averageLaw, calibration, expectation⟩ /-- Bell's restricted bipartite construction from the local correlation form. -/ def RestrictedCorrelationIllustrationCalculation (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) : Prop := framework.HasLocalCorrelationForm model → framework.HasRestrictedBipartiteLocalAccount /-- Distant-setting dependence recovers the full singlet correlation. -/ def NonlocalCorrelationIllustrationCalculation (framework : BellFramework Setting HiddenState Model Value Error) : Prop := framework.QuantumSingletCorrelationFormula → framework.HasNonlocalSingletCorrelationAccount /-- The three examples delimiting the theorem are represented separately. -/ def ScopeIllustrations (framework : BellFramework Setting HiddenState Model Value Error) : Prop := framework.HasSingleParticleHiddenVariableAccount ∧ framework.HasRestrictedBipartiteLocalAccount ∧ framework.HasNonlocalSingletCorrelationAccount /-- Hidden-variable accounts as such remain possible in the paper's examples. -/ def HiddenVariableAccountsRemainPossible (Model : Type w) : Prop := Nonempty Model /-- Bell's fixed-hidden-state locality on p. 196 is exactly local response factorization. The equal-setting restrictions construct the local functions; no physical bridge principle or reference-setting choice is required. This is not no-signalling after averaging over the hidden-state distribution. -/ theorem no_distant_setting_influence_iff_local_response_dependence (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) : ¬framework.DistantSettingInfluencesRemoteOutcome model ↔ framework.ResponsesUseOnlyLocalSettingAndHiddenState model := by classical change ¬framework.DistantSettingInfluencesRemoteOutcome model ↔ PhysicsLogic.Framework.DeterministicLocalResponse.AdmitsLocalFactorization (framework.bipartiteResponses model) rw [PhysicsLogic.Framework.DeterministicLocalResponse.admits_local_factorization_iff_remote_setting_independence] unfold DistantSettingInfluencesRemoteOutcome push_neg constructor · rintro ⟨left, right⟩ hidden exact ⟨fun a b c => left a b c hidden, fun a b c => right a b c hidden⟩ · intro independent exact ⟨fun a b c hidden => (independent hidden).1 a b c, fun a b c hidden => (independent hidden).2 a b c⟩ /-- Factoring a bipartite hidden-variable average through local response functions converts it into Bell's equation (2). -/ def FactorizedBipartiteAverageGivesLocalCorrelation (framework : BellFramework Setting HiddenState Model Value Error) : Prop := ∀ model, framework.ResponsesUseOnlyLocalSettingAndHiddenState model → framework.correlationIsAverageOfBipartiteResponses (framework.bipartiteResponses model) (framework.modelCorrelation model) → framework.HasLocalCorrelationForm model /-- The influence connects simultaneous but spatially distinct events. -/ def InfluenceIsInstantaneous (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) : Prop := (framework.influenceSeparation model).temporal = 0 ∧ (framework.influenceSeparation model).spatial ≠ 0 /-- The temporal displacement after a boost of velocity `velocity`, with the positive Lorentz factor omitted because it does not change temporal order. -/ def BoostedInfluenceTemporalSeparation (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (velocity : Real) : Real := (framework.influenceSeparation model).temporal - velocity * (framework.influenceSeparation model).spatial /-- A subluminal boost in units where the speed of light is one. -/ def IsAdmissibleBoost (velocity : Real) : Prop := |velocity| < 1 /-- The directed influence has the same causal order in every inertial frame. -/ def CausalDirectionPreservedInEveryInertialFrame (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) : Prop := ∀ velocity, IsAdmissibleBoost velocity → 0 ≤ framework.BoostedInfluenceTemporalSeparation model velocity /-- For measurements arranged at spacelike separation, the distant-setting influence required by the completion is instantaneous in some frame. -/ def SeparatedInfluenceIsInstantaneous (framework : BellFramework Setting HiddenState Model Value Error) (measurementsAreSpacelikeSeparated : Prop) : Prop := ∀ model, measurementsAreSpacelikeSeparated → framework.DistantSettingInfluencesRemoteOutcome model → framework.InfluenceIsInstantaneous model /-- A Lorentz-invariant directed causal mechanism must preserve the direction of the required remote influence in every inertial frame. -/ def LorentzInvariantInfluencePreservesCausalDirection (framework : BellFramework Setting HiddenState Model Value Error) : Prop := ∀ model, framework.lorentzInvariant model → framework.DistantSettingInfluencesRemoteOutcome model → framework.CausalDirectionPreservedInEveryInertialFrame model /-- Bell's limited-validity alternative for rapidly changed settings. -/ def LimitedValidityEscape (quantumPredictionsRemainValidDuringParticleFlight : Prop) : Prop := ¬quantumPredictionsRemainValidDuringParticleFlight /-- Bell calls limited validity conceivable rather than asserting that quantum predictions actually fail during flight. The paper-local claim therefore uses the shared epistemic layer to keep possibility and establishment apart. -/ def LimitedValidityAlternativeIsTentative {Regime : Type z} (possibility : PossibilityStatusContext Prop Regime) (establishment : EstablishmentStatusContext Prop Regime) (regime : Regime) (quantumPredictionsRemainValidDuringParticleFlight : Prop) : Prop := possibility.TentativeAt establishment (LimitedValidityEscape quantumPredictionsRemainValidDuringParticleFlight) regime /-- The proposed fast-setting experiment tests the limited-validity escape. -/ def FastSettingExperimentTestsLimitedValidity (fastSettingExperimentSupportsQuantumPredictions quantumPredictionsRemainValidDuringParticleFlight : Prop) : Prop := fastSettingExperimentSupportsQuantumPredictions → quantumPredictionsRemainValidDuringParticleFlight /-- The tentative limited-validity alternative motivates the in-flight setting-change test; it is not inferred from Lorentz failure. -/ def TentativeLimitedValidityMotivatesFastSettingExperiment {Regime : Type z} (possibility : PossibilityStatusContext Prop Regime) (establishment : EstablishmentStatusContext Prop Regime) (regime : Regime) (fastSettingExperimentSupportsQuantumPredictions quantumPredictionsRemainValidDuringParticleFlight : Prop) : Prop := LimitedValidityAlternativeIsTentative possibility establishment regime quantumPredictionsRemainValidDuringParticleFlight → FastSettingExperimentTestsLimitedValidity fastSettingExperimentSupportsQuantumPredictions quantumPredictionsRemainValidDuringParticleFlight theorem tentative_limited_validity_retains_possibility_and_nonestablishment {Regime : Type z} (possibility : PossibilityStatusContext Prop Regime) (establishment : EstablishmentStatusContext Prop Regime) (regime : Regime) (quantumPredictionsRemainValidDuringParticleFlight : Prop) (tentative : LimitedValidityAlternativeIsTentative possibility establishment regime quantumPredictionsRemainValidDuringParticleFlight) : possibility.consideredPossibleAt (LimitedValidityEscape quantumPredictionsRemainValidDuringParticleFlight) regime ∧ ¬establishment.establishedAt (LimitedValidityEscape quantumPredictionsRemainValidDuringParticleFlight) regime := tentative_status_retains_possibility_and_nonestablishment possibility establishment (LimitedValidityEscape quantumPredictionsRemainValidDuringParticleFlight) regime tentative /-- Semantic data for Bell's section V higher-dimensional extension. -/ structure HigherDimensionalScenario (State : Type u) (Observable : Type v) where completeHermitianOperator : Observable → Prop physicallyObservable : Observable → Prop containsBellTwoDimensionalSubscenario : State → Prop separablePredeterminationCompatible : State → Prop namespace HigherDimensionalScenario variable {State : Type u} {Observable : Type v} /-- Bell's explicit assumption that complete Hermitian operators are observable. -/ def CompleteHermitianOperatorsAreObservable (scenario : HigherDimensionalScenario State Observable) : Prop := ∀ observable, scenario.completeHermitianOperator observable → scenario.physicallyObservable observable /-- At least one state contains the two-dimensional Bell construction. -/ def HasBellSubscenario (scenario : HigherDimensionalScenario State Observable) : Prop := ∃ state, scenario.containsBellTwoDimensionalSubscenario state /-- Bell's observability assumption exposes an admissible two-state sector. -/ def ObservabilitySupportsBellSubscenario (scenario : HigherDimensionalScenario State Observable) : Prop := scenario.CompleteHermitianOperatorsAreObservable → scenario.HasBellSubscenario /-- The four-dimensional no-go transports through the Bell subscenario. -/ def BellSubscenarioTransportsNoGo (scenario : HigherDimensionalScenario State Observable) (bellNoGo : Prop) : Prop := bellNoGo → scenario.HasBellSubscenario → ¬∀ state, scenario.separablePredeterminationCompatible state /-- The two-dimensional reduction obstructs separable predetermination. -/ def BellSubscenarioObstructsSeparablePredetermination (scenario : HigherDimensionalScenario State Observable) : Prop := scenario.CompleteHermitianOperatorsAreObservable → ∀ state, scenario.containsBellTwoDimensionalSubscenario state → ¬scenario.separablePredeterminationCompatible state end HigherDimensionalScenario theorem model_responses_are_dichotomic (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) : framework.ResponsesAreDichotomic model := by intro leftSetting rightSetting hiddenState constructor · cases (framework.bipartiteResponses model).left leftSetting rightSetting hiddenState with | plus => exact Or.inl rfl | minus => exact Or.inr rfl · cases (framework.bipartiteResponses model).right leftSetting rightSetting hiddenState with | plus => exact Or.inl rfl | minus => exact Or.inr rfl /-- Removing the binary-range conjunct loses no condition: the response codomain already supplies it. The older source clauses remain explicitly recoverable. -/ theorem deterministic_correlation_supplement_iff_source_conditions (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) : framework.DeterministicSupplementReproducesQuantumCorrelations model ↔ framework.ResponsesAreDichotomic model ∧ framework.hiddenStateDistributionIsNormalized model ∧ framework.correlationIsAverageOfBipartiteResponses (framework.bipartiteResponses model) (framework.modelCorrelation model) ∧ framework.ReproducesQuantumCorrelation model := by constructor · intro supplement exact ⟨framework.model_responses_are_dichotomic model, supplement⟩ · rintro ⟨_binary, normalized, average, agreement⟩ exact ⟨normalized, average, agreement⟩ theorem local_factorization_excludes_distant_setting_influence (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) : framework.ResponsesUseOnlyLocalSettingAndHiddenState model → ¬framework.DistantSettingInfluencesRemoteOutcome model := (framework.no_distant_setting_influence_iff_local_response_dependence model).mpr theorem epr_predetermination {perfectPredictability operationalLocality : Prop} (principle : EPRPredeterminationPrinciple Setting HiddenState perfectPredictability operationalLocality) (predictable : perfectPredictability) (locality : operationalLocality) : PredeterminedLocalResponses Setting HiddenState := principle predictable locality /-- Section II discusses an actual complete state and alternative choices of spin component; its predetermination inference cannot be empty-domain logic. -/ theorem epr_predetermination_exposes_inhabited_state_and_distinct_settings {perfectPredictability operationalLocality : Prop} (principle : EPRPredeterminationPrinciple Setting HiddenState perfectPredictability operationalLocality) (predictable : perfectPredictability) (locality : operationalLocality) : Nonempty HiddenState ∧ ∃ firstSetting alternativeSetting : Setting, firstSetting ≠ alternativeSetting := (epr_predetermination principle predictable locality).1 theorem matching_measurements_available_in_experiment {experimentSetup : Prop} (procedureAvailable : MatchingSpinMeasurement Setting → Prop) (arrangement : ExperimentProvidesMatchingSpinMeasurements experimentSetup procedureAvailable) (experiment : experimentSetup) : MatchingSpinMeasurementsAvailable procedureAvailable := arrangement experiment /-- Bell's operational prediction step consumes both singlet anticorrelation and availability of the matching measurement procedure. -/ theorem matching_measurement_and_anticorrelation_give_predictability (framework : BellFramework Setting HiddenState Model Value Error) (reality : RealityCriterionContext Setting (MatchingSpinMeasurement Setting) BellCorrelationStage) (procedureAvailable : MatchingSpinMeasurement Setting → Prop) (principle : framework.PerfectAnticorrelationGivesPredictability reality procedureAvailable) (quantumPerfect : framework.QuantumPerfectAnticorrelation) (matchingMeasurements : MatchingSpinMeasurementsAvailable procedureAvailable) : EveryChosenRemoteSpinResultPredictable reality := principle quantumPerfect matchingMeasurements theorem operational_locality_gives_remote_non_disturbance (reality : RealityCriterionContext Setting (MatchingSpinMeasurement Setting) BellCorrelationStage) {operationalLocality : Prop} (principle : OperationalLocalityGivesRemoteNonDisturbance reality operationalLocality) (locality : operationalLocality) : EveryChosenRemoteSpinResultUndisturbed reality := principle locality theorem bell_epr_inputs_make_shared_remote_correlation_route_applicable (framework : BellFramework Setting HiddenState Model Value Error) (reality : RealityCriterionContext Setting (MatchingSpinMeasurement Setting) BellCorrelationStage) (procedureAvailable : MatchingSpinMeasurement Setting → Prop) (component : Setting) {experimentSetup operationalLocality : Prop} (experiment : experimentSetup) (locality : operationalLocality) (matchingMeasurements : MatchingSpinMeasurementsAvailable procedureAvailable) (quantumPerfect : framework.QuantumPerfectAnticorrelation) (predictionPrinciple : framework.PerfectAnticorrelationGivesPredictability reality procedureAvailable) (nonDisturbancePrinciple : OperationalLocalityGivesRemoteNonDisturbance reality operationalLocality) : framework.toRemoteCorrelationPredictionContext reality procedureAvailable experimentSetup operationalLocality |>.RemoteCorrelationRouteApplicableAt (framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality) := by let context := framework.toRemoteCorrelationPredictionContext reality procedureAvailable experimentSetup operationalLocality have calculation : context.CorrelationCalculationAt (framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality) := fun component _ => ⟨rfl, rfl, rfl, rfl, rfl, quantumPerfect⟩ have predictionBridge : context.PredictionReadoutBridgeAt (framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality) := by intro _ _ component _ exact matching_measurement_and_anticorrelation_give_predictability framework reality procedureAvailable predictionPrinciple quantumPerfect matchingMeasurements component have nonDisturbanceBridge : context.NonDisturbanceBridgeAt (framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality) := by intro _ component _ exact operational_locality_gives_remote_non_disturbance reality nonDisturbancePrinciple locality component exact context.setup_calculation_and_bridges_make_route_applicable (framework.bell_inputs_realize_selected_remote_correlation_setup reality procedureAvailable component experiment locality matchingMeasurements) calculation predictionBridge nonDisturbanceBridge /-- Bell's section-II singlet route directly realizes the structural explanation of the selected inhabited certainty-without-disturbance phenomenon. It does not include Bell's later predetermination or inequality conclusions. -/ theorem bell_epr_route_realizes_structural_correlation_explanation (framework : BellFramework Setting HiddenState Model Value Error) (reality : RealityCriterionContext Setting (MatchingSpinMeasurement Setting) BellCorrelationStage) (procedureAvailable : MatchingSpinMeasurement Setting → Prop) (component : Setting) {experimentSetup operationalLocality : Prop} (experiment : experimentSetup) (locality : operationalLocality) (matchingMeasurements : MatchingSpinMeasurementsAvailable procedureAvailable) (quantumPerfect : framework.QuantumPerfectAnticorrelation) (predictionPrinciple : framework.PerfectAnticorrelationGivesPredictability reality procedureAvailable) (nonDisturbancePrinciple : OperationalLocalityGivesRemoteNonDisturbance reality operationalLocality) : framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality |>.DirectStructuralRemoteCorrelationPredictionExplanationAt := framework.toRemoteCorrelationPredictionContext reality procedureAvailable experimentSetup operationalLocality |>.applicable_route_realizes_structural_remote_correlation_explanation (framework |>.bell_epr_inputs_make_shared_remote_correlation_route_applicable reality procedureAvailable component experiment locality matchingMeasurements quantumPerfect predictionPrinciple nonDisturbancePrinciple) /-! Bell's singlet, matching-measurement, and operational-locality inputs realize the source-sensitive remote-prediction explanation before predetermination or the inequality route is introduced. -/ theorem singlet_inputs_realize_source_structural_remote_correlation_explanation (framework : BellFramework Setting HiddenState Model Value Error) (reality : RealityCriterionContext Setting (MatchingSpinMeasurement Setting) BellCorrelationStage) (procedureAvailable : MatchingSpinMeasurement Setting -> Prop) (component : Setting) {experimentSetup operationalLocality : Prop} (experiment : experimentSetup) (locality : operationalLocality) (matchingMeasurements : MatchingSpinMeasurementsAvailable procedureAvailable) (quantumPerfect : framework.QuantumPerfectAnticorrelation) (predictionPrinciple : framework.PerfectAnticorrelationGivesPredictability reality procedureAvailable) (nonDisturbancePrinciple : OperationalLocalityGivesRemoteNonDisturbance reality operationalLocality) : framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality |>.DirectSourceStructuralRemoteCorrelationPredictionExplanationAt .singletAnticorrelationMatchingMeasurementAndOperationalLocality (framework.bellRemoteCorrelationDerivationObtains reality procedureAvailable experimentSetup operationalLocality) := framework.toRemoteCorrelationPredictionContext reality procedureAvailable experimentSetup operationalLocality |>.source_derivation_and_applicable_route_realize_source_structural_remote_correlation_explanation .singletAnticorrelationMatchingMeasurementAndOperationalLocality (framework.bellRemoteCorrelationDerivationObtains reality procedureAvailable experimentSetup operationalLocality) ⟨experiment, locality, matchingMeasurements, quantumPerfect, predictionPrinciple, nonDisturbancePrinciple⟩ (framework |>.bell_epr_inputs_make_shared_remote_correlation_route_applicable reality procedureAvailable component experiment locality matchingMeasurements quantumPerfect predictionPrinciple nonDisturbancePrinciple) theorem bell_epr_route_realizes_shared_remote_correlation_prediction (framework : BellFramework Setting HiddenState Model Value Error) (reality : RealityCriterionContext Setting (MatchingSpinMeasurement Setting) BellCorrelationStage) (procedureAvailable : MatchingSpinMeasurement Setting → Prop) (component : Setting) {experimentSetup operationalLocality : Prop} (experiment : experimentSetup) (locality : operationalLocality) (matchingMeasurements : MatchingSpinMeasurementsAvailable procedureAvailable) (quantumPerfect : framework.QuantumPerfectAnticorrelation) (predictionPrinciple : framework.PerfectAnticorrelationGivesPredictability reality procedureAvailable) (nonDisturbancePrinciple : OperationalLocalityGivesRemoteNonDisturbance reality operationalLocality) : framework.toRemoteCorrelationPredictionContext reality procedureAvailable experimentSetup operationalLocality |>.EstablishedRemoteCorrelationPredictionAt (framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality) := framework.toRemoteCorrelationPredictionContext reality procedureAvailable experimentSetup operationalLocality |>.applicable_route_establishes_remote_correlation_prediction (framework |>.bell_epr_inputs_make_shared_remote_correlation_route_applicable reality procedureAvailable component experiment locality matchingMeasurements quantumPerfect predictionPrinciple nonDisturbancePrinciple) /-- One explicitly chosen spin component witnesses that Bell's arbitrary-component remote-prediction route is nonempty and physically realized. Primary-source anchor: section II, p. 195, where a selected component of particle 2 is predicted by measuring the same component of particle 1 without remote influence. -/ theorem bell_epr_route_exhibits_nonvacuous_shared_remote_correlation (framework : BellFramework Setting HiddenState Model Value Error) (reality : RealityCriterionContext Setting (MatchingSpinMeasurement Setting) BellCorrelationStage) (procedureAvailable : MatchingSpinMeasurement Setting → Prop) (component : Setting) {experimentSetup operationalLocality : Prop} (experiment : experimentSetup) (locality : operationalLocality) (matchingMeasurements : MatchingSpinMeasurementsAvailable procedureAvailable) (quantumPerfect : framework.QuantumPerfectAnticorrelation) (predictionPrinciple : framework.PerfectAnticorrelationGivesPredictability reality procedureAvailable) (nonDisturbancePrinciple : OperationalLocalityGivesRemoteNonDisturbance reality operationalLocality) : framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality |>.NonvacuousRemoteCorrelationPredictionAt := framework.toRemoteCorrelationPredictionContext reality procedureAvailable experimentSetup operationalLocality |>.established_prediction_exhibits_nonvacuous_remote_correlation_prediction (framework |>.bell_epr_route_realizes_shared_remote_correlation_prediction reality procedureAvailable component experiment locality matchingMeasurements quantumPerfect predictionPrinciple nonDisturbancePrinciple) theorem bell_model_inputs_establish_theory_model_grounding (framework : BellFramework Setting HiddenState Model Value Error) (reality : RealityCriterionContext Setting (MatchingSpinMeasurement Setting) BellCorrelationStage) (procedureAvailable : MatchingSpinMeasurement Setting → Prop) (component : Setting) {experimentSetup operationalLocality : Prop} (experiment : experimentSetup) (locality : operationalLocality) (matchingMeasurements : MatchingSpinMeasurementsAvailable procedureAvailable) : framework.toRemoteCorrelationPredictionContext reality procedureAvailable experimentSetup operationalLocality |>.TheoryModelGroundingAt (framework.toRemoteCorrelationPredictionInterpretation reality procedureAvailable experimentSetup operationalLocality) .singletQuantumDescription .separatedSpinPairExperiment (framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality) := by have theoryUse : framework.toRemoteCorrelationPredictionInterpretation reality procedureAvailable experimentSetup operationalLocality |>.theoryUsesRemoteCorrelationModel .singletQuantumDescription (framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality) := ⟨rfl, rfl, experiment⟩ have represents : framework.toRemoteCorrelationPredictionInterpretation reality procedureAvailable experimentSetup operationalLocality |>.remoteCorrelationModelRepresentsWorld (framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality) .separatedSpinPairExperiment := ⟨rfl, rfl, experiment, locality⟩ apply framework.toRemoteCorrelationPredictionContext reality procedureAvailable experimentSetup operationalLocality |>.theory_model_inputs_establish_grounding (framework.toRemoteCorrelationPredictionInterpretation reality procedureAvailable experimentSetup operationalLocality) · exact framework.bell_inputs_realize_selected_remote_correlation_setup reality procedureAvailable component experiment locality matchingMeasurements · exact theoryUse · exact represents · intro _claim modelConclusion exact ⟨rfl, rfl, modelConclusion⟩ · intro _claim modelConclusion exact ⟨rfl, rfl, modelConclusion⟩ theorem bell_epr_route_establishes_theory_model_grounded_remote_prediction (framework : BellFramework Setting HiddenState Model Value Error) (reality : RealityCriterionContext Setting (MatchingSpinMeasurement Setting) BellCorrelationStage) (procedureAvailable : MatchingSpinMeasurement Setting → Prop) (component : Setting) {experimentSetup operationalLocality : Prop} (experiment : experimentSetup) (locality : operationalLocality) (matchingMeasurements : MatchingSpinMeasurementsAvailable procedureAvailable) (quantumPerfect : framework.QuantumPerfectAnticorrelation) (predictionPrinciple : framework.PerfectAnticorrelationGivesPredictability reality procedureAvailable) (nonDisturbancePrinciple : OperationalLocalityGivesRemoteNonDisturbance reality operationalLocality) : framework.toRemoteCorrelationPredictionContext reality procedureAvailable experimentSetup operationalLocality |>.TheoryModelGroundedRemoteCorrelationPredictionAt (framework.toRemoteCorrelationPredictionInterpretation reality procedureAvailable experimentSetup operationalLocality) .singletQuantumDescription .separatedSpinPairExperiment (framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality) := by have established := framework.bell_epr_route_realizes_shared_remote_correlation_prediction reality procedureAvailable component experiment locality matchingMeasurements quantumPerfect predictionPrinciple nonDisturbancePrinciple exact framework.toRemoteCorrelationPredictionContext reality procedureAvailable experimentSetup operationalLocality |>.established_prediction_and_grounding_establish_theory_model_grounded_prediction (framework.toRemoteCorrelationPredictionInterpretation reality procedureAvailable experimentSetup operationalLocality) established (framework |>.bell_model_inputs_establish_theory_model_grounding reality procedureAvailable component experiment locality matchingMeasurements) theorem grounded_bell_remote_prediction_transfers_every_shared_claim (framework : BellFramework Setting HiddenState Model Value Error) (reality : RealityCriterionContext Setting (MatchingSpinMeasurement Setting) BellCorrelationStage) (procedureAvailable : MatchingSpinMeasurement Setting → Prop) {experimentSetup operationalLocality : Prop} (grounded : framework.toRemoteCorrelationPredictionContext reality procedureAvailable experimentSetup operationalLocality |>.TheoryModelGroundedRemoteCorrelationPredictionAt (framework.toRemoteCorrelationPredictionInterpretation reality procedureAvailable experimentSetup operationalLocality) .singletQuantumDescription .separatedSpinPairExperiment (framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality)) : ∀ claim : RemoteCorrelationPredictionClaim Setting, (framework.toRemoteCorrelationPredictionContext reality procedureAvailable experimentSetup operationalLocality |>.toTheoryModelContext (framework.toRemoteCorrelationPredictionInterpretation reality procedureAvailable experimentSetup operationalLocality) |>.theoryEntails (remoteCorrelationTheoryAt BellRemoteTheory.singletQuantumDescription (framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality)) claim ()) ∧ (framework.toRemoteCorrelationPredictionContext reality procedureAvailable experimentSetup operationalLocality |>.toTheoryModelContext (framework.toRemoteCorrelationPredictionInterpretation reality procedureAvailable experimentSetup operationalLocality) |>.trueIn (remoteCorrelationWorldAt BellRemoteWorld.separatedSpinPairExperiment (framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality)) claim ()) := framework.toRemoteCorrelationPredictionContext reality procedureAvailable experimentSetup operationalLocality |>.grounded_prediction_transfers_all_claims_to_theory_and_world grounded theorem epr_requires_more_complete_state_specification {perfectPredictability operationalLocality : Prop} {wavefunctionDeterminesIndividualOutcomes moreCompleteStateSpecificationExists : Prop} (eprPrinciple : EPRPredeterminationPrinciple Setting HiddenState perfectPredictability operationalLocality) (predictable : perfectPredictability) (locality : operationalLocality) (wavefunctionLimitation : ¬wavefunctionDeterminesIndividualOutcomes) (completionPrinciple : PredeterminationRequiresMoreCompleteState Setting HiddenState wavefunctionDeterminesIndividualOutcomes moreCompleteStateSpecificationExists) : moreCompleteStateSpecificationExists := completionPrinciple (epr_predetermination eprPrinciple predictable locality) wavefunctionLimitation theorem epr_predetermination_realized_by_candidate_model_is_local (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) {perfectPredictability operationalLocality : Prop} (eprPrinciple : EPRPredeterminationPrinciple Setting HiddenState perfectPredictability operationalLocality) (predictable : perfectPredictability) (locality : operationalLocality) (dichotomic : framework.ResponsesAreDichotomic model) (realization : framework.EPRPredeterminedResponsesRealizeLocalModel model operationalLocality) : framework.ResponsesUseOnlyLocalSettingAndHiddenState model := realization (epr_predetermination eprPrinciple predictable locality) locality dichotomic /-- Bell's explicit candidate-realization bridge converts the physically inhabited EPR assignment into the established shared local-response result. -/ theorem epr_predetermination_establishes_nonvacuous_candidate_local_response (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) {perfectPredictability operationalLocality : Prop} (eprPrinciple : EPRPredeterminationPrinciple Setting HiddenState perfectPredictability operationalLocality) (predictable : perfectPredictability) (locality : operationalLocality) (dichotomic : framework.ResponsesAreDichotomic model) (realization : framework.EPRPredeterminedResponsesRealizeLocalModel model operationalLocality) : ∃ localResponses : LocalResponses Setting HiddenState, PhysicsLogic.Framework.DeterministicLocalResponse.EstablishedDeterministicLocalResponse (framework.bipartiteResponses model) localResponses := by have predetermined := epr_predetermination eprPrinciple predictable locality obtain ⟨localResponses, factorizes⟩ := framework.epr_predetermination_realized_by_candidate_model_is_local model eprPrinciple predictable locality dichotomic realization exact ⟨localResponses, framework.bell_local_responses_establish_deterministic_local_response model localResponses factorizes predetermined.1⟩ /-- The same source-specific inference supplies an actual hidden state, distinct settings, local support screening, and no-signalling support. -/ theorem epr_predetermination_exhibits_nonvacuous_candidate_local_response (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) {perfectPredictability operationalLocality : Prop} (eprPrinciple : EPRPredeterminationPrinciple Setting HiddenState perfectPredictability operationalLocality) (predictable : perfectPredictability) (locality : operationalLocality) (dichotomic : framework.ResponsesAreDichotomic model) (realization : framework.EPRPredeterminedResponsesRealizeLocalModel model operationalLocality) : ∃ localResponses : LocalResponses Setting HiddenState, (PhysicsLogic.Framework.DeterministicLocalResponse.deterministicLocalResponseCalculationModelAt (framework.bipartiteResponses model) localResponses) |>.NonvacuousDeterministicLocalResponseAt := by obtain ⟨localResponses, established⟩ := framework.epr_predetermination_establishes_nonvacuous_candidate_local_response model eprPrinciple predictable locality dichotomic realization exact ⟨localResponses, PhysicsLogic.Framework.DeterministicLocalResponse.established_response_exhibits_nonvacuous_local_factorization (framework.bipartiteResponses model) localResponses established⟩ /-- Bell's original section-II bridges compose two distinct shared technical results: an actual remote prediction and an actual local hidden-state model. -/ theorem bell_remote_prediction_and_predetermination_realize_nonvacuous_local_response (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (reality : RealityCriterionContext Setting (MatchingSpinMeasurement Setting) BellCorrelationStage) (procedureAvailable : MatchingSpinMeasurement Setting -> Prop) (component : Setting) {experimentSetup operationalLocality : Prop} (experiment : experimentSetup) (locality : operationalLocality) (matchingMeasurements : MatchingSpinMeasurementsAvailable procedureAvailable) (quantumPerfect : framework.QuantumPerfectAnticorrelation) (predictionPrinciple : framework.PerfectAnticorrelationGivesPredictability reality procedureAvailable) (nonDisturbancePrinciple : OperationalLocalityGivesRemoteNonDisturbance reality operationalLocality) (eprPrinciple : EPRPredeterminationPrinciple Setting HiddenState (EveryChosenRemoteSpinResultPredictable reality) operationalLocality) (realization : framework.EPRPredeterminedResponsesRealizeLocalModel model operationalLocality) : (framework.remoteCorrelationModel reality procedureAvailable experimentSetup operationalLocality |>.NonvacuousRemoteCorrelationPredictionAt) ∧ ∃ localResponses : LocalResponses Setting HiddenState, (PhysicsLogic.Framework.DeterministicLocalResponse.deterministicLocalResponseCalculationModelAt (framework.bipartiteResponses model) localResponses) |>.NonvacuousDeterministicLocalResponseAt := by have predictable := matching_measurement_and_anticorrelation_give_predictability framework reality procedureAvailable predictionPrinciple quantumPerfect matchingMeasurements exact ⟨framework.bell_epr_route_exhibits_nonvacuous_shared_remote_correlation reality procedureAvailable component experiment locality matchingMeasurements quantumPerfect predictionPrinciple nonDisturbancePrinciple, framework.epr_predetermination_exhibits_nonvacuous_candidate_local_response model eprPrinciple predictable locality (framework.model_responses_are_dichotomic model) realization⟩ /-- For dichotomic response values, Bell's pointwise algebra reduces the difference of two products to the nonnegative `1 - B(b)B(c)` term. -/ theorem dichotomic_response_product_difference [Ring Value] [LinearOrder Value] [IsStrictOrderedRing Value] (responses : LocalResponses Setting HiddenState) (a b c : Setting) (hiddenState : HiddenState) : |responseProduct (orderedRingCorrelationOrder Value) responses a c hiddenState - responseProduct (orderedRingCorrelationOrder Value) responses a b hiddenState| = 1 - responseProduct (orderedRingCorrelationOrder Value) responses b c hiddenState := by cases responseA : responses.left a hiddenState <;> cases responseB : responses.left b hiddenState <;> cases responseC : responses.left c hiddenState <;> simp [responseProduct, outcomeValue, orderedRingCorrelationOrder, responseA, responseB, responseC] all_goals rw [abs_of_nonpos] <;> norm_num /-- The stronger all-function laws imply the restricted laws. The converse is not assumed; a general probability integral is used only on its integrable domain. -/ theorem bell_response_average_laws_of_all_function_laws (order : CorrelationOrder Value) (average : HiddenAverage HiddenState Value) (responses : LocalResponses Setting HiddenState) (preservesSubtraction : average.PreservesSubtraction order.sub) (preservesConstants : average.PreservesConstants) (absoluteBound : average.SatisfiesAbsoluteBound order.magnitude order.le) : BellResponseAverageLaws order average responses := ⟨fun a b c => preservesSubtraction (responseProduct order responses a c) (responseProduct order responses a b), preservesConstants _, fun a b c => absoluteBound (fun state => order.sub (responseProduct order responses a c state) (responseProduct order responses a b state)), fun b c => preservesSubtraction (fun _ => order.one) (responseProduct order responses b c)⟩ /-- Bell's equation (15) follows from equation (14) and averaging laws on just the response expressions used in the calculation. -/ theorem single_response_average_satisfies_bell_inequality [Ring Value] [LinearOrder Value] [IsStrictOrderedRing Value] (average : HiddenAverage HiddenState Value) (responses : LocalResponses Setting HiddenState) (correlation : Correlation Setting Value) (averageLaws : BellResponseAverageLaws (orderedRingCorrelationOrder Value) average responses) (singleResponse : IsSingleResponseAverage (orderedRingCorrelationOrder Value) average responses correlation) : SatisfiesBell1964Inequality (orderedRingCorrelationOrder Value) correlation := by rcases averageLaws with ⟨subtractProducts, averageOne, absoluteBound, subtractFromOne⟩ change average.value (fun _ => (1 : Value)) = 1 at averageOne intro a b c change |correlation a b - correlation a c| ≤ 1 + correlation b c rw [singleResponse a b, singleResponse a c, singleResponse b c] calc |-average.value (responseProduct (orderedRingCorrelationOrder Value) responses a b) - -average.value (responseProduct (orderedRingCorrelationOrder Value) responses a c)| = |average.value (responseProduct (orderedRingCorrelationOrder Value) responses a c) - average.value (responseProduct (orderedRingCorrelationOrder Value) responses a b)| := by congr 1 abel _ = |average.value (fun hiddenState => responseProduct (orderedRingCorrelationOrder Value) responses a c hiddenState - responseProduct (orderedRingCorrelationOrder Value) responses a b hiddenState)| := by exact congrArg (fun value : Value => |value|) (subtractProducts a b c).symm _ ≤ average.value (fun hiddenState => |responseProduct (orderedRingCorrelationOrder Value) responses a c hiddenState - responseProduct (orderedRingCorrelationOrder Value) responses a b hiddenState|) := absoluteBound a b c _ = average.value (fun hiddenState => 1 - responseProduct (orderedRingCorrelationOrder Value) responses b c hiddenState) := by congr 1 funext hiddenState exact dichotomic_response_product_difference responses a b c hiddenState _ = average.value (fun _ => 1) - average.value (responseProduct (orderedRingCorrelationOrder Value) responses b c) := by exact subtractFromOne b c _ = 1 - average.value (responseProduct (orderedRingCorrelationOrder Value) responses b c) := by rw [averageOne] _ = 1 + -average.value (responseProduct (orderedRingCorrelationOrder Value) responses b c) := by simp [sub_eq_add_neg] /-- Any paper-local realization of equation (14) by a normalized positive linear average therefore supplies equation (15); no separate inequality calculation is needed. -/ theorem represented_single_response_form_satisfies_bell_inequality [Ring Value] [LinearOrder Value] [IsStrictOrderedRing Value] (framework : BellFramework Setting HiddenState Model Value Error) (orderIsStandard : framework.order = orderedRingCorrelationOrder Value) (representation : framework.SingleResponseFormHasAverageRepresentation) : framework.SingleResponseFormSatisfiesBellInequality := by intro responses correlation singleForm obtain ⟨average, averageLaws, singleResponse⟩ := representation responses correlation singleForm rw [orderIsStandard] at averageLaws singleResponse ⊢ exact single_response_average_satisfies_bell_inequality average responses correlation averageLaws singleResponse private def signedCounterexampleAverage : HiddenAverage Bool Real where value integrand := 2 * integrand false - integrand true private inductive SignedCounterexampleSetting where | a | b | c deriving DecidableEq private def signedCounterexampleResponses : LocalResponses SignedCounterexampleSetting Bool where left setting hiddenState := match hiddenState, setting with | false, _ => .minus | true, .c => .plus | true, _ => .minus right _ _ := .minus private def signedCounterexampleCorrelation : Correlation SignedCounterexampleSetting Real := fun left right => -signedCounterexampleAverage.value (responseProduct realCorrelationOrder signedCounterexampleResponses left right) theorem signed_counterexample_average_preserves_subtraction : signedCounterexampleAverage.PreservesSubtraction (· - ·) := by intro left right simp [signedCounterexampleAverage] ring theorem signed_counterexample_average_preserves_constants : signedCounterexampleAverage.PreservesConstants := by intro constant simp [signedCounterexampleAverage] ring theorem signed_counterexample_has_single_response_form : IsSingleResponseAverage realCorrelationOrder signedCounterexampleAverage signedCounterexampleResponses signedCounterexampleCorrelation := by intro left right rfl /-- Normalization and linearity alone do not imply Bell's inequality: the signed weights `2` and `-1` preserve constants and subtraction but violate the absolute-average bound required of a probability distribution. -/ theorem signed_counterexample_violates_bell_inequality : ViolatesBell1964Inequality realCorrelationOrder signedCounterexampleCorrelation := by refine ⟨.a, .b, .c, ?_⟩ have correlationAB : signedCounterexampleCorrelation .a .b = -1 := by change -(2 * ((-1 : Real) * -1) - ((-1 : Real) * -1)) = -1 norm_num have correlationAC : signedCounterexampleCorrelation .a .c = -3 := by change -(2 * ((-1 : Real) * -1) - ((-1 : Real) * 1)) = -3 norm_num have correlationBC : signedCounterexampleCorrelation .b .c = -3 := by change -(2 * ((-1 : Real) * -1) - ((-1 : Real) * 1)) = -3 norm_num change 1 + signedCounterexampleCorrelation .b .c < |signedCounterexampleCorrelation .a .b - signedCounterexampleCorrelation .a .c| rw [correlationAB, correlationAC, correlationBC] norm_num theorem signed_counterexample_fails_absolute_average_bound : ¬signedCounterexampleAverage.SatisfiesAbsoluteBound abs (· ≤ ·) := by intro absoluteBound have impossible := absoluteBound (fun hiddenState : Bool => if hiddenState then 1 else 0) norm_num [signedCounterexampleAverage] at impossible theorem exact_agreement_transfers_bell_inequality (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (modelBound : SatisfiesBell1964Inequality framework.order (framework.modelCorrelation model)) (agreement : framework.ReproducesQuantumCorrelation model) : SatisfiesBell1964Inequality framework.order framework.quantumCorrelation := by intro a b c have bound := modelBound a b c rw [agreement a b, agreement a c, agreement b c] at bound exact bound theorem violation_excludes_bell_inequality (order : CorrelationOrder Value) (orderConsistent : order.Consistent) {correlation : Correlation Setting Value} (violation : ViolatesBell1964Inequality order correlation) : ¬SatisfiesBell1964Inequality order correlation := by intro bound cases violation with | intro a settingsBC => cases settingsBC with | intro b settingC => cases settingC with | intro c violates => exact orderConsistent (order.magnitude (order.sub (correlation a b) (correlation a c))) (order.add order.one (correlation b c)) (bound a b c) violates /-- Bell's original eq. (13) to eq. (15) derivation for a reproducing model. -/ theorem reproducing_local_model_satisfies_bell_inequality (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (localModel : framework.IsLocalHiddenVariableModel model) (agreement : framework.ReproducesQuantumCorrelation model) (quantumPerfect : framework.QuantumPerfectAnticorrelation) (opposition : framework.PerfectAnticorrelationForcesOppositeResponses) (rewrite : framework.OppositeResponsesGiveSingleResponseForm) (deriveInequality : framework.SingleResponseFormSatisfiesBellInequality) : SatisfiesBell1964Inequality framework.order (framework.modelCorrelation model) := by obtain ⟨localResponses, factorizes, localAverage⟩ := localModel.2 have modelPerfect := framework.agreement_transfers_perfect_anticorrelation model agreement quantumPerfect have opposite := opposition model localResponses localModel.1 factorizes localAverage modelPerfect have singleForm := rewrite model localResponses localAverage opposite exact deriveInequality localResponses (framework.modelCorrelation model) singleForm /-- The checked exact no-go conclusion of Bell's 1964 section IV. -/ theorem no_exact_local_representation (framework : BellFramework Setting HiddenState Model Value Error) (orderConsistent : framework.order.Consistent) (localBound : framework.EveryLocalModelSatisfiesBellInequality) (quantumViolation : ViolatesBell1964Inequality framework.order framework.quantumCorrelation) : ¬framework.HasExactLocalRepresentation := by intro representation cases representation with | intro model properties => have quantumBound := exact_agreement_transfers_bell_inequality framework model (localBound model properties.1) properties.2 exact violation_excludes_bell_inequality framework.order orderConsistent quantumViolation quantumBound /-- The exact no-go with Bell's eqs. (13), (14), and (15) exposed rather than compressed into a single local-bound hypothesis. -/ theorem no_exact_local_representation_from_original_derivation [Ring Value] [LinearOrder Value] [IsStrictOrderedRing Value] (framework : BellFramework Setting HiddenState Model Value Error) (orderIsStandard : framework.order = orderedRingCorrelationOrder Value) (quantumPerfect : framework.QuantumPerfectAnticorrelation) (opposition : framework.PerfectAnticorrelationForcesOppositeResponses) (rewrite : framework.OppositeResponsesGiveSingleResponseForm) (averageRepresentation : framework.SingleResponseFormHasAverageRepresentation) (singletFormula : framework.QuantumSingletCorrelationFormula) (violationCalculation : framework.QuantumSingletViolationCalculation) : ¬framework.HasExactLocalRepresentation := by have orderConsistent : framework.order.Consistent := by rw [orderIsStandard] intro left right bound exact not_lt_of_ge bound have deriveInequality := represented_single_response_form_satisfies_bell_inequality framework orderIsStandard averageRepresentation have quantumViolation := violationCalculation singletFormula intro representation obtain ⟨model, localModel, agreement⟩ := representation have modelBound := reproducing_local_model_satisfies_bell_inequality framework model localModel agreement quantumPerfect opposition rewrite deriveInequality have quantumBound := exact_agreement_transfers_bell_inequality framework model modelBound agreement exact violation_excludes_bell_inequality framework.order orderConsistent quantumViolation quantumBound /-- Bell's positive approximation gap excludes arbitrary local accuracy. -/ theorem no_arbitrarily_accurate_local_approximation (framework : BellFramework Setting HiddenState Model Value Error) (gap : framework.HasBellApproximationGap) : ¬framework.HasArbitrarilyAccurateLocalApproximation := by intro arbitraryAccuracy cases gap with | intro error gapProperties => have approximationExists := arbitraryAccuracy error gapProperties.1 cases approximationExists with | intro model approximationProperties => exact gapProperties.2 model approximationProperties.1 approximationProperties.2 /-- Bell's three examples show that hidden variables as such are not excluded. -/ theorem scope_illustrations_preserve_hidden_variable_possibility (framework : BellFramework Setting HiddenState Model Value Error) (illustrations : framework.ScopeIllustrations) : HiddenVariableAccountsRemainPossible Model := by obtain ⟨model, _⟩ := illustrations.1 exact ⟨model⟩ /-- The nonlocal illustration reproduces the full singlet correlation, while the no-go theorem excludes only its membership in the local class. -/ theorem nonlocal_singlet_illustration_identifies_locality_as_obstruction (framework : BellFramework Setting HiddenState Model Value Error) (noLocalRepresentation : ¬framework.HasExactLocalRepresentation) (nonlocalAccount : framework.HasNonlocalSingletCorrelationAccount) : ∃ model, framework.ReproducesQuantumCorrelation model ∧ ¬framework.IsLocalHiddenVariableModel model := by obtain ⟨model, supplement, _⟩ := nonlocalAccount have agreement := supplement.2.2 refine ⟨model, agreement, ?_⟩ intro localModel exact noLocalRepresentation ⟨model, localModel, agreement⟩ /-- Bell's section V reduction produces an incompatible higher-dimensional state. -/ theorem higher_dimensional_separable_predetermination_fails {State : Type u} {Observable : Type v} (scenario : HigherDimensionalScenario State Observable) (observability : scenario.CompleteHermitianOperatorsAreObservable) (subscenario : scenario.HasBellSubscenario) (reduction : scenario.BellSubscenarioObstructsSeparablePredetermination) : ∃ state, ¬scenario.separablePredeterminationCompatible state := by obtain ⟨state, containsBellScenario⟩ := subscenario exact ⟨state, reduction observability state containsBellScenario⟩ /-- If a deterministic supplement reproduces the quantum correlations, Bell's no-go forces that supplement outside the local class. -/ theorem every_reproducing_completion_is_nonlocal (framework : BellFramework Setting HiddenState Model Value Error) (noLocalRepresentation : ¬framework.HasExactLocalRepresentation) (model : Model) (agreement : framework.ReproducesQuantumCorrelation model) : ¬framework.IsLocalHiddenVariableModel model := by intro localModel exact noLocalRepresentation ⟨model, localModel, agreement⟩ /-- A deterministic supplement with no distant-setting influence would factor into Bell-local responses and hence be a local hidden-variable model. -/ theorem deterministic_supplement_without_distant_influence_is_local (framework : BellFramework Setting HiddenState Model Value Error) (averageConversion : framework.FactorizedBipartiteAverageGivesLocalCorrelation) (model : Model) (supplement : framework.DeterministicSupplementReproducesQuantumCorrelations model) (noInfluence : ¬framework.DistantSettingInfluencesRemoteOutcome model) : framework.IsLocalHiddenVariableModel model := by have localDependence := (framework.no_distant_setting_influence_iff_local_response_dependence model).mp noInfluence exact ⟨supplement.1, averageConversion model localDependence supplement.2.1⟩ /-- A reproducing deterministic completion requires distant-setting dependence. -/ theorem reproducing_completion_requires_distant_influence (framework : BellFramework Setting HiddenState Model Value Error) (noLocalRepresentation : ¬framework.HasExactLocalRepresentation) (averageConversion : framework.FactorizedBipartiteAverageGivesLocalCorrelation) (model : Model) (supplement : framework.DeterministicSupplementReproducesQuantumCorrelations model) : framework.DistantSettingInfluencesRemoteOutcome model := by by_contra noInfluence have localModel := deterministic_supplement_without_distant_influence_is_local framework averageConversion model supplement noInfluence exact noLocalRepresentation ⟨model, localModel, supplement.2.2⟩ /-- For separated measurements, the required influence is instantaneous. -/ theorem reproducing_completion_requires_instantaneous_influence (framework : BellFramework Setting HiddenState Model Value Error) (noLocalRepresentation : ¬framework.HasExactLocalRepresentation) (averageConversion : framework.FactorizedBipartiteAverageGivesLocalCorrelation) (measurementsAreSpacelikeSeparated : Prop) (separation : measurementsAreSpacelikeSeparated) (separatedInfluenceIsInstantaneous : framework.SeparatedInfluenceIsInstantaneous measurementsAreSpacelikeSeparated) (model : Model) (supplement : framework.DeterministicSupplementReproducesQuantumCorrelations model) : framework.InfluenceIsInstantaneous model := separatedInfluenceIsInstantaneous model separation (reproducing_completion_requires_distant_influence framework noLocalRepresentation averageConversion model supplement) /-- An instantaneous influence across nonzero spatial separation reverses temporal order in an admissibly boosted inertial frame. -/ theorem instantaneous_influence_reverses_causal_order_in_some_inertial_frame (framework : BellFramework Setting HiddenState Model Value Error) (model : Model) (instantaneous : framework.InfluenceIsInstantaneous model) : ¬framework.CausalDirectionPreservedInEveryInertialFrame model := by intro preserved rcases instantaneous with ⟨temporalZero, spatialNonzero⟩ rcases lt_or_gt_of_ne spatialNonzero with spatialNegative | spatialPositive · have boostedOrder := preserved (-1 / 2) (by norm_num [IsAdmissibleBoost]) simp [BoostedInfluenceTemporalSeparation, temporalZero] at boostedOrder linarith · have boostedOrder := preserved (1 / 2) (by norm_num [IsAdmissibleBoost]) simp [BoostedInfluenceTemporalSeparation, temporalZero] at boostedOrder linarith /-- Bell's final conditional Lorentz conclusion. -/ theorem reproducing_completion_is_not_lorentz_invariant (framework : BellFramework Setting HiddenState Model Value Error) (noLocalRepresentation : ¬framework.HasExactLocalRepresentation) (averageConversion : framework.FactorizedBipartiteAverageGivesLocalCorrelation) (measurementsAreSpacelikeSeparated : Prop) (separation : measurementsAreSpacelikeSeparated) (separatedInfluenceIsInstantaneous : framework.SeparatedInfluenceIsInstantaneous measurementsAreSpacelikeSeparated) (lorentzCausalDirection : framework.LorentzInvariantInfluencePreservesCausalDirection) (model : Model) (supplement : framework.DeterministicSupplementReproducesQuantumCorrelations model) : ¬framework.lorentzInvariant model := by have influence := reproducing_completion_requires_distant_influence framework noLocalRepresentation averageConversion model supplement have instantaneous := reproducing_completion_requires_instantaneous_influence framework noLocalRepresentation averageConversion measurementsAreSpacelikeSeparated separation separatedInfluenceIsInstantaneous model supplement have orderReversal := instantaneous_influence_reverses_causal_order_in_some_inertial_frame framework model instantaneous intro lorentzInvariant exact orderReversal (lorentzCausalDirection model lorentzInvariant influence) /-- A fast-setting experiment that confirms the quantum predictions removes Bell's limited-validity escape for that experimental regime. -/ theorem fast_setting_experiment_excludes_limited_validity_escape {fastSettingExperimentSupportsQuantumPredictions quantumPredictionsRemainValidDuringParticleFlight : Prop} (testPrinciple : FastSettingExperimentTestsLimitedValidity fastSettingExperimentSupportsQuantumPredictions quantumPredictionsRemainValidDuringParticleFlight) (experimentalSupport : fastSettingExperimentSupportsQuantumPredictions) : ¬LimitedValidityEscape quantumPredictionsRemainValidDuringParticleFlight := by unfold LimitedValidityEscape intro limitedValidity exact limitedValidity (testPrinciple experimentalSupport) namespace Countermodels /-- Positive scales need not satisfy Bell's printed equation-(22) bound. -/ theorem positive_scales_do_not_establish_equation_twenty_two_lower_bound : (0 : Real) < 1 / 100 ∧ (0 : Real) < 1 / 100 ∧ ¬PaperDirectionApproximationLowerBound (1 / 100) (1 / 100) := by have rootSquare : (Real.sqrt 2) ^ 2 = 2 := Real.sq_sqrt (by norm_num) have rootPositive : 0 < Real.sqrt 2 := Real.sqrt_pos.2 (by norm_num) constructor · norm_num constructor · norm_num intro lowerBound unfold PaperDirectionApproximationLowerBound at lowerBound norm_num at lowerBound nlinarith private def everyClaimConsideredPossible : PossibilityStatusContext Prop Unit where consideredPossibleAt := fun _ _ => True private def noClaimEstablished : EstablishmentStatusContext Prop Unit where establishedAt := fun _ _ => False /-- Treating Bell's limited-validity escape as tentative does not assert that the quantum predictions actually fail during flight. -/ theorem tentative_limited_validity_does_not_assert_actual_failure : LimitedValidityAlternativeIsTentative everyClaimConsideredPossible noClaimEstablished () True ∧ ¬LimitedValidityEscape True := by constructor · exact ⟨trivial, id⟩ · simp [LimitedValidityEscape] private def calibrationWithoutAverageData : SingleSpinIllustrationData where polarization := bellDirectionB rotatedDirection := fun direction => direction angleToPolarization := fun _ => 0 rotatedAngleToPolarization := fun _ => 0 response := fun _ _ => .plus average := fun _ => 0 uniformOn := fun _ => True /-- Equation (6) alone cannot supply equation (7): the hemisphere-average calculation remains a logically active input. -/ theorem rotation_calibration_without_hemisphere_average_does_not_supply_expectation : ∃ data : SingleSpinIllustrationData, SingleSpinIllustrationData.HasRotationCalibration data ∧ ¬SingleSpinIllustrationData.ReproducesPureSpinExpectation data := by refine ⟨calibrationWithoutAverageData, ?_, ?_⟩ · intro measurementDirection unitDirection simp [calibrationWithoutAverageData] · intro expectation have unitDirection : bellDirectionB.IsUnit := bell_directions_are_unit.2.1 have result := expectation bellDirectionB unitDirection norm_num [calibrationWithoutAverageData] at result private def unavailableMatchingMeasurement (measurement : MatchingSpinMeasurement Bool) : Prop := measurement.component = true private def noRemotePrediction : RealityCriterionContext Bool (MatchingSpinMeasurement Bool) BellCorrelationStage where predictableWithCertainty := fun measurement component _ => measurement.component = component ∧ component = true leavesUndisturbed := fun measurement component _ => measurement.component = component physicallyAdmissible := fun component _ => component = false ∨ component = true private def perfectReferenceCorrelation (leftSetting rightSetting : Bool) : Real := if leftSetting = rightSetting then -1 else 0 def HasPerfectReferenceAnticorrelation : Prop := ∀ component, perfectReferenceCorrelation component component = -1 /-- An abstract perfect-anticorrelation proposition supplies neither an available matching measurement nor a certainty relation. Bell's operational bridge and its availability premise therefore cannot be omitted. -/ theorem perfect_anticorrelation_alone_does_not_supply_operational_predictability : HasPerfectReferenceAnticorrelation ∧ ¬MatchingSpinMeasurementsAvailable unavailableMatchingMeasurement ∧ ¬EveryChosenRemoteSpinResultPredictable noRemotePrediction := by refine ⟨?_, ?_, ?_⟩ · intro component simp [perfectReferenceCorrelation] · intro available simpa [unavailableMatchingMeasurement] using available false · intro predictable have prediction := predictable false simpa [noRemotePrediction] using prediction.2 private def remoteSettingDependentResponses : BipartiteResponses Bool Unit where left _ rightSetting _ := if rightSetting then .plus else .minus right _ _ _ := .plus /-- The abstract existence of predetermined local response values does not identify them with an arbitrary candidate model's response functions. The explicit realization bridge in section II is therefore logically necessary. -/ theorem predetermined_responses_do_not_realize_an_arbitrary_candidate_model : PredeterminedLocalResponses Bool Unit ∧ ¬∃ localResponses : LocalResponses Bool Unit, ∀ leftSetting rightSetting hiddenState, remoteSettingDependentResponses.left leftSetting rightSetting hiddenState = localResponses.left leftSetting hiddenState ∧ remoteSettingDependentResponses.right leftSetting rightSetting hiddenState = localResponses.right rightSetting hiddenState := by constructor · exact ⟨⟨⟨()⟩, false, true, Bool.false_ne_true⟩, ⟨{ left := fun _ _ => .plus right := fun _ _ => .minus }⟩⟩ · rintro ⟨localResponses, factorizes⟩ have atFalse := (factorizes false false ()).1 have atTrue := (factorizes false true ()).1 simp [remoteSettingDependentResponses] at atFalse atTrue exact Outcome.noConfusion (atFalse.trans atTrue.symm) /-- Total functions on an empty hidden-state domain carry no physical value. -/ def emptyHiddenStateLocalResponses : LocalResponses Bool Empty where left _ hiddenState := nomatch hiddenState right _ hiddenState := nomatch hiddenState theorem empty_hidden_state_response_functions_do_not_establish_predetermination : Nonempty (LocalResponses Bool Empty) ∧ ¬PredeterminedLocalResponses Bool Empty := by refine ⟨⟨emptyHiddenStateLocalResponses⟩, ?_⟩ intro predetermined rcases predetermined.1.1 with ⟨hiddenState⟩ exact nomatch hiddenState /-- Universal functions over no magnet settings provide no predictions. -/ def emptySettingLocalResponses : LocalResponses Empty Unit where left setting := nomatch setting right setting := nomatch setting theorem empty_setting_response_functions_do_not_establish_predetermination : Nonempty (LocalResponses Empty Unit) ∧ ¬PredeterminedLocalResponses Empty Unit := by refine ⟨⟨emptySettingLocalResponses⟩, ?_⟩ intro predetermined rcases predetermined.1.2 with ⟨setting, _alternative, _distinct⟩ exact nomatch setting /-- One fixed magnet setting cannot encode Bell's alternative local choices. -/ def singletonSettingLocalResponses : LocalResponses Unit Unit where left _ _ := .plus right _ _ := .minus theorem singleton_setting_response_functions_do_not_establish_predetermination : Nonempty (LocalResponses Unit Unit) ∧ ¬PredeterminedLocalResponses Unit Unit := by refine ⟨⟨singletonSettingLocalResponses⟩, ?_⟩ intro predetermined rcases predetermined.1.2 with ⟨first, alternative, distinct⟩ cases first cases alternative exact distinct rfl /-- A finite-speed influence can reach a remote apparatus after positive elapsed time without reaching it at the emission time. -/ def SignalCanReachBy (distance signalSpeed elapsedTime : Nat) : Prop := distance ≤ signalSpeed * elapsedTime theorem distant_influence_does_not_by_itself_imply_instantaneous_propagation : SignalCanReachBy 2 1 2 ∧ ¬SignalCanReachBy 2 1 0 := by norm_num [SignalCanReachBy] end Countermodels end BellFramework /-! ## Actual Spin Density Matrices for Equations (3) and (11) -/ namespace FiniteSpinPair open Matrix FiniteQuantumState open scoped BigOperators ComplexOrder Kronecker set_option backward.isDefEq.respectTransparency false def observable (direction : SpinDirection) : Operator QubitBasis := spinObservable direction.x direction.y direction.z def correlation (rho : Operator PairBasis) (left right : SpinDirection) : Real := expectation rho (observable left ⊗ₖ observable right) def axisKet (index : Fin 6) : QubitBasis -> Complex := match index.val with | 0 => ![1, 1] | 1 => ![1, -1] | 2 => ![1, Complex.I] | 3 => ![1, -Complex.I] | 4 => ketZero | _ => ketOne def axisNormalization (index : Fin 6) : Real := if index.val < 4 then 1 / 2 else 1 def axisState (index : Fin 6) : Operator QubitBasis := axisNormalization index • outer (axisKet index) def oppositeAxis (index : Fin 6) : Fin 6 := match index.val with | 0 => 1 | 1 => 0 | 2 => 3 | 3 => 2 | 4 => 5 | _ => 4 /-- Six equally weighted opposite-spin product states realize the isotropic mixture. -/ def isotropicMixture : ProductMixture QubitBasis QubitBasis 6 where weight := fun _ => 1 / 6 leftState := axisState rightState := fun index => axisState (oppositeAxis index) def isotropicState : Operator PairBasis := isotropicMixture.matrix theorem axisState_isDensity (index : Fin 6) : IsDensity (axisState index) := by apply scaled_outer_isDensity · unfold axisNormalization split <;> norm_num · fin_cases index <;> norm_num [axisNormalization, axisKet, ketZero, ketOne, Fin.sum_univ_two, Complex.normSq_apply] theorem isotropicMixture_admissible : isotropicMixture.Admissible := by exact ⟨by intro index; norm_num [isotropicMixture], by norm_num [isotropicMixture, Fin.sum_univ_succ], fun index => ⟨axisState_isDensity index, axisState_isDensity (oppositeAxis index)⟩⟩ theorem isotropicState_separable : Separable isotropicState := ⟨6, isotropicMixture, isotropicMixture_admissible, rfl⟩ set_option maxHeartbeats 800000 in /-- The finite mixture is rotationally isotropic at the density-operator level. -/ theorem isotropicState_matrix : isotropicState = (1 / 6 : Real) • 1 + (1 / 3 : Real) • singlet := by ext ⟨i, j⟩ ⟨k, l⟩ fin_cases i <;> fin_cases j <;> fin_cases k <;> fin_cases l <;> norm_num [isotropicState, isotropicMixture, ProductMixture.matrix, axisState, axisNormalization, axisKet, oppositeAxis, singlet, singletVector, tensorKet, ketZero, ketOne, outer, Matrix.vecMulVec_apply, Fin.sum_univ_succ, Complex.real_smul, map_ofNat] <;> ring_nf <;> norm_num [Complex.I_sq] theorem actual_singlet_correlation_is_equation_three (left right : SpinDirection) : correlation singlet left right = singletCorrelation left right := by norm_num [correlation, expectation, observable, spinObservable, pauliX, pauliY, pauliZ, singlet, outer, singletVector, tensorKet, ketZero, ketOne, Matrix.trace, Matrix.mul_apply, Matrix.vecMulVec_apply, Fintype.sum_prod_type, Fin.sum_univ_two, Complex.real_smul, Complex.mul_re, Complex.mul_im, singletCorrelation, SpinDirection.dot] ring theorem observable_traceless (direction : SpinDirection) : Matrix.trace (observable direction) = 0 := by simp [observable, spinObservable, pauliX, pauliY, pauliZ, Matrix.trace, Fin.sum_univ_two, Complex.real_smul] theorem identity_has_zero_spin_correlation (left right : SpinDirection) : correlation (1 : Operator PairBasis) left right = 0 := by change (Matrix.trace ((1 : Operator PairBasis) * (observable left ⊗ₖ observable right))).re = 0 rw [one_mul, Matrix.trace_kronecker, observable_traceless, observable_traceless] norm_num /-- Bell's original section-III equation (11), not a modern replacement inequality. -/ theorem actual_isotropic_product_mixture_is_equation_eleven (left right : SpinDirection) : correlation isotropicState left right = -(left.dot right) / 3 := by rw [isotropicState_matrix] change expectation ((1 / 6 : Real) • 1 + (1 / 3 : Real) • singlet) (observable left ⊗ₖ observable right) = _ rw [expectation_add, expectation_real_smul, expectation_real_smul] change (1 / 6 : Real) * correlation 1 left right + (1 / 3 : Real) * correlation singlet left right = _ rw [identity_has_zero_spin_correlation, actual_singlet_correlation_is_equation_three] simp [singletCorrelation] ring def SourceEquationElevenAt : Prop := IsDensity isotropicState /\ Separable isotropicState /\ ∀ left right, correlation isotropicState left right = -(left.dot right) / 3 theorem source_equation_eleven_is_realized : SourceEquationElevenAt := ⟨separable_isDensity isotropicState_separable, isotropicState_separable, actual_isotropic_product_mixture_is_equation_eleven⟩ theorem isotropicState_marginals : partialTraceRight isotropicState = maximallyMixedQubit /\ partialTraceLeft isotropicState = maximallyMixedQubit := by rw [isotropicState_matrix] constructor <;> ext i j <;> fin_cases i <;> fin_cases j <;> norm_num [partialTraceRight, partialTraceLeft, singlet, outer, singletVector, tensorKet, ketZero, ketOne, maximallyMixedQubit, Matrix.vecMulVec_apply, Fin.sum_univ_two, Complex.real_smul] def zDirection : SpinDirection := ⟨0, 0, 1⟩ theorem equal_local_states_do_not_fix_singlet_correlations : IsDensity isotropicState /\ Separable isotropicState /\ IsPure singlet /\ ¬Separable singlet /\ partialTraceRight isotropicState = partialTraceRight singlet /\ partialTraceLeft isotropicState = partialTraceLeft singlet /\ correlation isotropicState zDirection zDirection = -(1 / 3) /\ correlation singlet zDirection zDirection = -1 := by refine ⟨separable_isDensity isotropicState_separable, isotropicState_separable, singlet_isPure, singlet_not_separable, isotropicState_marginals.1.trans singlet_marginals.1.symm, isotropicState_marginals.2.trans singlet_marginals.2.symm, ?_, ?_⟩ · norm_num [actual_isotropic_product_mixture_is_equation_eleven, zDirection, SpinDirection.dot] · norm_num [actual_singlet_correlation_is_equation_three, singletCorrelation, zDirection, SpinDirection.dot] theorem actual_density_matrix_violates_the_original_bell_inequality : IsPure singlet /\ BellFramework.ViolatesBell1964Inequality realCorrelationOrder (correlation singlet) := by refine ⟨singlet_isPure, ?_⟩ have equality : correlation singlet = singletCorrelation := funext fun left => funext fun right => actual_singlet_correlation_is_equation_three left right rw [equality] exact BellFramework.concrete_singlet_correlation_violates_bell_1964 end FiniteSpinPair end PhysicsLogic.Papers.Bell1964