partial_view_underdetermines_outcome
plain-language theorem explainer
Distinct full ledger configurations can agree on every observer-index entry, so a subsystem observer cannot tell them apart. Anyone treating measurement as readout from a partial view cites this existence fact. The proof is a concrete four-entry witness: two positive configs match on the first two slots and differ on the complementary slots.
Claim. There exist a ledger size $N$, an observer subsystem $S$ partitioning $N$ entries, a coarse-grained outcome space, and two positive configurations $c_1,c_2$ on $N$ entries such that $c_1$ and $c_2$ agree on every observer index of $S$, yet the full entry maps of $c_1$ and $c_2$ are unequal.
background
Module F-009 (Measurement Mechanism) explains how a fully deterministic ledger trajectory can look random to an internal observer. An observer is not external: it is a subsystem of the $N$-entry ledger. A Subsystem fixes $K$ with $0<K<N$ and a set of observer indices of cardinality $K$; the complementary indices are the system entries.
A Configuration is an $N$-tuple of positive real ratios (ledger entries). Two configurations are observationally equivalent for $S$ when they agree on every observer index: the observer literally has no access to the complementary entries. An OutcomeSpace is a finite coarse-graining of the observer's post-measurement projection; the instantaneous readout depends only on observer entries, but those values themselves are set by the global variational update.
The module's key claim is that many distinct full states share one partial view. That hidden difference is what a later coupled variational step can act on, producing an outcome the observer could not have predicted from its own entries alone.
proof idea
Explicit witness, not an abstract non-constructive argument. Take $N=4$ and observer indices ${0,1}$ (so $K=2$). Supply a dummy outcome space with ten bins (only needed to inhabit the existential). Set
$c_1=(1,1,2,1/2)$ and $c_2=(1,1,10,1/10)$, both entrywise positive by finite case split and norm_num.
Observational equivalence is immediate: on indices $0$ and $1$ the entries match by construction. Inequality of full maps is the evaluation at index $2$: $2\neq 10$. The complementary pair $(2,1/2)$ versus $(10,1/10)$ is the hidden system data the observer never sees.
why it matters
This is the existence half of the module's "apparent randomness" story: the partial view underdetermines the full pre-measurement state. Together with the sibling facts that the outcome is a function of the full configuration and that equal full states give equal outcomes, it pins down where ignorance lives, namely in the complementary ledger entries, not in any stochastic collapse postulate.
It supports the F-009 program that quantum-looking randomness is projection through finite internal resolution. The full ledger is not a Bell-local hidden variable; non-local correlations come from the global variational update (VariationalDynamics). No downstream theorem currently depends on this declaration, so it is a foundational lemma waiting on the Born-rule and correlation-creation sections of the same module.
Framework link: it makes precise the measurement side of the forcing chain's deterministic ledger picture without adding extra randomness axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.