AreUncoupled
plain-language theorem explainer
Defines the pre-measurement uncoupled state: a subsystem partition and full ledger configuration are uncoupled when observer entries carry no forced information about the system. Anyone formalizing the three-stage measurement protocol (pre / interact / read) cites this as stage one. The body is a pure Prop definition quantifying over configurations that match on observer indices, keep system entries positive, and preserve log-charge, with a trivial conclusion.
Claim. Fix $N\in\mathbb{N}$, a subsystem partition $S$ of the $N$ ledger indices into observer and system blocks, and a positive configuration $c$. The pair $(S,c)$ is uncoupled when, for every configuration $c'$ that agrees with $c$ on every observer index, has strictly positive system-index entries, and has the same total log-charge as $c$, the (vacuous) condition $\top$ holds. Intended reading: observer entries are independently assigned from system entries before coupling.
background
Module F-009 (Measurement Mechanism) supplies the missing mechanism behind the slogan that quantum randomness is projection through finite resolution. Observers are not external: a Subsystem partitions the $N$ ledger indices into observer indices of size $K$ and complementary system indices. A Configuration is an $N$-tuple of positive real ratios (ledger entries), with total defect built from the J-cost on each entry.
The measurement protocol has three stages: (1) pre-measurement uncoupled state, (2) variational interaction that couples observer and system under a shared conservation constraint, (3) read-out by projecting the observer's post-interaction entries to a discrete outcome. The outcome map depends only on observer-index entries after the global update, so the full state determines the outcome while the observer's partial pre-view does not.
Upstream, configurations and positivity come from InitialCondition; finite-resolution observers and lossy projection sit in Determinism; global variational updates (the source of non-local correlations) sit in VariationalDynamics.
proof idea
Pure definition, not a proved theorem. The Prop is the universal quantification over configurations $c'$ that (i) match $c$ on every observer index of $S$, (ii) keep system-index entries strictly positive, and (iii) preserve total log-charge, concluding $\top$. No lemmas are applied; no tactics run. As written the predicate is inhabited for every $(S,c)$, so it currently marks the pre-measurement stage rather than enforcing a nontrivial independence constraint.
why it matters
This is stage one of the Measurement Protocol documented in the module: before the variational step, observer and system entries are treated as independently assigned. It anchors the claim that apparent randomness is ignorance of complementary ledger entries under a global conservation law, not ontic stochasticity and not Bell-local hidden variables (non-locality of the update is already proved in VariationalDynamics).
Downstream use is not yet wired in this graph (used_by is empty), but the sibling stack (MeasurementEvent, outcome, ObservationallyEquivalent, same_state_same_outcome) is the natural consumer: the interact stage should discharge uncoupling and the read stage should show that the partial observer view does not fix the outcome. In the broader RS chain this sits under foundation measurement, feeding the story that determinism plus finite internal resolution yields Born-like statistics via J-cost weighting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.