Measurement
plain-language theorem explainer
The Measurement structure records a local observation on one particle of an EPR pair via an axis vector in R^3, a binary outcome, and a real time stamp. Quantum foundations researchers formalizing Bell tests or no-signaling results cite it when building ledger-based accounts of correlations. The declaration is a direct record type with no attached axioms or reduction steps.
Claim. A measurement consists of an axis vector $(x,y,z)inmathbb{R}^3$, an outcome $o in {+1,-1}$, and a time $t in mathbb{R}$.
background
Recognition Science treats nonlocality and no-signaling as consequences of ledger consistency: entangled particles share ledger entries so that correlations appear across space, yet a local read leaves the distant entry unchanged. Module QF-006 introduces the basic objects needed for this derivation. Upstream, Time is defined as the reals, while a sibling Measurement from data import supplies a generic experimental container with name, value, and error fields.
proof idea
The declaration is a direct record definition introducing the three fields axis, outcome, and time. No lemmas or tactics are invoked; the structure functions as a primitive type for later correlation and invariance statements.
why it matters
This record supplies the local observation object used by the no-signaling theorem and ledger_explains_nonlocality in the same module, which in turn feed LedgerComputation and KGateMeasurement. It realizes the QF-006 claim that ledger consistency produces Bell violations without faster-than-light signaling, aligning with the phi-ladder and eight-tick octave of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.