Formal reconstruction · Local hidden variables and singlet correlations
On the Einstein Podolsky Rosen Paradox
The logical anatomy of EPR predetermination, Bell's original three-setting inequality, its quantum violation, and the conditional physical conclusion
Definitions, structures, and assumptions
Structures, classes, and inductive alternatives
- structure
- structureThe selected response calculation contains only the unrestricted bipartite responses and the proposed local response functions. It carries no proof of factorization, theory use, or physical representation.
- inductiveOnly the response-factorization claims independently shared by Bell 1964 and CHSH 1969 transfer through the interpretation. Correlations, probability distributions, detector assumptions, inequalities, and apparatus physics are not constructors.
- structureProof-free constraint selecting one exact deterministic-response calculation. It stores no factorization, nontrivial-domain, support-screening, or no-signalling proof.
- structureThe selected response constraint plus one typed paper-local derivation. The proposition-valued source relation keeps Bell's complete-state local functional form distinct from CHSH's locally carried shared-information premise.
- structurePaper-local meanings for a selected response calculation, the theory using it, and the bipartite experiment it represents.
- structureThe selected situated deterministic local-response phenomenon. It retains the unrestricted and local response functions but no factorization or support proof.
- structureThe theory using the response calculation is distinct from the calculation.
- structureThe represented bipartite experiment is distinct from model and theory.
- structure
- structureProof-free data for a finite convex decomposition into product states.
- structureThe selected phenomenon: an inhabited sector of remote quantities is predictable with certainty by local procedures that leave those quantities undisturbed.
- structureProof-free data and proposition families selected by one exact remote- correlation route. No field supplies a proof of preparation, separation, procedure availability, correlation, prediction, non-disturbance, applicability, theory use, or physical representation. The local procedure subsystem and remote predicted subsystem are retained as separate selected objects. Separation, procedure availability, and the correlation calculation are indexed by those exact roles.
- inductiveEvery proposition retained by the exact shared EPR/Bell route.
- structure
- structurePaper-local theory and world meanings for an exact selected model. A model consequence transfers only through explicit theory and representation bridges.
- structureA paper-local theory object paired with the selected exact model.
- structureA represented separated-system experiment paired with the exact model.
- structureThe two operational relations shared before any reality interpretation.
- structureProof-free data identifying the separated-correlation structure used to explain one selected sector of remote predictions.
- structure
- structure
- structure
- structure
- inductive
- inductive
- inductive
- structure
- inductive
- structure
- structureA selected claim must depend on exactly these source-map steps.
- structureA selected claim must retain exactly these epistemic statuses.
- structureA selected route must name exactly these immediate predecessor routes.
- structure
- structure
- inductive
- inductiveStages distinguished by Bell's preparation-and-separation argument. Primary-source anchor: section II, pp. 195-196.
- inductiveTyped 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.
- structurePaper-local semantic framework for Bell's models and correlations.
- structureThe 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.
- structureThe 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.
- structureSemantic data for Bell's section V higher-dimensional extension.
- inductive
- inductiveThe two distinct members of Bell's separated spin pair.
- inductiveTyped token for Bell's section-II remote-prediction derivation.
- inductive
- inductive
- structureThe 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
- structureOperations needed to state Bell's original inequality abstractly.
- structureThe temporal and one-dimensional spatial displacement from the setting event to the remote reading event in a chosen inertial frame.
- structureThe operational procedure Bell uses to predict a remote spin component: measure that same component on the opposite member of the singlet pair.
- inductive
- structureBell'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.
- structureA spatial Stern-Gerlach orientation.
- structure
- structure
- structure
- structure
- structure
- structure
- structure
- inductive
Definitions and domain choices
- definition
- definition
- definition
- definition
- definition
- definitionThe proof-free response constraint selected by one calculation.
- definitionThe selected response constraint with one paper-local derivation.
- definitionThe proof-free local-response phenomenon selected by one calculation.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionSource-sensitive structural explanation of one selected response route.
- definitionOrdinary structural explanation of one selected local-response route.
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA physically nontrivial deterministic-response domain has an actual shared hidden state and at least two distinguishable apparatus settings. Either setting can also be used on the other wing; nontriviality requires one wing to offer a genuine alternative choice.
- definitionThe pre-factorization content of a selected deterministic response model: the unrestricted bipartite responses and proposed local response functions are exactly the selected data. No factorization or established locality result is included.
- definitionExact selected response data together with its pre-factorization domain.
- definition
- definition
- definition
- definition
- definition
- definition
- definitionInterpret one hidden-state value as common past information and the selected apparatus settings as background conditions. The left and right conditional supports are supplied by the exact local response functions. This is a support relation, not a probability distribution.
- definition
- definition
- definition
- definitionA finite quantum state is positive semidefinite and has unit trace.
- definitionFor a normalized positive operator, idempotence expresses rank-one purity.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionSeparability is an actual finite convex product decomposition.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionSource-sensitive explanation of remote certainty without disturbance.
- definitionThe realized separated-correlation structure explains the selected inhabited sector of certain, non-disturbing remote predictions.
- definitionAt least one physical quantity is selected for remote prediction.
- definition
- definitionThe complete realized remote-correlation result at one proof-free model. This direct proposition is stronger than the implication-valued route: preparation, subsystem separation, procedure availability, the correlation calculation, both physical bridges, and the prediction conclusion all hold at the model's own data, and at least one selected remote quantity witnesses that the universal route is not empty. Physical admissibility is intentionally absent. EPR, Bohr, and Bell share certainty and non-disturbance before EPR applies a further reality criterion, Bohr rejects the arrangement-independent inference, and Bell applies a predetermination principle.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe exact nonempty certainty-without-disturbance phenomenon selected here.
- definitionThe exact separated-correlation constraint selected by this model.
- definitionThe selected separated-correlation constraint with one source route.
- definition
- definition
- definitionStructural-explanation semantics for remote certainty without disturbance. The constraint is satisfied only by the exact model with its prepared and separated setup, calculated correlations, both physical bridges, and a nonempty selected quantity sector. The explained phenomenon contains neither physical admissibility nor any completeness or predetermination conclusion.
- definition
- definitionThe exact technical meaning of every shared claim at one model.
- definition
- definition
- definitionThe output-led established result: exact selected semantics together with the direct, inhabited remote-correlation prediction at the model's own data.
- definition
- definition
- definition
- definitionExact selected semantics retains the experiment, both subsystem roles, regime, both operational observation relations, quantity selection, procedure assignment, and all four route-used physical relation families. Philosophical physical admissibility is not part of the selected technical model.
- definitionThe exact selected prepared and separated experiment, together with a witness that at least one remote quantity is selected, before any correlation calculation or prediction bridge is used.
- definition
- definition
- definition
- definition
- definitionThe exact proof-free model induced by this context at selected indices.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionInterpret an exact correlation model without identifying it with the theory using it or the represented separated-system experiment.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionForget physical admissibility when extracting operational observations.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionImmediate predecessor routes. Claims established by their transitive predecessors are inherited by the dependency closure.
- definition
- definition
- definition
- definition
- definition
- definitionTemporary reductio-introduction steps discharged by this inference. Discharge removes only those exact origins from the conclusion's epistemic basis; it does not assert the temporary hypotheses globally.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA source-mapped claim holds when its declared formula evaluates under the given paper-local semantic interpretation.
- definition
- definition
- definition
- definition
- definition
- definitionEvery claim in the supplied identifier list holds.
- definitionA source-mapped step is semantically sound when the interpreted premises imply the interpreted conclusion. Physical principles and imported calculations therefore remain explicit hypotheses of paper-specific certificates rather than acquiring truth from their source-map labels. A reductio hypothesis is different: it introduces a temporary assumption into a subargument and therefore is not required to hold globally. Its later uses remain ordinary premise-sensitive steps, and discharging it into a negated conclusion remains an ordinary semantic obligation.
- definitionEvery step in the supplied identifier list is semantically sound.
- definition
- definition
- definition
- definition
- definition
- definitionThe formula declared for a claim identifier, when that claim is present.
- definition
- definitionEvery source-mapped step whose justification contributes to the claim through declared premise-to-conclusion steps.
- definitionAll justification statuses contributed by the exact source-mapped origins of a claim. This records epistemic provenance; it does not assert any paper claim or discharge any physical assumption.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe declared argument step with the requested identifier, when present.
- definition
- definitionThe premise list and conclusion attached to a declared step identifier.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA typed countermodel matrix avoids string-keyed audit rows. Each index selects one proposition-valued separation obligation.
- definition
- definition
- definition
- definitionOne countermodel row retains a weaker proposition while rejecting a stronger upgrade. This is a proposition, not a structure carrying proof fields.
- definition
- definition
- definitionIndependent dependency and epistemic ledgers must review the same actual source claims, including every public conclusion and the selected paper conclusion. Empty, duplicated, nonexistent, or one-sided entries are invalid.
- definitionEvery actually declared source route must have exactly one independently reviewed predecessor row. Correct rows for a selected subset are insufficient.
- definitionThe declared main conclusion must be exposed by at least one public route output, rather than existing only as an unexported source-map claim.
- definition
- definition
- definitionTwo finite lists describe the same dependency set. Duplicate expected entries are rejected so a ledger cannot pass by repeating a label.
- definitionEvery paper-level, claim-level, and step-level source reference is present and has a nonempty work and locator. PaperArgument.auditable separately checks that every claim and step carries at least one source.
- definitionA source reference is usable for review only when both the work and its locator are nonempty.
- definitionStatic fidelity checks that can be evaluated from a paper's source map alone. They do not assert the truth of any physical premise.
- definitionEvery declared output of a named source route holds under the semantic interpretation. This is the proof obligation discharged by paper-specific Lean theorems.
- definition
- definitionA route is fully certified only when both its individual steps and its declared outputs are semantically checked.
- definitionEvery source-mapped inference step in a named route is semantically sound.
- definition
- definition
- definition
- definition
- definition
- definitionThe source-mapped route with the requested identifier, when present.
- definition
- definitionThe public semantic interface inherited from predecessor routes. Descendants receive only declared route outputs, not every internal intermediate claim. Outputs still carrying a temporary reductio origin are excluded.
- definitionAll direct and inherited route dependencies. The route-order check separately ensures that the declared graph is acyclic and topologically ordered.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionEquation (22) turns the structured averaged estimate into a selected gap.
- definitionThe 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.
- definitionEquations (18)-(21) are the deferred averaged-setting calculation.
- definitionThe two angular averages introduced before equation (16), using one selected finite window for both the local and quantum correlations.
- definitionAngular averaging is introduced from the local and quantum correlations, with the common positive window retained in the resulting proposition.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe 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.
- definitionBefore locality is imposed, deterministic bipartite responses and the normalized hidden-state distribution define the model correlation.
- definitionThe temporal displacement after a boost of velocity `velocity`, with the positive Lorentz factor omitted because it does not change temporal order.
- definitionThe directed influence has the same causal order in every inertial frame.
- definitionThe correlation requirement retained from the source's broader demand to preserve statistical predictions. It does not assert the full joint law.
- definition
- definition
- definitionA finite-speed influence can reach a remote apparatus after positive elapsed time without reaching it at the emission time.
- definitionTotal functions on an empty hidden-state domain carry no physical value.
- definition
- definitionUniversal functions over no magnet settings provide no predictions.
- definitionOne fixed magnet setting cannot encode Bell's alternative local choices.
- definitionThe normalized deterministic supplement reproduces the quantum correlation function. This necessary part of full statistics does not constrain marginals.
- definitionA remote setting has physical outcome-level influence when changing it while holding the local setting and hidden state fixed changes the opposite result.
- definitionThe EPR inference is represented independently of the later inequality.
- definitionThe 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.
- definitionFor every chosen remote component, its same-component procedure predicts the result with certainty.
- definitionFor every chosen remote component, the same-component procedure leaves that remote component undisturbed in Bell's separated experiment.
- definitionThe technical local-model result derived in Bell's section IV.
- definitionThe separated Stern-Gerlach arrangement includes an implementable same-component procedure for every selected spin direction.
- definitionFactoring a bipartite hidden-variable average through local response functions converts it into Bell's equation (2).
- definitionThe proposed fast-setting experiment tests the limited-validity escape.
- definitionLocal models approximate the quantum correlation arbitrarily accurately.
- definitionBell's averaged-setting result supplies a positive uniform error gap.
- definitionExact local hidden-variable reproduction of the quantum correlation.
- definitionA model's represented correlation has Bell's local form, equation (2).
- definitionThe full singlet correlation can be represented if nonlocal dependence is allowed.
- definitionEquation (13) holds for one local representation of the model.
- definitionA local model exists for Bell's restricted bipartite correlations.
- definitionBell's section III single-particle hidden-variable illustration exists.
- definitionEquation (14) holds for one local representation of the model.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionHidden-variable accounts as such remain possible in the paper's examples.
- definitionThe two-dimensional reduction obstructs separable predetermination.
- definitionThe four-dimensional no-go transports through the Bell subscenario.
- definitionBell's explicit assumption that complete Hermitian operators are observable.
- definitionAt least one state contains the two-dimensional Bell construction.
- definitionBell's observability assumption exposes an admissible two-state sector.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe influence connects simultaneous but spatially distinct events.
- definitionA subluminal boost in units where the speed of light is one.
- definitionA model is local when its normalized hidden-state account has local form.
- definition
- definitionBell 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.
- definitionBell's limited-validity alternative for rapidly changed settings.
- definitionEquation (2) is formed from the local responses and normalized distribution.
- definitionThe unrestricted bipartite responses factor through Bell-local response functions: the left result is independent of the right setting and conversely.
- definitionA Lorentz-invariant directed causal mechanism must preserve the direction of the required remote influence in every inertial frame.
- definitionEvery spin component in Bell's EPR argument has an available same-component measurement procedure on the opposite wing.
- definitionDistant-setting dependence recovers the full singlet correlation.
- definitionBell's operational locality premise supplies the no-disturbance half of the EPR criterion for every matching remote-spin procedure.
- definitionBell's eq. (14): opposite responses rewrite the local correlation.
- definitionBell's original equation (22), after his three directions are inserted.
- definitionA chosen positive window/error pair lies strictly below Bell's bound.
- definitionBell's eq. (13): perfect anticorrelation forces opposite responses.
- definitionPerfect singlet anticorrelation licenses prediction of the remote result only when the matching measurement procedure is operationally available.
- definitionPredetermined responses plus the wavefunction's failure to determine individual results require a more complete state specification.
- definitionBell's predetermined responses require an actual complete-state value and genuinely alternative magnet settings, not functions on an empty domain.
- definitionThe singlet prediction has perfect anticorrelation at equal settings.
- definitionBell's singlet prediction `P(a,b) = -a dot b`, equation (3).
- definitionThe quantum spin calculation supplies a violating triple for equation (15). Its exact input is the represented singlet correlation formula.
- definitionA model reproduces every quantum correlation in the scenario.
- definitionThe outcome functions have only Bell's two values, `+1` and `-1`.
- definitionThe response representation has exactly Bell's local functional form: each wing receives only its own setting and the shared hidden state.
- definitionBell's restricted bipartite construction from the local correlation form.
- definitionBell's original inequality, eq. (15).
- definitionThe three examples delimiting the theorem are represented separately.
- definitionBell's chosen positive error and window violate equation (22), while every local model approximating the singlet at that error would have to satisfy it.
- definitionThe 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.
- definitionFor measurements arranged at spacelike separation, the distant-setting influence required by the completion is instantaneous in some frame.
- definitionEquation (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.
- definitionThe algebraic integration of eq. (14) gives Bell's eq. (15).
- definitionThe unresolved sign boundary in equation (4) has zero probability.
- definitionThe hemisphere average evaluated in Bell's equation (5).
- definitionThe physical geometry of Bell's pure spin state and the two angles used in equations (5)-(7).
- definitionBell's rotated-direction calibration, equation (6).
- definitionBell's hidden direction has the uniform law on the selected hemisphere.
- definitionThe positive unit hemisphere selected by the pure-state polarization.
- definitionThe final single-spin quantum expectation, equation (7).
- definitionEquation (4), away from the zero-dot-product boundary whose probability Bell sets aside separately.
- definitionAll source-level clauses of Bell's section-III single-spin construction.
- definitionThe imported spherical-average calculation: the uniform hemisphere law, sign rule, and zero-weight boundary imply equation (5).
- definitionSpecializing the singlet formula to equal settings gives anticorrelation.
- definitionThe tentative limited-validity alternative motivates the in-flight setting-change test; it is not inferred from Lorentz failure.
- definitionA correlation violates Bell's original inequality for some three settings.
- definition
- definition
- definition
- definition
- definitionRaw 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.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionBell's error scales have physically positive real magnitude.
- definition
- definition
- definitionBell's exact proof-free shared model for the selected singlet route.
- definitionThe deterministic paper-local response functions induce the generic joint possibility relation used by the paradigm layer.
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe numerical value of Bell's single-spin sign response.
- definition
- definitionBell'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).
- definitionThe 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.
- definitionBell'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.
- definition
- definitionInterpret the exact common-law argument by actual real spin readouts and one measure without a setting argument. The template's response data are retained. Its approximation, single-particle, experiment and spacetime semantics are unchanged, not claimed to be instantiated by this exact-argument adapter. Measurability belongs to the domains of the represented averages, not to all hidden-state functions. No normalization proof is stored in the data.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionPredetermined bipartite responses before locality is imposed. Each wing may depend on both apparatus settings and the shared hidden state.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionSix equally weighted opposite-spin product states realize the isotropic mixture.
- definition
- definition
- definition
- definition
- definitionOne measure, with no setting argument; totalized integrals are not assumed globally linear.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionBell-local predetermined responses `A(a, lambda)` and `B(b, lambda)`.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionBell's settings with `a·c=0` and `a·b=b·c=1/sqrt(2)`.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe remote-prediction route is evaluated after the pair is separated.
- definitionBell's selected two-particle spin singlet.
- definition
- definitionA substantive screening claim supplies an actual common-cause value.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionPossibility-level no-signalling: whether a local outcome can occur does not depend on the distant setting. This is weaker than factorization.
- definitionAt fixed settings and hidden state, a factorized support is a Cartesian rectangle: two allowed opposite corners force each crossed corner.
- definitionEvery pair of settings admits at least one joint outcome.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA model-to-world interpretation law. It does not assert that the model has produced a conclusion; use `GroundedModelConclusionAt` for that.
- definitionA model-to-theory interpretation law. It does not assert that the model has produced a conclusion; use `GroundedModelConclusionAt` for that.
- definition
- definition
- definition
- definition
- definition
- definitionBuild the epistemic dependency basis in paper order. A conclusion inherits the justification origin of its own step and every origin already attached to its premises.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionExpand a set of route identifiers by one dependency edge, iterated with enough fuel to traverse any acyclic graph on the declared routes.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
Selected instances and coercions
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
Source mappings and interpretation choices
- checked statement
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- structure
- definition
- instance
- definition
- definition
- constructor
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- recursor
- definition
- definition
- structure
- definition
- definition
- instance
- definition
- definition
- definition
- constructor
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- definition
- recursor
- definition
- definition
- definition
- structure
- definition
- definition
- instance
- definition
- definition
- definition
- definition
- definition
- constructor
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- definition
- definition
- recursor
- definition
- definition
- definition
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- definitionSource-ordered prerequisites of Bell's exact 1964 contradiction.
- checked statementEach Bell route remains an explicit premise. The EPR route is scoped to its locality hypothesis, rather than asserted alongside its eventual refutation. This scoped certificate is not an unconditional certificate of all route outputs.
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- definitionThe physical Lorentz conclusion explicitly inherits the exact no-go.
- checked statementIntegral-level readback of equations (1)-(3) and the exact common-law exclusion.
- definitionThe separate approximation route has its own discharged supposition.
- definition
- checked statement
- checked statement
- inductive
- definition
- instance
- definition
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- inductive
- definition
- instance
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- definition
- inductive
- definition
- instance
- definition
- definition
- definition
- definition
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- structure
- definition
- instance
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statementThe source's exact route follows from the explicit integral interpretation and normalization. Equation (13), equation (14), the restricted averaging laws and the quantum violation are derived, not theorem inputs. No reproducing local-model certificate is assumed.
- checked statementThe original physical interpretation still needs the actual experiment and its stronger instantaneous/Lorentz-direction bridges. Integral definitions and local-average conversion are now derived from response measurability.
- definition
- definition
- checked statementBell's EPR setup is hypothetical under locality. Its reproducing local candidate is not a certified predecessor fact after the exact no-go.
- checked statement
- checked statementBell's exact-contradiction source route is realized by the primary eqs. (13)-(15) theorem chain and the quantum violation. The inequality is scoped to a normalized reproducing local candidate. The global no-go quantifies over proposed representations; it does not consume an actual EPR candidate.
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- definition
- checked statementBell's higher-dimensional reduction is realized conditionally.
- checked statement
- definition
- definition
- definition
- definition
- checked statement
- checked statementBell's final caveat is an independent epistemic route: the paper treats limited validity as conceivable, then proposes a fast-setting test of that alternative. The route does not consume the Lorentz-failure certificate.
- definition
- constructor
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- definition
- definition
- checked statementBell's final physical route is conditional on the no-go result and the paper's explicit physical bridge principles. It ends at conditional Lorentz failure; Bell's limited-validity alternative is certified separately below.
- checked statement
- checked statement
- definition
- recursor
- definition
- definition
- checked statementBell's averaged-setting route is realized by its positive error gap.
- checked statementThe EPR route stays under its locality hypothesis; later outputs do not require an actual reproducing local candidate from that hypothesis.
- checked statementBell's three examples formally delimit the scope of the no-go theorem.
- checked statement
- checked statement
- definition
- definition
- checked statementBell's section-III single-spin construction is realized by its own source route, rather than being compressed into an existential label.
- definition
- definition
- definition
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- checked statement
- definition
- definition
- checked statement
- definition
- instance
- definition
- checked statement
- checked statement
- checked statement
- definition
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- checked statement
- definition
- checked statementBell's final paragraph offers limited validity as a conceivable alternative to the preceding conditional conclusion. It is not licensed by failure of Lorentz invariance, and the fast-setting proposal belongs to the same independent experimental route.
- checked statement
- checked statement
- checked statement
- definition
- checked statement
- definition
- checked statement
- definition
- checked statement
- definition
- checked statement
- checked statement
- definition
- definition
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- definition
- definition
Checked statements: parameters, hypotheses, and interpretation
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementAn 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.
- checked statementPositive scales need not satisfy Bell's printed equation-(22) bound.
- checked statementThe 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.
- checked statementEquation (6) alone cannot supply equation (7): the hemisphere-average calculation remains a logically active input.
- checked statement
- checked statementTreating Bell's limited-validity escape as tentative does not assert that the quantum predictions actually fail during flight.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementCorrelation-function equality transfers any equal-setting anticorrelation predicate.
- checked statementThe typed complete-state source reconstructs the raw shared factorization route instead of storing a completed shared response endpoint.
- checked statement
- checked statement
- checked statementOne 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.
- checked statement
- checked statementBell'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.
- checked statementSections 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.
- checked statement
- checked statementOne explicitly chosen spin component inhabits Bell's exact prepared and separated setup before perfect anticorrelation or either prediction bridge is used.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementAn explicit Bell-local response representation realizes the complete shared deterministic-local-response result, including generic factorization at every hidden state.
- checked statement
- checked statementBell'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.
- checked statementSection 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.
- checked statement
- checked statementBell's singlet prediction model discards EPR's optional admissibility assignment before any source-specific predetermination inference.
- checked statementBell's original section-II bridges compose two distinct shared technical results: an actual remote prediction and an actual local hidden-state model.
- checked statementThe stronger all-function laws imply the restricted laws. The converse is not assumed; a general probability integral is used only on its integrable domain.
- checked statementBell's complete-state derivation realizes the source-sensitive shared explanation without consuming an established response wrapper.
- checked statementMeasurability is the only extra domain input for the canonical bipartite integral.
- checked statementLocal factorization converts the very same bipartite integral into equation (2).
- checked statementEquation (14) follows on each setting's own almost-everywhere opposition set.
- checked statementEquation (13) is derived from positivity, normalization and the two bounded readouts.
- checked statementThe actual integral supplies the required restricted-domain average, not an opaque bridge.
- checked statement
- checked statementUnit directions and equation (3) give the same-setting minimum.
- checked statementBell's three actual unit directions violate equation (15).
- checked statement
- checked statementRemoving the binary-range conjunct loses no condition: the response codomain already supplies it. The older source clauses remain explicitly recoverable.
- checked statementThe response calculation grounded below is exactly the candidate's unrestricted responses together with Bell's proposed local equation-(1) functions.
- checked statementA deterministic supplement with no distant-setting influence would factor into Bell-local responses and hence be a local hidden-variable model.
- checked statementFor dichotomic response values, Bell's pointwise algebra reduces the difference of two products to the nonnegative `1 - B(b)B(c)` term.
- checked statement
- checked statementBell's explicit candidate-realization bridge converts the physically inhabited EPR assignment into the established shared local-response result.
- checked statementThe same source-specific inference supplies an actual hidden state, distinct settings, local support screening, and no-signalling support.
- checked statementSection II discusses an actual complete state and alternative choices of spin component; its predetermination inference cannot be empty-domain logic.
- checked statement
- checked statement
- checked statementIf a deterministic supplement reproduces the quantum correlations, Bell's no-go forces that supplement outside the local class.
- checked statement
- checked statementA fast-setting experiment that confirms the quantum predictions removes Bell's limited-validity escape for that experimental regime.
- checked statement
- checked statement
- checked statementBell's section V reduction produces an incompatible higher-dimensional state.
- checked statement
- checked statement
- checked statementAn instantaneous influence across nonzero spatial separation reverses temporal order in an admissibly boosted inertial frame.
- checked statement
- checked statementBell'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.
- checked statementBell's operational prediction step consumes both singlet anticorrelation and availability of the matching measurement procedure.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementBell's positive approximation gap excludes arbitrary local accuracy.
- checked statementBell'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.
- checked statementThe checked exact no-go conclusion of Bell's 1964 section IV.
- checked statementThe exact no-go with Bell's eqs. (13), (14), and (15) exposed rather than compressed into a single local-bound hypothesis.
- checked statementThe nonlocal illustration reproduces the full singlet correlation, while the no-go theorem excludes only its membership in the local class.
- checked statement
- checked statement
- checked statement
- checked statementThe named Bell model retains the full paper-local semantics of matching measurements, perfect anticorrelation, preparation, and operational locality.
- checked statementThe 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.
- checked statementAny paper-local realization of equation (14) by a normalized positive linear average therefore supplies equation (15); no separate inequality calculation is needed.
- checked statementBell's final conditional Lorentz conclusion.
- checked statementA reproducing deterministic completion requires distant-setting dependence.
- checked statementFor separated measurements, the required influence is instantaneous.
- checked statementBell's original eq. (13) to eq. (15) derivation for a reproducing model.
- checked statement
- checked statementBell's three examples show that hidden variables as such are not excluded.
- checked statementThe selected no-go result retains both positive scales and Bell's bound.
- checked statementA selected equation-(22) gap supplies the existential gap used below.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementNormalization 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.
- checked statement
- checked statement
- checked statement
- checked statementBell's equation (15) follows from equation (14) and averaging laws on just the response expressions used in the calculation.
- checked statementEquations (5) and (6) alone compose to Bell's equation (7).
- checked statementThe source-level section-III clauses exhibit a complete single-spin account.
- checked statementEquations (5) and (6) imply equation (7), with the spherical integral kept as an explicit imported calculation.
- checked statementBell's own setting geometry gives a concrete violation of the original three-setting inequality for `P(a,b) = -a dot b`.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementEquation (15) uses left responses at three settings and opposition at only `b,c`.
- checked statement
- checked statementThe universal inequality is derived, not a prerequisite of the finite contradiction.
- checked statement
- checked statementEquation (14) needs opposition only at the selected right setting.
- checked statementThe all-setting API follows from the selected-setting statement.
- checked statementEquation (13) requires measurability only at this one setting.
- checked statementThe exact argument's physical reading (p. 196 and section VI): with one setting-independent law, the five singlet correlations force a deterministic response to depend on the distant setting. Only five actually used readouts need measurability. The conclusion is fixed-hidden-state dependence, not an operational signal, an influence speed, or Lorentz noninvariance.
- checked statementThe complete exact contradiction needs five correlations at Bell's three directions. Neither the right response at `a` nor any response at another direction needs measurability. Opposition is derived separately at `b,c`, with their own null sets. The directions are Bell's p. 199 geometry, used to violate equation (15).
- checked statementThe abstract averaging laws follow on the measurable, bounded response domain.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementBell's complete exact exclusion with its physical conditions exposed using standard mathematical objects: unit magnet directions, two local binary spin readouts, and one normalized law independent of the settings. It excludes the singlet correlations, not a claim about signalling, influence speed or frames.
- checked statementFull singlet joint statistics imply the forbidden correlation; the converse requires the two zero marginal means exposed in the scalar characterization.
- checked statementBinary labels contain exactly the same readout information as the scalar range restriction.
- checked statementEquation (14) and its response-domain laws use the same actual probability integral.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementBell's original section-III equation (11), not a modern replacement inequality.
- checked statementThe target four probabilities are the Born traces of the explicitly written unit-direction binary spin operators, not freely assigned correlation labels.
- checked statement
- checked statementThe actual singlet has zero single-wing spin means in every direction.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe finite mixture is rotationally isotropic at the density-operator level.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe extremal equal-setting correlation fixes the two selected readouts almost everywhere.
- checked statementA binary joint law also depends on both single-wing means, not just their product mean.
- checked statement
- checked statement
- checked statementThe complete exact contradiction, expressed without project-specific semantic wrappers.
- checked statementBell's exact three-setting bound on the same five scalar readouts.
- checked statementFor binary readouts, the unbiased joint law is equivalent to two zero marginals together with the specified correlation. This is a representation identity, not the claim that correlation agreement supplies the marginals.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe old all-function subtraction requirement fails whenever the probability space admits a nonintegrable function. Totalization assigns zero to both divergent integrals.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
Axioms and trust boundaries
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
Constructors, projections, and other meaning dependencies
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- recursor
External mathematical declarations
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
Every physical statement,
dependency, equation, epistemic qualifier, and source locator in this
edition is taken only from Bell1964.lean,
Bell1964/SourceMap.lean, and
Bell1964/Coverage.lean. This is Bell's original 1964
three-setting argument; it is not silently replaced by CHSH.
The formal argument has one foundation, two no-go branches, three qualified consequences, and one independent alternative
The EPR route describes a hypothetical local completion and its quantum target under the locality hypothesis. One branch refutes exact local representation and a second excludes arbitrarily accurate local approximation. Neither consumes an actual reproducing local candidate after that hypothesis has been discharged. The exact no-go then supports three further routes: examples delimiting what the theorem does not exclude, a higher-dimensional transport under an observability assumption, and a conditional account of remote influence, Lorentz incompatibility. Bell's final limited-validity paragraph is a separate tentative experimental alternative rather than a descendant of that Lorentz conclusion.
| Transition | Status | Retained qualification |
|---|---|---|
| Perfect singlet anticorrelation | imported quantum result | Operational predictability also requires an available matching measurement. |
| Remote-orientation independence | physical locality principle | It is a premise, not a consequence of anticorrelation. |
| EPR predetermination and model realization | paper derivation plus explicit bridge | Abstract predetermined values must be tied to the candidate model's responses. |
| Bell inequality | checked algebra | Uses a normalized positive average, not normalization and linearity alone. |
| Quantum violation | deferred comparison with imported singlet law | A concrete direction triple is also proved in Lean. |
| Robust gap | route-local reductio and deferred estimates | The temporary approximation hypothesis is discharged. |
| Physical consequence | conditional derivation | Instantaneity and Lorentz failure require separate spacelike and causal premises. |
| Limited-validity alternative | tentative interpretation | Considered possible but not established; independent of Lorentz failure. |
Perfect anticorrelation becomes predetermination only through an operational route
The experiment contains two separated spin-one-half particles in a singlet state. For every chosen spin direction on the remote particle, the same component can be measured on the opposite particle. Equal settings give opposite outcomes. The matching operation and perfect anticorrelation together make the remote result predictable in advance; operational locality says that carrying out the first measurement does not disturb the remote result.
certain prediction + remote non-disturbance ⟹ predetermined result for every chosen component. Bell's EPR inference; prediction and non-disturbance are separate operational bridges (1)
The wavefunction does not determine an individual result. Combining that limitation with predetermined responses licenses the possibility of a more complete state description. Its hidden parameter λ may be a single variable, a collection, or even a collection of functions. The response values are dichotomic.
An explicit realization premise identifies these response functions with the outcomes inferred to be predetermined. The locality premise then restricts the left response to (a,λ) and the right response to (b,λ); neither may depend on the distant setting. This realization step is logically independent of merely asserting that some predetermined values exist.
The formal theorems separately derive availability of matching measurements, remote predictability, remote non-disturbance, EPR-predetermined responses, the need for a more complete state, and local dependence of a candidate model realizing those responses.
matching_measurement_and_anticorrelation_give_predictability, epr_requires_more_complete_state_specification, and epr_predetermination_realized_by_candidate_model_is_local · §II, pp. 195–196
Shared remote-correlation grounding
toRemoteCorrelationPredictionContext keeps the separated
experiment, matching procedure, perfect correlation, certain readout,
and non-disturbance bridges distinct. Its selected experiment records
two spin-one-half particles with total spin zero, and its stage type
distinguishes common preparation from separated measurement; every
route relation is scoped to those exact indices.
bell_inputs_realize_selected_remote_correlation_setup
additionally takes an explicit spin component, establishing the exact
inhabited setup before perfect anticorrelation or either bridge is used.
Grounding consumes that setup, not the correlation output, and connects
the model to the singlet description and separated-pair world before
grounded_bell_remote_prediction_transfers_every_shared_claim
transfers its claims.
The candidate completion is required to reproduce a specific quantum correlation
A normalized distribution over λ defines the local hidden-variable correlation. Normalization is its own premise; it is not inferred from the generality of λ. The model must reproduce every correlation of the quantum singlet target exactly.
The EPR formulation route packages the separated experiment, matching measurement, locality premise, arbitrary λ, binary responses, normalized distribution, predetermined outcomes, response-realization bridge, local dependence, local correlation form, singlet law, and exact statistical-agreement requirement. None of those ingredients is supplied retrospectively by the inequality. Its certificate is explicitly conditional on locality. Later no-go and physical routes do not take that actual local-candidate certificate as a premise.
The formalization also realizes the local responses in a shared deterministic-response framework. The established result records a nonempty hidden-state domain, distinct settings, factorization, total support, and no-signalling, while a theorem reconstructs the route; an explicitly supplied λ, setting pair, and distinct alternative setting yield a nonvacuous fixed-state exercise with witnessed common-cause support screening, without asserting probabilistic conditional independence. The raw factorization route and nontrivial domain also realize an ordinary structural explanation. A source-sensitive refinement retains Bell's complete-state, dichotomic, normalized hidden-variable premise rather than reconstructing it from the completed response result. A named selected-setup theorem requires that nontrivial domain before separate theory/model/world grounding transfers every shared claim.
bell_local_responses_realize_structural_deterministic_local_response_explanation · bell_deterministic_local_response_source_derivation_makes_shared_route_applicable · bell_source_inputs_realize_source_structural_deterministic_local_response_explanation · bell_hidden_state_realizes_common_cause_support_screening · bell_local_responses_exhibit_nonvacuous_shared_factorization · bell_inputs_realize_selected_deterministic_response_setup · bell_local_response_route_establishes_theory_model_grounded_response · grounded_bell_local_response_transfers_every_shared_claim
Perfect anticorrelation reduces the local model to one response function and forces Bell's inequality
Exact agreement at equal settings transfers the quantum value −1 to the local model. With dichotomic responses and a normalized positive distribution, that minimum correlation forces the two local responses to be opposite almost everywhere. Substitution eliminates one response function.
PL(a,b) = −⟨A(a,λ)A(b,λ)⟩ρ. Bell equations (13) and (14), obtained from exact equal-setting anticorrelation (5)
For values ±1, the pointwise product difference equals the nonnegative expression (1-A(b,λ)A(c,λ)). Passing through the hidden average requires subtraction linearity, preservation of constants, and the standard absolute-value bound associated with positivity. Lean checks the algebra rather than taking the inequality as an axiom.
Dichotomic pointwise algebra, the single-response representation, subtraction linearity on the response products, normalization of the constant one, and the absolute-average bound on their differences prove equation (6) for every triple of settings. No law on all hidden-state functions is required. The actual probability integral supplies these laws for bounded measurable spin readouts.
dichotomic_response_product_difference and single_response_average_satisfies_bell_inequality · §IV, equations (12)–(15)
The complete exact no-go statement is now exposed by
no_normalized_local_binary_spin_integral_model using
standard mathematical objects alone: a hidden-state measure, unit
three-vectors, and two measurable real readout functions with values
+1 or -1. One measure is used for every pair of settings; each readout
depends only on its own magnet direction and the shared hidden state.
These conditions cannot reproduce the negative-dot-product singlet
correlation for all unit directions. The statement concerns
correlations, not the full joint distribution, signalling, or frames.
impossible: ∀ a,b ∈ S², ∫ A(a,λ) B(b,λ) dμ(λ) = -a·b.
common_law_exists_iff_explicit_local_spin_readouts
constructs the representation correspondence in both directions;
it does not identify two model classes merely by proving them empty.
In the abstract exact source route, equality-transfer and standard
order consistency are derived, reducing the supplied premise list
from nine to seven. This is a concrete removal of redundant inputs,
not a count of independent physical choices or a human approval.
The wider source interpretation and auxiliary models remain unreviewed.
withCommonProbabilityLaw connects the original abstract
correlation predicates to explicit integrals, real spin values and
unit directions. The concrete exact source-route certificate derives
opposition, the single-response rewrite, the averaging laws and the
quantum violation from the measure's normalization, rather than
accepting those intermediate principles as inputs. Measurability is
explicit in the represented averages' domains. Other experiment,
approximation and spacetime fields remain inherited and unreviewed;
the stronger instantaneous/Lorentz interpretation still needs its
separate physical bridges. This is not a semantic approval of the
adapter or the whole paper.
What the correlation does not specify
For two binary readouts, the joint probabilities depend on both single-wing means as well as the correlation. The kernel-checked characterization uses the actual measure of each joint event:
r,s ∈ {+1,-1}.
Singlet: E(A)=E(B)=0, E(AB)=-a·b;
hence P(A=r,B=s) = [1-rs a·b]/4.
actual_singlet_single_spin_means_are_zero and
actual_singlet_binary_spin_probabilities compute these
quantities from the existing singlet density matrix and the explicit
operators (I+rσ·a)/2 for unit directions.
no_normalized_local_binary_spin_joint_model then excludes
the full binary singlet joint law under the same local common-law
assumptions. Correlation agreement alone does not supply the two
marginal conditions.
A diagnostic makes the converse failure concrete: take one uniform hidden variable λ on [0,1], let A always equal +1, and let B equal +1 when λ≤(1-a·b)/2 and -1 otherwise. Its actual integrals reproduce every unit-direction singlet correlation, yet E(A)=1 and the singlet joint law fails. Changing a distant setting changes B throughout the open interval; this is not a local counterexample to Bell's theorem, a full quantum completion, or a nonsignalling claim. The diagnostic and the joint-law calculations clarify the formalization's scope; they are not models or additional calculations attributed to Bell's paper.
A concrete singlet violation
The Lean file defines three unit directions with (a·c=0) and (a·b=b·c=1/√2). For the singlet correlation, equation (6) would demand (1/√2≤1-1/√2), which is false.
|PQ(a,b) − PQ(a,c)| = 1/√2 > 1 − 1/√2 = 1 + PQ(b,c). explicit unit vectors and real-number inequality proved in Lean (7)
Every exact local representation would satisfy Bell's inequality; exact statistical agreement would transfer that inequality to the quantum correlation; the concrete quantum violation excludes it. Therefore no model is simultaneously Bell-local and exactly reproducing the full singlet correlation. This is the source map's main conclusion.
no_exact_local_representation_from_original_derivation · §IV, pp. 197–199
The argument also excludes arbitrary uniform approximation and transports to a higher-dimensional state
Positive approximation gap
To avoid relying on isolated settings, Bell introduces independently averaged local and quantum correlations over one selected finite angular window. The robust route temporarily supposes arbitrary uniform local accuracy, then uses an explicit selector to obtain the concrete local model and positive ε used by the deferred calculation. Equations (18)–(21) retain the transferred averaged error, bounded averaged responses, equal-setting estimate, and three-setting estimate. Bell's directions in equation (22) then produce a fixed positive error scale at which no local model approximates the singlet correlation.
¬ uniformly-approximates(PL, PQ, ε*), hence no arbitrary local accuracy. selected angular window + selected ε + averaged-estimate chain + Bell-direction lower bound; the Lean encoding does not assign a numerical value to ε* (8)
The selected equation-(22) gap becomes the existential positive approximation gap and contradicts the route-local arbitrary- accuracy hypothesis. The witness-selection bridge is explicit, the hypothesis is discharged, and the output is independent of the reductio assumption.
no_arbitrarily_accurate_local_approximation · §IV, equations (16)–(22)
Higher-dimensional extension
Section V adds an explicit physical assumption: complete Hermitian operators are observable. If a higher-dimensional scenario contains a two-dimensional Bell subscenario, the four-dimensional no-go transports through it. The conclusion is existential: at least one state is incompatible with separable predetermination, not that every state is.
The observability assumption, Bell subscenario, and transport bridge yield a state for which separable predetermination fails.
higher_dimensional_separable_predetermination_fails · §V, p. 199
Three constructions show that locality—not hidden variables alone—is excluded
Bell's section III examples delimit the exact theorem instead of serving as counterexamples to it. The first construction is now represented at its source-level resolution; the restricted bipartite and nonlocal examples remain separate deferred calculations.
<result> = 1 - 2 theta-prime/pi, 1 - 2 theta-prime/pi = cos theta implies <result> = cos theta. Bell equations (4)-(7); the spherical average is retained as an explicit imported calculation (8a)
The formal route keeps the pure-state polarization, uniform hemisphere law, rotated sign response, zero-probability boundary, hemisphere average, and rotation calibration distinct. Equations (5) and (6) then give equation (7), and only the complete chain exposes the single-spin hidden-variable account.
single_spin_average_and_rotation_calibration_reproduce_quantum_expectation · single_spin_construction_exhibits_hidden_variable_account · §III, pp. 196-197
| Scenario | What exists | What it shows |
|---|---|---|
| Single-particle spin measurements | Pure polarization, uniform hemisphere, sign response, and calibrated expectation | Hidden variables are not intrinsically impossible. |
| Selected bipartite correlations | A local hidden-variable account | Local models can reproduce restricted correlation sectors. |
| Full singlet correlation | A deterministic account with distant-setting dependence | The full target can be recovered once Bell locality is abandoned. |
Equation (11) is now computed from six equally weighted opposite-spin product density matrices. Their separable mixture gives P(a,b) = -a dot b/3, while the actual singlet projector gives P(a,b) = -a dot b. The one-particle density matrices are identical, but equal z settings give -1/3 and -1. The matrix-derived singlet correlation feeds the existing proof of the original three-setting Bell inequality violation.
actual_isotropic_product_mixture_is_equation_eleven · equal_local_states_do_not_fix_singlet_correlations · actual_density_matrix_violates_the_original_bell_inequality · certified_scope_comparison_retains_original_equation_eleven · original journal p. 197
The examples establish that some hidden-variable model exists, while the full singlet illustration plus the exact no-go exhibits a model that reproduces quantum correlations but is not local.
scope_illustrations_preserve_hidden_variable_possibility and nonlocal_singlet_illustration_identifies_locality_as_obstruction · §III, pp. 196–197
A reproducing deterministic supplement requires distant influence; the stronger spacetime conclusions are conditional
A deterministic correlation supplement has a normalized hidden distribution, a bipartite hidden-state average, and exact agreement with the quantum correlation. Dichotomic outcomes are already enforced by the binary response codomain. The duplicated range conjunct has been removed with a checked equivalence preserving the former four source conditions; the physical restriction remains. This necessary correlation component is not identified with the source's broader demand for all quantum statistics. Absence of distant-setting dependence is now proved equivalent to local response factorization; it is not a separately supplied physical principle. The abstract framework still needs its averaging-interpretation bridge to convert that factorization into Bell's local correlation form. The concrete probability theorem instead exposes the binary responses, common normalized measure and five singlet correlations directly, and derives distant-setting dependence from the scalar no-go argument.
⟹ at least one response depends on the distant analyzer setting. factorization derived; the abstract averaging interpretation remains an explicit input (9)
Distant influence alone is not yet instantaneous. The next step also assumes spacelike-separated measurements and a bridge from such a required influence to zero temporal separation with nonzero spatial separation. For an instantaneous directed influence, the boosted time difference has the sign-sensitive form below; an admissible boost reverses its temporal order. A further Lorentz criterion requires a Lorentz-invariant causal mechanism to preserve that direction in every inertial frame.
some |v| < 1 reverses the directed order + Lorentz causal-direction criterion ⟹ supplement not Lorentz invariant. positive Lorentz factor omitted because it does not change temporal order (10)
The formal chain derives distant influence, then instantaneous influence under the spacelike bridge, then temporal-order reversal, and finally Lorentz incompatibility under the causal-direction criterion. Each dependency remains visible.
reproducing_completion_requires_distant_influence, reproducing_completion_requires_instantaneous_influence, and reproducing_completion_is_not_lorentz_invariant · §VI, p. 199
The limited-validity caveat
Bell retains an escape: conceivably the quantum predictions have limited validity when settings change during particle flight. The Lean claim is therefore a tentative epistemic status of that escape, not the assertion that the predictions actually fail. It belongs to an independent route rather than following from Lorentz failure. That tentative alternative motivates a fast-setting experiment. The formal test theorem says that if such an experiment supports the quantum predictions, the limited-validity escape is excluded for that experimental regime. The 1964 route proposes the test; it does not supply its later outcome.
Experimental support plus the stated test principle contradicts the claim that quantum predictions fail during flight.
fast_setting_experiment_excludes_limited_validity_escape · §VI, p. 199
The Lean development exposes four bridges that cannot be compressed into slogans
| Shortcut | Why it fails | Formal witness |
|---|---|---|
| Equation (6) alone gives the single-spin quantum expectation. | The rotation calibration does not determine the hidden-direction average; equation (5) remains independent. | rotation_calibration_without_hemisphere_average_does_not_supply_expectation |
| Perfect anticorrelation alone gives operational predictability. | An available matching procedure and a certainty bridge are separately required. | perfect_anticorrelation_alone_does_not_supply_operational_predictability |
| Abstract predetermined responses are automatically the candidate model's responses. | A remote-setting-dependent candidate need not factor through arbitrary local functions. | predetermined_responses_do_not_realize_an_arbitrary_candidate_model |
| Normalized linear averaging is enough for Bell's inequality. | A signed average can preserve constants and subtraction while violating the absolute-value bound and the inequality. | signed_counterexample_violates_bell_inequality |
| Any distant influence is instantaneous. | A finite-speed signal can reach a remote location after positive time but not at emission. | distant_influence_does_not_by_itself_imply_instantaneous_propagation |
| Lorentz failure proves limited validity of quantum predictions. | Bell presents limited validity as a conceivable alternative, not as a consequence of the preceding conditional conclusion. | tentative_limited_validity_does_not_assert_actual_failure |
Value-level countermodel boundary
The perfect-anticorrelation witness retains an equal-setting reference correlation of minus one while one of two matching components and its certainty prediction remain unavailable. The non-implication therefore distinguishes a singlet-style correlation statement from the operational measurement and prediction bridge rather than relying on a truth-value label.
Excluded
Exact Bell-local reproduction of the full singlet correlation, arbitrary uniform local approximation, and universal separable predetermination in the stated higher-dimensional scenario.
Not excluded
Hidden variables in general, local accounts of restricted sectors, or nonlocal deterministic accounts of the full singlet correlation.
Conditional physical scope
Instantaneity requires the separated-measurement bridge; Lorentz failure requires the causal-direction criterion; the fast-setting proposal requires experimental support to close the limited-validity escape.
Linked concepts and notation
Linked terms lead to their controlling paper-local definition, theorem, or equation. Operational, probabilistic, and spacetime qualifications are retained.
Matching spin measurement
The operational procedure of measuring the same spin component on the opposite singlet particle for any chosen direction.
MatchingSpinMeasurement
Perfect anticorrelation
The imported equal-setting singlet prediction that opposite particles yield opposite dichotomic outcomes.
QuantumPerfectAnticorrelation
EPR predetermination
The inference from certain remote predictability and operational non-disturbance to predetermined local response values.
EPRPredeterminationPrinciple
Operational locality
The premise that the distant magnet orientation does not affect the local result and supplies remote non-disturbance.
OperationalLocalityGivesRemoteNonDisturbance
Local dichotomic responses
Outcome functions taking ±1 and depending only on the corresponding local setting and shared hidden state.
ResponsesUseOnlyLocalSettingAndHiddenState
Bell-local correlation
The normalized positive hidden-state average of the product of two local response functions.
HasLocalCorrelationForm
Quantum singlet correlation
The target law (P_Q(a,b)=-a·b), with perfect anticorrelation at equal settings.
singletCorrelation
Normalized positive average
A hidden-state average normalized on the constant one, preserving the selected response-product subtractions, and satisfying their absolute-value bound. These are derived for measurable spin readouts under one probability measure, not required on all hidden-state functions.
SingleResponseFormHasAverageRepresentation
Bell's original inequality
The three-setting bound |P(a,b)−P(a,c)|≤1+P(b,c), derived from the one-response form.
SatisfiesBell1964Inequality
Exact local no-go
The negation of an exact model that is both Bell-local and reproduces every quantum singlet correlation.
HasExactLocalRepresentation
Positive approximation gap
A selected positive ε forced by Bell's three directions after one finite-window averaging chain, then promoted to an error scale at which no local model approximates the quantum correlation.
SelectedApproximationGapAt and HasBellApproximationGap
Delimiting hidden-variable models
The single-particle, restricted local bipartite, and full nonlocal singlet constructions.
ScopeIllustrations
Distant-setting influence
Dependence of at least one response on the other apparatus's setting for some hidden state.
DistantSettingInfluencesRemoteOutcome
Instantaneous influence
A directed influence with zero temporal and nonzero spatial separation, obtained only through the spacelike-separation bridge.
InfluenceIsInstantaneous
Lorentz causal-direction criterion
The premise that a Lorentz-invariant directed mechanism preserves the influence's causal direction in every inertial frame.
LorentzInvariantInfluencePreservesCausalDirection
Limited-validity escape
A tentatively considered, unestablished possibility that quantum predictions fail when analyzer settings change while particles are in flight.
LimitedValidityAlternativeIsTentative
Fast-setting experiment
The proposed in-flight setting-change test that can exclude the limited-validity escape in the tested regime.
FastSettingExperimentTestsLimitedValidity
Route inventory and formal provenance
The source map declares eight routes and fifty-one semantic claims.
Coverage interprets every claim in the paper-local Bell framework and
checks each route in its appropriate hypothesis scope. Nonempty result
steps use checked ClaimsHold premise maps; later routes may
recover actual exact-exclusion or single-particle outputs from their
certificates, but never require a discharged EPR candidate. The combined
fidelity theorem preserves this distinction rather than asserting that
all route outputs are simultaneously true.
| Route | Source-route predecessors | Declared outputs | Profile |
|---|---|---|---|
| EPR formulation | — | Experiment, local responses, correlation form, singlet target, agreement requirement | definitions, quantum inputs, locality, derivations |
| Single-particle construction | — | Pure-spin geometry, hemisphere law, sign rule, equations (5)-(7), concrete account | source construction with explicit imported average |
| Exact contradiction | EPR formulation | Conditional candidate inequality, actual quantum violation, exact incompatibility | checked algebra, explicit comparison, discharged local candidate |
| Scope illustrations | Exact contradiction, single-particle construction | Restricted and nonlocal models, hidden-variable possibility, locality as obstruction | dependent constructions and interpretation |
| Robust nonapproximability | EPR formulation | No arbitrarily accurate local approximation | selected window/ε, explicit witness bridge, deferred estimates |
| Higher-dimensional generalization | Exact contradiction | Failure of universal separable predetermination | observability assumption and formal transport |
| Physical conclusion | Exact contradiction | Reproducing supplement implies distant dependence; additional spacetime bridges imply Lorentz incompatibility | conditional derivation |
| Limited-validity alternative | — | Tentative limited-validity caveat, fast-setting proposal | independent experimental alternative |
EPR route · epr_formulation_route_is_semantically_realized
Single-particle route · single_particle_construction_route_is_semantically_realized
Exact route · exact_contradiction_route_is_semantically_realized
Scope route · scope_illustrations_route_is_semantically_realized
Robust route · robust_nonapproximability_route_is_semantically_realized
Higher-dimensional route · higher_dimensional_route_is_semantically_realized
Physical route · physical_conclusion_route_is_semantically_realized
Limited-validity route · limited_validity_alternative_route_is_semantically_realized
Dependency audits
route_semantic_realization_is_exhaustive covers all eight
routes. robust_reductio_is_route_local and
robust_reductio_is_discharged_from_route_output prevent
the temporary approximation supposition from leaking into the
conclusion. The paper-local semantics also require an explicit
selector from arbitrary accuracy to the concrete local model and
ε used by equations (18)–(21).
exact_bell_inequality_is_independent_of_deferred_calculation
records that equation (15) is checked algebra. Further audits retain
matching-measurement availability, model realization, independent
probability normalization, the section-III average/calibration
chain, the separated experiment, and the causal direction criterion
as genuine dependencies. routes_have_exact_predecessor_graph,
source_contracts_are_independent_hypotheses,
result_steps_apply_exact_semantic_inputs,
dependent_steps_name_inherited_outputs, and
dependent_routes_consume_certified_predecessor_outputs
harden route composition and forbid direct certificate-to-atom
extraction; limited_validity_alternative_is_not_a_lorentz_consequence
keeps Bell's final alternative independent.
Lean-encoded bibliographic record
J. S. Bell, On the Einstein Podolsky Rosen Paradox (1964),
§§I–VI, pp. 195–200. All section, page, equation, and provenance
locators above are stored in SourceMap.lean.
TraceComplete Lean semantic identifier ledger
Reading note. The article above is the human exposition. This collapsed cross-reference records every public theorem and every constructor of the five paper-local source-map vocabularies. It introduces no additional claim; its purpose is to make semantic omissions mechanically detectable.
Primary semantic theorems before section-III refinement (59)
bell_epr_route_realizes_structural_correlation_explanationbellRemoteCorrelationDerivationObtainssinglet_inputs_realize_source_structural_remote_correlation_explanation
bell_directions_are_unitbell_directions_have_paper_dot_productsconcrete_singlet_correlation_violates_bell_1964bell_local_responses_make_factorization_route_applicablebell_local_responses_establish_deterministic_local_responsebell_local_responses_realize_every_shared_claimlocal_responses_realize_generic_factorizationbell_local_responses_have_rectangular_joint_supportbell_local_responses_realize_total_no_signalling_supportdeterministic_local_response_model_retains_paper_semanticsbell_local_response_model_inputs_establish_theory_model_groundingbell_local_response_route_establishes_theory_model_grounded_responsegrounded_bell_local_response_transfers_every_shared_claimremote_correlation_model_retains_paper_semanticsbell_inputs_realize_selected_remote_correlation_setupremote_correlation_model_retains_singlet_experiment_and_stage_datamodel_responses_are_dichotomiclocal_factorization_excludes_distant_setting_influenceepr_predeterminationmatching_measurements_available_in_experimentmatching_measurement_and_anticorrelation_give_predictabilityoperational_locality_gives_remote_non_disturbancebell_epr_inputs_make_shared_remote_correlation_route_applicablebell_epr_route_realizes_shared_remote_correlation_predictionbell_model_inputs_establish_theory_model_groundingbell_epr_route_establishes_theory_model_grounded_remote_predictiongrounded_bell_remote_prediction_transfers_every_shared_claimepr_requires_more_complete_state_specificationepr_predetermination_realized_by_candidate_model_is_localdichotomic_response_product_differencesingle_response_average_satisfies_bell_inequalityrepresented_single_response_form_satisfies_bell_inequalitysigned_counterexample_average_preserves_subtractionsigned_counterexample_average_preserves_constantssigned_counterexample_has_single_response_formsigned_counterexample_violates_bell_inequalitysigned_counterexample_fails_absolute_average_boundexact_agreement_transfers_bell_inequalityviolation_excludes_bell_inequalityreproducing_local_model_satisfies_bell_inequalityno_exact_local_representationno_exact_local_representation_from_original_derivationno_arbitrarily_accurate_local_approximationscope_illustrations_preserve_hidden_variable_possibilitynonlocal_singlet_illustration_identifies_locality_as_obstructionhigher_dimensional_separable_predetermination_failsevery_reproducing_completion_is_nonlocaldeterministic_supplement_without_distant_influence_is_localreproducing_completion_requires_distant_influencereproducing_completion_requires_instantaneous_influenceinstantaneous_influence_reverses_causal_order_in_some_inertial_framereproducing_completion_is_not_lorentz_invariantfast_setting_experiment_excludes_limited_validity_escapeperfect_anticorrelation_alone_does_not_supply_operational_predictabilitypredetermined_responses_do_not_realize_an_arbitrary_candidate_modeldistant_influence_does_not_by_itself_imply_instantaneous_propagation
Selected response setup: bell_inputs_realize_selected_deterministic_response_setup
Averaged-setting refinement (1)
selected_approximation_gap_supplies_bell_gap
Coverage theorems before section-III refinement (8)
every_source_claim_has_semanticsepr_formulation_route_is_semantically_realizedscope_illustrations_route_is_semantically_realizedexact_contradiction_route_is_semantically_realizedrobust_nonapproximability_route_is_semantically_realizedhigher_dimensional_route_is_semantically_realizedphysical_conclusion_route_is_semantically_realizedroute_semantic_realization_is_exhaustive
Source-map audit theorems before section-III refinement (12)
argument_wellFormedargument_auditableroutes_wellFormedrobust_reductio_is_route_localrobust_reductio_is_discharged_from_route_outputexact_bell_inequality_is_independent_of_deferred_calculationlocal_response_dependence_uses_epr_predetermination_and_model_realizationperfect_predictability_depends_on_matching_measurement_availabilityprobability_normalization_is_not_inferred_from_hidden_parameter_generalityinstantaneous_conclusion_depends_on_experiment_setuplorentz_conclusion_depends_on_experiment_setuplorentz_conclusion_depends_on_causal_direction_criterion
Semantic atoms before section-III refinement (41)
separatedSpinSingletExperimentequalSettingOutcomesPerfectlyAnticorrelatedsameComponentMeasurementAvailableForEveryChosenDirectiondistantMagnetOrientationDoesNotAffectLocalResultanyChosenRemoteSpinResultPredictableInAdvanceallPossibleSpinComponentResultsPredeterminedwavefunctionDoesNotDetermineIndividualResultmoreCompleteStateSpecificationPossiblehiddenParameterMayBeArbitraryCollectionoutcomeFunctionsTakeValuesPlusOrMinusOnecandidateModelRealizesEPRPredeterminedResponseseachOutcomeDependsOnlyOnLocalSettingAndHiddenStatehiddenStateDistributionNormalizedcorrelationHasLocalHiddenVariableFormEq2singletCorrelationEqualsNegativeDotProductEq3completionRetainsQuantumCorrelationPredictionhiddenVariableAccountExistshiddenVariablesAloneAreNotExcludedlocalityIsEssentialDifficultysameSettingSingletCorrelationEqualsMinusOneoppositeOutcomesAlmostEverywhereEq13correlationRewrittenUsingOneOutcomeFunctionEq14singleResponseAverageObeysNormalizedPositiveLinearitybellInequalityEq15singletCorrelationViolatesBellInequalityexactLocalHiddenVariableRepresentationExistsaveragedSettingCorrelationsIntroduceduniformlyAccurateLocalApproximationExistsaveragedApproximationEstimateEqs18To21approximationErrorLowerBoundEq22arbitrarilyCloseLocalApproximationExistseveryCompleteHermitianOperatorIsObservablehigherDimensionalSystemsContainAnalogousTwoDimensionalSubspacesseparablePredeterminationCompatibleWithAllQuantumStatesdeterministicSupplementReproducesQuantumCorrelationsdistantSettingCanInfluenceRemoteReadinginfluenceMustPropagateInstantaneouslylorentzInvariantInfluencePreservesCausalDirectionsupplementedTheoryIsLorentzInvariantquantumPredictionsMayHaveLimitedValidityfastSettingChangeExperimentIsCrucial
Claim identifiers before section-III refinement (44)
experimentSetupperfectAnticorrelationmatchingMeasurementAvailabilitylocalityHypothesisperfectPredictabilitypredeterminationInferencepredeterminedOutcomeswavefunctionIndividualLimitationmoreCompleteSpecificationhiddenParameterGeneralitybinaryOutcomeFunctionspredeterminedResponseRealizationlocalOutcomeDependencenormalizedDistributionlocalCorrelationFormsingletQuantumCorrelationstatisticalAgreementRequirementsingleParticleIllustrationrestrictedCorrelationIllustrationnonlocalCorrelationIllustrationhiddenVariablesNotExcludedlocalityEssentialsameSettingQuantumMinimumoutcomeOppositioncorrelationRewritehiddenAverageLawsbellInequalityquantumViolationexactIncompatibilityaveragedCorrelationSetupuniformApproximationHypothesisaveragedApproximationEstimateapproximationLowerBoundarbitraryCloseApproximationImpossibleobservabilityAssumptiontwoDimensionalSubspaceReductionhigherDimensionalIncompatibilitydeterministicSupplementConditionremoteInfluenceRequiredinstantaneousInfluencelorentzCausalDirectionCriterionlorentzIncompatibilitylimitedValidityCaveatfastSettingExperiment
Step identifiers before section-III refinement (44)
specifyExperimentstatePerfectAnticorrelationstateMatchingMeasurementAvailabilitystateLocalityHypothesisinferPerfectPredictabilityformulatePredeterminationInferenceinferPredeterminedOutcomesstateWavefunctionLimitationinferMoreCompleteSpecificationgeneralizeHiddenParameterdefineBinaryOutcomeFunctionsstatePredeterminedResponseRealizationencodeLocalOutcomeDependencenormalizeHiddenDistributiondefineLocalCorrelationstateSingletQuantumCorrelationrequireStatisticalAgreementconstructSingleParticleModelconstructRestrictedCorrelationModelconstructNonlocalCorrelationModeldelimitHiddenVariableNoGoidentifyLocalityAsEssentialspecializeSameSettingCorrelationinferOutcomeOppositionrewriteCorrelationstateHiddenAverageLawsderiveBellInequalityevaluateQuantumViolationconcludeExactIncompatibilityintroduceAveragedCorrelationssupposeUniformApproximationderiveAveragedEstimatederiveApproximationLowerBoundconcludeNonapproximabilitystateObservabilityAssumptionreduceToTwoDimensionalSubspacesgeneralizeIncompatibilitystateDeterministicSupplementConditioninferRemoteInfluenceinferInstantaneousInfluencestateLorentzCausalDirectionCriterioninferLorentzIncompatibilityrecordLimitedValidityCaveatidentifyFastSettingExperiment
Route identifiers before section-III refinement (6)
eprFormulationscopeIllustrationsexactContradictionrobustNonapproximabilityhigherDimensionalGeneralizationphysicalConclusion
Route kinds before section-III refinement (6)
conceptualDerivationdelimitingExamplesexactNoGorobustNoGoformalExtensionconditionalPhysicalConsequence
Section-III refinement and traceability additions
Totals after refinement. 66 primary semantic theorems, 10 coverage theorems, 20 source-map audit theorems, 48 atoms, 51 claims, 51 steps, 8 routes, and 8 route kinds.
Primary theorems: single_spin_average_and_rotation_calibration_reproduce_quantum_expectationsingle_spin_hemisphere_rotation_reproduces_quantum_expectationsingle_spin_construction_exhibits_hidden_variable_accountrotation_calibration_without_hemisphere_average_does_not_supply_expectationbell_local_responses_exhibit_nonvacuous_shared_factorizationbell_epr_route_exhibits_nonvacuous_shared_remote_correlation
Coverage: single_particle_construction_route_is_semantically_realized
Source-map audits: single_particle_expectation_uses_average_and_rotation_calibrationsingle_particle_account_retains_source_construction
Atoms: singleParticlePureSpinGeometrysingleParticleUniformHemisphereLawsingleParticleRotatedSignResponseEq4singleParticleBoundaryHasZeroWeightsingleParticleHemisphereAverageEq5singleParticleRotationCalibrationEq6singleParticleQuantumExpectationEq7
Claims: singleParticlePureStateGeometrysingleParticleHemisphereLawsingleParticleSignResponsesingleParticleZeroBoundarysingleParticleAveragesingleParticleRotationCalibrationsingleParticleExpectation
Steps: stateSingleParticlePureStateGeometrystateSingleParticleHemisphereLawdefineSingleParticleSignResponserecordSingleParticleZeroBoundarycalculateSingleParticleAveragecalibrateSingleParticleRotationderiveSingleParticleExpectation
Route: singleParticleConstructionKind: constructiveExample
Final-paragraph epistemic and route-composition refinement
Primary theorems: tentative_limited_validity_retains_possibility_and_nonestablishmenttentative_limited_validity_does_not_assert_actual_failure
Coverage: limited_validity_alternative_route_is_semantically_realized
Source-map audits: routes_have_exact_predecessor_graphsource_contracts_are_independent_hypothesesresult_steps_apply_exact_semantic_inputsdependent_steps_name_inherited_outputsdependent_routes_consume_certified_predecessor_outputslimited_validity_alternative_is_not_a_lorentz_consequence
Route: limitedValidityAlternativeKind: experimentalAlternative
Current checked semantic identifiers
These complete lists follow current Lean declaration order. Historical and selected explanatory lists elsewhere retain their separate scope.
Primary semantic theorems (100)
bell_directions_are_unit, bell_directions_have_paper_dot_products, singleSpinOutcomeValue_preserves_generic_encoding, single_spin_average_and_rotation_calibration_reproduce_quantum_expectation, single_spin_hemisphere_rotation_reproduces_quantum_expectation, singlet_correlation_violates_at_bell_directions, concrete_singlet_correlation_violates_bell_1964, bell_local_responses_make_factorization_route_applicable, bell_local_responses_establish_deterministic_local_response, bell_local_responses_realize_structural_deterministic_local_response_explanation, bell_local_responses_realize_every_shared_claim, local_responses_realize_generic_factorization, bell_hidden_state_realizes_common_cause_support_screening, bell_local_responses_have_rectangular_joint_support, bell_local_responses_realize_total_no_signalling_support, bell_local_responses_exhibit_nonvacuous_shared_factorization, bell_deterministic_local_response_source_derivation_makes_shared_route_applicable, bell_source_inputs_realize_source_structural_deterministic_local_response_explanation, deterministic_local_response_model_retains_paper_semantics, bell_inputs_realize_selected_deterministic_response_setup, bell_local_response_model_inputs_establish_theory_model_grounding, bell_local_response_route_establishes_theory_model_grounded_response, grounded_bell_local_response_transfers_every_shared_claim, agreement_transfers_perfect_anticorrelation, selected_approximation_gap_exposes_printed_threshold, selected_approximation_gap_supplies_bell_gap, remote_correlation_model_retains_paper_semantics, bell_remote_correlation_model_ignores_physical_admissibility, bell_inputs_realize_selected_remote_correlation_setup, remote_correlation_model_retains_singlet_experiment_and_stage_data, single_spin_construction_exhibits_hidden_variable_account, no_distant_setting_influence_iff_local_response_dependence, tentative_limited_validity_retains_possibility_and_nonestablishment, model_responses_are_dichotomic, deterministic_correlation_supplement_iff_source_conditions, local_factorization_excludes_distant_setting_influence, epr_predetermination, epr_predetermination_exposes_inhabited_state_and_distinct_settings, matching_measurements_available_in_experiment, matching_measurement_and_anticorrelation_give_predictability, operational_locality_gives_remote_non_disturbance, bell_epr_inputs_make_shared_remote_correlation_route_applicable, bell_epr_route_realizes_structural_correlation_explanation, singlet_inputs_realize_source_structural_remote_correlation_explanation, bell_epr_route_realizes_shared_remote_correlation_prediction, bell_epr_route_exhibits_nonvacuous_shared_remote_correlation, bell_model_inputs_establish_theory_model_grounding, bell_epr_route_establishes_theory_model_grounded_remote_prediction, grounded_bell_remote_prediction_transfers_every_shared_claim, epr_requires_more_complete_state_specification, epr_predetermination_realized_by_candidate_model_is_local, epr_predetermination_establishes_nonvacuous_candidate_local_response, epr_predetermination_exhibits_nonvacuous_candidate_local_response, bell_remote_prediction_and_predetermination_realize_nonvacuous_local_response, dichotomic_response_product_difference, bell_response_average_laws_of_all_function_laws, single_response_average_satisfies_bell_inequality, represented_single_response_form_satisfies_bell_inequality, signed_counterexample_average_preserves_subtraction, signed_counterexample_average_preserves_constants, signed_counterexample_has_single_response_form, signed_counterexample_violates_bell_inequality, signed_counterexample_fails_absolute_average_bound, exact_agreement_transfers_bell_inequality, violation_excludes_bell_inequality, reproducing_local_model_satisfies_bell_inequality, no_exact_local_representation, no_exact_local_representation_from_original_derivation, no_arbitrarily_accurate_local_approximation, scope_illustrations_preserve_hidden_variable_possibility, nonlocal_singlet_illustration_identifies_locality_as_obstruction, higher_dimensional_separable_predetermination_fails, every_reproducing_completion_is_nonlocal, deterministic_supplement_without_distant_influence_is_local, reproducing_completion_requires_distant_influence, reproducing_completion_requires_instantaneous_influence, instantaneous_influence_reverses_causal_order_in_some_inertial_frame, reproducing_completion_is_not_lorentz_invariant, fast_setting_experiment_excludes_limited_validity_escape, positive_scales_do_not_establish_equation_twenty_two_lower_bound, tentative_limited_validity_does_not_assert_actual_failure, rotation_calibration_without_hemisphere_average_does_not_supply_expectation, perfect_anticorrelation_alone_does_not_supply_operational_predictability, predetermined_responses_do_not_realize_an_arbitrary_candidate_model, empty_hidden_state_response_functions_do_not_establish_predetermination, empty_setting_response_functions_do_not_establish_predetermination, singleton_setting_response_functions_do_not_establish_predetermination, distant_influence_does_not_by_itself_imply_instantaneous_propagation, axisState_isDensity, isotropicMixture_admissible, isotropicState_separable, isotropicState_matrix, actual_singlet_correlation_is_equation_three, observable_traceless, identity_has_zero_spin_correlation, actual_isotropic_product_mixture_is_equation_eleven, source_equation_eleven_is_realized, isotropicState_marginals, equal_local_states_do_not_fix_singlet_correlations, actual_density_matrix_violates_the_original_bell_inequality
Coverage theorems (12)
every_source_claim_has_semantics, epr_formulation_route_is_semantically_realized, single_particle_construction_route_is_semantically_realized, scope_illustrations_route_is_semantically_realized, exact_contradiction_route_is_semantically_realized, robust_nonapproximability_route_is_semantically_realized, higher_dimensional_route_is_semantically_realized, physical_conclusion_route_is_semantically_realized, limited_validity_alternative_route_is_semantically_realized, route_semantic_realization_is_exhaustive, common_probability_law_certifies_exact_source_route, common_probability_law_certifies_physical_source_route
Source-map audit theorems (20)
argument_wellFormed, argument_auditable, routes_wellFormed, routes_have_exact_predecessor_graph, source_contracts_are_independent_hypotheses, result_steps_apply_exact_semantic_inputs, dependent_steps_name_inherited_outputs, dependent_routes_consume_certified_predecessor_outputs, limited_validity_alternative_is_not_a_lorentz_consequence, robust_reductio_is_route_local, robust_reductio_is_discharged_from_route_output, exact_bell_inequality_is_independent_of_deferred_calculation, local_response_dependence_uses_epr_predetermination_and_model_realization, perfect_predictability_depends_on_matching_measurement_availability, probability_normalization_is_not_inferred_from_hidden_parameter_generality, single_particle_expectation_uses_average_and_rotation_calibration, single_particle_account_retains_source_construction, instantaneous_conclusion_depends_on_experiment_setup, lorentz_conclusion_depends_on_experiment_setup, lorentz_conclusion_depends_on_causal_direction_criterion
Semantic atoms (49)
separatedSpinSingletExperiment, equalSettingOutcomesPerfectlyAnticorrelated, sameComponentMeasurementAvailableForEveryChosenDirection, distantMagnetOrientationDoesNotAffectLocalResult, anyChosenRemoteSpinResultPredictableInAdvance, allPossibleSpinComponentResultsPredetermined, wavefunctionDoesNotDetermineIndividualResult, moreCompleteStateSpecificationPossible, hiddenParameterMayBeArbitraryCollection, outcomeFunctionsTakeValuesPlusOrMinusOne, candidateModelRealizesEPRPredeterminedResponses, eachOutcomeDependsOnlyOnLocalSettingAndHiddenState, hiddenStateDistributionNormalized, correlationHasLocalHiddenVariableFormEq2, singletCorrelationEqualsNegativeDotProductEq3, completionRetainsQuantumCorrelationPrediction, singleParticlePureSpinGeometry, singleParticleUniformHemisphereLaw, singleParticleRotatedSignResponseEq4, singleParticleBoundaryHasZeroWeight, singleParticleHemisphereAverageEq5, singleParticleRotationCalibrationEq6, singleParticleQuantumExpectationEq7, isotropicProductMixtureCorrelationEq11, hiddenVariableAccountExists, hiddenVariablesAloneAreNotExcluded, localityIsEssentialDifficulty, sameSettingSingletCorrelationEqualsMinusOne, oppositeOutcomesAlmostEverywhereEq13, correlationRewrittenUsingOneOutcomeFunctionEq14, singleResponseAverageObeysNormalizedPositiveLinearity, bellInequalityEq15, singletCorrelationViolatesBellInequality, exactLocalHiddenVariableRepresentationExists, averagedSettingCorrelationsIntroduced, uniformlyAccurateLocalApproximationExists, averagedApproximationEstimateEqs18To21, approximationErrorLowerBoundEq22, arbitrarilyCloseLocalApproximationExists, everyCompleteHermitianOperatorIsObservable, higherDimensionalSystemsContainAnalogousTwoDimensionalSubspaces, separablePredeterminationCompatibleWithAllQuantumStates, deterministicSupplementReproducesQuantumCorrelations, distantSettingCanInfluenceRemoteReading, influenceMustPropagateInstantaneously, lorentzInvariantInfluencePreservesCausalDirection, supplementedTheoryIsLorentzInvariant, quantumPredictionsMayHaveLimitedValidity, fastSettingChangeExperimentIsCrucial
Claim identifiers (52)
experimentSetup, perfectAnticorrelation, matchingMeasurementAvailability, localityHypothesis, perfectPredictability, predeterminationInference, predeterminedOutcomes, wavefunctionIndividualLimitation, moreCompleteSpecification, hiddenParameterGenerality, binaryOutcomeFunctions, predeterminedResponseRealization, localOutcomeDependence, normalizedDistribution, localCorrelationForm, singletQuantumCorrelation, statisticalAgreementRequirement, singleParticlePureStateGeometry, singleParticleHemisphereLaw, singleParticleSignResponse, singleParticleZeroBoundary, singleParticleAverage, singleParticleRotationCalibration, singleParticleExpectation, singleParticleIllustration, restrictedCorrelationIllustration, isotropicProductMixtureComparison, nonlocalCorrelationIllustration, hiddenVariablesNotExcluded, localityEssential, sameSettingQuantumMinimum, outcomeOpposition, correlationRewrite, hiddenAverageLaws, bellInequality, quantumViolation, exactIncompatibility, averagedCorrelationSetup, uniformApproximationHypothesis, averagedApproximationEstimate, approximationLowerBound, arbitraryCloseApproximationImpossible, observabilityAssumption, twoDimensionalSubspaceReduction, higherDimensionalIncompatibility, deterministicSupplementCondition, remoteInfluenceRequired, instantaneousInfluence, lorentzCausalDirectionCriterion, lorentzIncompatibility, limitedValidityCaveat, fastSettingExperiment
Step identifiers (52)
specifyExperiment, statePerfectAnticorrelation, stateMatchingMeasurementAvailability, stateLocalityHypothesis, inferPerfectPredictability, formulatePredeterminationInference, inferPredeterminedOutcomes, stateWavefunctionLimitation, inferMoreCompleteSpecification, generalizeHiddenParameter, defineBinaryOutcomeFunctions, statePredeterminedResponseRealization, encodeLocalOutcomeDependence, normalizeHiddenDistribution, defineLocalCorrelation, stateSingletQuantumCorrelation, requireStatisticalAgreement, stateSingleParticlePureStateGeometry, stateSingleParticleHemisphereLaw, defineSingleParticleSignResponse, recordSingleParticleZeroBoundary, calculateSingleParticleAverage, calibrateSingleParticleRotation, deriveSingleParticleExpectation, constructSingleParticleModel, constructRestrictedCorrelationModel, calculateIsotropicProductMixture, constructNonlocalCorrelationModel, delimitHiddenVariableNoGo, identifyLocalityAsEssential, specializeSameSettingCorrelation, inferOutcomeOpposition, rewriteCorrelation, stateHiddenAverageLaws, deriveBellInequality, evaluateQuantumViolation, concludeExactIncompatibility, introduceAveragedCorrelations, supposeUniformApproximation, deriveAveragedEstimate, deriveApproximationLowerBound, concludeNonapproximability, stateObservabilityAssumption, reduceToTwoDimensionalSubspaces, generalizeIncompatibility, stateDeterministicSupplementCondition, inferRemoteInfluence, inferInstantaneousInfluence, stateLorentzCausalDirectionCriterion, inferLorentzIncompatibility, recordLimitedValidityCaveat, identifyFastSettingExperiment
Route identifiers (8)
eprFormulation, singleParticleConstruction, scopeIllustrations, exactContradiction, robustNonapproximability, higherDimensionalGeneralization, physicalConclusion, limitedValidityAlternative
Route kinds (8)
conceptualDerivation, constructiveExample, delimitingExamples, exactNoGo, robustNoGo, formalExtension, conditionalPhysicalConsequence, experimentalAlternative
Checked source-route details
This ledger is generated from the elaborated Lean route records. It lists direct predecessors, ordered inference steps, and exported claims. The independent fidelity audit checks every field; this ledger does not replace the physical semantics or certify every explanatory diagram.
eprFormulation
Logical kind: conceptualDerivation.
Required predecessor routes: none.
Ordered inference steps: specifyExperiment, statePerfectAnticorrelation, stateMatchingMeasurementAvailability, stateLocalityHypothesis, inferPerfectPredictability, formulatePredeterminationInference, inferPredeterminedOutcomes, stateWavefunctionLimitation, inferMoreCompleteSpecification, generalizeHiddenParameter, defineBinaryOutcomeFunctions, statePredeterminedResponseRealization, encodeLocalOutcomeDependence, normalizeHiddenDistribution, defineLocalCorrelation, stateSingletQuantumCorrelation, requireStatisticalAgreement.
Exported conclusions: experimentSetup, matchingMeasurementAvailability, localityHypothesis, hiddenParameterGenerality, binaryOutcomeFunctions, normalizedDistribution, predeterminedOutcomes, predeterminedResponseRealization, localOutcomeDependence, localCorrelationForm, singletQuantumCorrelation, statisticalAgreementRequirement.
singleParticleConstruction
Logical kind: constructiveExample.
Required predecessor routes: none.
Ordered inference steps: stateSingleParticlePureStateGeometry, stateSingleParticleHemisphereLaw, defineSingleParticleSignResponse, recordSingleParticleZeroBoundary, calculateSingleParticleAverage, calibrateSingleParticleRotation, deriveSingleParticleExpectation, constructSingleParticleModel.
Exported conclusions: singleParticlePureStateGeometry, singleParticleHemisphereLaw, singleParticleSignResponse, singleParticleZeroBoundary, singleParticleAverage, singleParticleRotationCalibration, singleParticleExpectation, singleParticleIllustration.
exactContradiction
Logical kind: exactNoGo.
Required predecessor routes: eprFormulation.
Ordered inference steps: specializeSameSettingCorrelation, inferOutcomeOpposition, rewriteCorrelation, stateHiddenAverageLaws, deriveBellInequality, evaluateQuantumViolation, concludeExactIncompatibility.
Exported conclusions: bellInequality, quantumViolation, exactIncompatibility.
scopeIllustrations
Logical kind: delimitingExamples.
Required predecessor routes: exactContradiction, singleParticleConstruction.
Ordered inference steps: constructRestrictedCorrelationModel, calculateIsotropicProductMixture, constructNonlocalCorrelationModel, delimitHiddenVariableNoGo, identifyLocalityAsEssential.
Exported conclusions: restrictedCorrelationIllustration, isotropicProductMixtureComparison, nonlocalCorrelationIllustration, hiddenVariablesNotExcluded, localityEssential.
robustNonapproximability
Logical kind: robustNoGo.
Required predecessor routes: eprFormulation.
Ordered inference steps: introduceAveragedCorrelations, supposeUniformApproximation, deriveAveragedEstimate, deriveApproximationLowerBound, concludeNonapproximability.
Exported conclusions: arbitraryCloseApproximationImpossible.
higherDimensionalGeneralization
Logical kind: formalExtension.
Required predecessor routes: exactContradiction.
Ordered inference steps: stateObservabilityAssumption, reduceToTwoDimensionalSubspaces, generalizeIncompatibility.
Exported conclusions: higherDimensionalIncompatibility.
physicalConclusion
Logical kind: conditionalPhysicalConsequence.
Required predecessor routes: exactContradiction.
Ordered inference steps: stateDeterministicSupplementCondition, inferRemoteInfluence, inferInstantaneousInfluence, stateLorentzCausalDirectionCriterion, inferLorentzIncompatibility.
Exported conclusions: remoteInfluenceRequired, lorentzIncompatibility.
limitedValidityAlternative
Logical kind: experimentalAlternative.
Required predecessor routes: none.
Ordered inference steps: recordLimitedValidityCaveat, identifyFastSettingExperiment.
Exported conclusions: limitedValidityCaveat, fastSettingExperiment.