measurement_creates_correlation
plain-language theorem explainer
After a variational successor step, any feasible alternative that matches the post-step state on the observer's ledger indices has total J-defect at least as large as the successor. Measurement theorists in the RS ledger picture cite this to say the step encodes system information into observer entries. The proof is a one-line appeal to the minimality half of the variational-successor witness; the observer-matching hypothesis is unused.
Claim. Let $N \ge 2$, let $S$ partition the $N$ ledger indices into observer and system blocks, and let $c$, $\mathrm{next}$ be positive-ratio configurations with $\mathrm{next}$ a variational successor of $c$. Then every configuration $\mathrm{alt}$ that agrees with $\mathrm{next}$ on all observer indices and is feasible from $c$ satisfies $\sum_i J(\mathrm{next}_i) \le \sum_i J(\mathrm{alt}_i)$, where $J$ is the defect cost.
background
In F-009 (Measurement Mechanism), observers are internal subsystems of the ledger. A subsystem partitions $N$ entries into observer indices of size $K$ and complementary system indices. A configuration is an $N$-tuple of positive real ratios; total defect is the sum of per-entry defects, each equal to the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$).
The module answers what Determinism left open: which ledger data fixes the outcome an internal observer sees. The observer reads only its own entries; many full states share that partial view. Apparent randomness is ignorance of the complement under the global conservation constraint, not Bell-local hidden variables (non-locality of the variational update is proved elsewhere).
Upstream, a variational successor packages discrete dynamics: $\mathrm{next}$ is feasible from $c$ and minimizes total defect among all feasible alternatives. Feasibility is the conservation-constrained reachable set from $c$.
proof idea
Term-mode one-liner. Introduce the alternative configuration together with observer-agreement and feasibility. Drop the observer-agreement hypothesis, then apply the second component of the variational-successor witness, which already states that $\mathrm{next}$ has least total defect among every configuration feasible from $c$. The claimed inequality on the observer-matching subclass follows a fortiori.
why it matters
This is the correlation-creation step of F-009: after the variational step, observer entries encode system information, because any attempt to vary system entries while freezing observer entries cannot undercut the defect minimum. That encoding is the measurement record.
Downstream it feeds Variational_To_Measurement_Bridge in the Unified Forcing Chain, whose doc-comment lists the package: outcomes determined by the full state, partial views underdetermine, variational coupling of observer and system, defect monotonicity making correlation permanent, and positive J-cost weights maximized at the variational update. The sibling permanence result then locks the record by monotone defect decrease (decoherence). In the forcing narrative this sits on T5 J-uniqueness: the same forced $J$ supplies the defect whose minimality writes the measurement record.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.