deterministic_but_unpredictable
plain-language theorem explainer
Measurement outcomes are uniquely fixed by the full N-entry ledger configuration, yet two configurations can agree on every observer index and still differ elsewhere. Researchers citing the RS account of apparent quantum randomness (epistemic, not ontological) would invoke this split. The proof is a two-component term: uniqueness of the outcome map paired with existence of distinct observer-indistinguishable states.
Claim. Fix a subsystem partition $S$ of an $N$-entry ledger (observer block of size $K$ with $0<K<N$) and an outcome space. Then (i) for every configuration $c$, there is a unique outcome index $k$ equal to the measurement outcome of $c$, and (ii) there exist configurations $c_1,c_2$ that agree on all observer indices yet have unequal full entry maps.
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 an observer block of size $K$ and its complement. A configuration is an $N$-tuple of positive real ratios; total defect is the sum of the J-cost (defect) on each entry.
Observational equivalence means two configurations agree on every observer index. The observer literally cannot access the complementary entries, so this is a structural indistinguishability, not an approximation. An outcome space is a finite coarse-graining of the observer's post-measurement partial view; the outcome map sends a full configuration to one of those coarse labels.
Upstream, configurations and total defect come from InitialCondition and LawOfExistence (defect equals the unique J-cost). The module sits after Determinism and VariationalDynamics: the full trajectory is deterministic and the variational update is global, so non-local correlations are already in the ledger state.
proof idea
Term-mode pair constructor. The left conjunct is discharged by applying outcome_is_determined at each configuration $c$, which supplies unique existence of the outcome label. The right conjunct is exactly subsystem_cannot_know_whole S, which produces two configurations that are observationally equivalent for $S$ yet differ as full entry maps. No further rewriting or case analysis.
why it matters
This is the hinge claim of F-009: the universe is deterministic, but the observer is a proper part, not the whole. Apparent randomness is epistemic ignorance of complementary ledger entries. The doc-comment positions it against the usual menu: no Copenhagen collapse (the full state evolves deterministically), no many-worlds branching (one trajectory), and not Bell-style local hidden variables (the "hidden" data are the system entries, already carrying non-local correlations from the global variational update).
It packages the two prior sibling facts (outcome uniqueness; existence of distinct observer-equivalent states) into the single citation surface for the measurement problem. The module's next block builds Born-rule structure via J-cost weights $\exp(-\mathrm{total_defect})$, the RS analogue of $|\psi|^2$. No downstream dependents are wired yet; the natural consumers are correlation-creation and Born-weight theorems in the same file, and any bridge from Determinism's lossy project to concrete outcome statistics. Framework landmarks: J-uniqueness (T5) underwrites the defect cost; global update non-locality (VariationalDynamics) keeps Bell-type objections off the table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.