The framework equivalences concern a specified deterministic response model at fixed hidden state, not a probability law after averaging. They expose literal equality of response values and require no new physical definitions. The finite diagnostic uses one common fair hidden bit for all settings. Both observed marginals are uniform despite a remote-setting-dependent response at each hidden value. Its complete joint law also has a distinct local realization. Thus the example does not violate a Bell inequality or exclude a local model of the observed statistics; it prevents inference of locality of a particular hidden-state realization from those statistics. Empty domains remain possible for the universal framework laws; this Boolean diagnostic has two settings, two positive-probability hidden values and two outcome channels.
Other argumentsExamples and distinctions
Constructed examples of this model; each answer includes the Lean statement.
Exact root statement
(∀ (left right : Bool),
outcomeLaw remotePermutation fairCoin left right = outcomeLaw localRealization fairCoin left right) ∧
PhysicsLogic.Framework.DeterministicLocalResponse.AdmitsLocalFactorization localRealization ∧
¬PhysicsLogic.Framework.DeterministicLocalResponse.AdmitsLocalFactorization remotePermutation
Compare two arguments
Compare their definitions and hypotheses. Shared declarations may be instantiated
differently; differences do not establish equivalence or implication.
No comparison argument selected.
Compare an earlier extraction
Compare the displayed specifications with an earlier JSON export.
This compares text, not mathematical equivalence. Files stay in this browser.
No earlier extraction selected.
Notes and questions
Import merges local entries without overwriting them.
All declarations in the selected argument
Definitions, structures, and assumptions
Structures, classes, and inductive alternatives
structure
structure
structure
Definitions and domain choices
definition
definition
definition
definition
definition
definition
definition
definition
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
Constructors, projections, and other meaning dependencies