subsystem_cannot_know_whole
plain-language theorem explainer
Any proper subsystem observer (K < N ledger entries) is informationally blind to the full configuration: two distinct positive-entry states can agree on every observer index yet differ elsewhere. Measurement and foundations work cite this as the structural source of epistemic unpredictability. The proof is a direct witness construction on a complementary system index.
Claim. For every subsystem partition $S$ of an $N$-entry ledger with observer size $K$ satisfying $0 < K < N$, there exist configurations $c_1, c_2$ (maps $\mathrm{Fin}\, N \to \mathbb{R}_{>0}$) that agree on every observer index yet have unequal full entry functions.
background
Module F-009 formalizes measurement as an internal ledger process: observers are not external agents but proper subsets of the $N$ positive real ledger entries. A Subsystem fixes observer cardinality $K$ with $0 < K < N$, an observer index set of size $K$, and complementary system indices of size $N-K$.
A configuration is an $N$-tuple of positive reals (ratios). Two configurations are observationally equivalent for $S$ when they agree on every observer index; the observer literally cannot read the complementary entries. The outcome map projects only through the observer view, yet those values themselves are fixed by the global variational state.
Upstream, outcome_is_determined records that the full configuration uniquely fixes the discrete outcome. The present result is the complementary underdetermination fact: the partial view does not pin down the full state. Together they separate ontological determinism from epistemic unpredictability inside the ledger.
proof idea
Tactic proof by explicit witnesses. From $K < N$ the complementary system index set is nonempty (empty complement would force system card $0$, contradicting $N-K > 0$). Pick any system index $j$ outside the observer set.
Build $c_1$ with every entry $1$, and $c_2$ equal to $1$ except entry $j$ equal to $2$ (positivity by case split). On observer indices, $i \neq j$, so both maps read $1$, giving observational equivalence. Equality of full entry functions would force $c_1(j)=c_2(j)$, i.e. $1=2$, contradiction. No deep lemmas beyond Finset nonempty/card and the subsystem field inequalities.
why it matters
This is the second half of the measurement-problem resolution in F-009. Downstream, deterministic_but_unpredictable packages it with outcome_is_determined: outcomes are fixed by the full state yet not fixed by the observer's partial view, so apparent randomness is epistemic (the observer is a part, not the whole), without Copenhagen collapse, many-worlds branching, or Bell-local hidden variables.
It is cited in measurement_mechanism_certificate (item: observer cannot access the full state) and feeds the UnifiedForcingChain bridge Variational_To_Measurement_Bridge / variational_to_measurement_bridge_holds, which lifts variational dynamics plus subsystem projection facts into the measurement layer. In the broader RS story it makes precise why internal observers see stochastic Born-like statistics while the ledger trajectory remains deterministic under the global variational update.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.