observer_view
plain-language theorem explainer
Given a subsystem partition of an N-entry ledger and a full configuration, the observer view is the restriction of the configuration to the observer's index set. Anyone formalizing internal measurement or partial-state ignorance cites this map. The definition is a one-line projection: each observer index is read from the configuration entries.
Claim. For a partition of $N$ ledger entries into an observer block of size $K$ (with $0 < K < N$) and its complement, and for a configuration $c$ with positive real entries $c_i$, the observer view is the map sending each observer index $i$ to $c_i$.
background
Module F-009 (Measurement Mechanism) turns the slogan that quantum randomness is projection through finite resolution into an explicit ledger mechanism. Observers are not external agents: they are subsystems, i.e. a choice of $K$ indices among $N$ ledger slots, with the complementary $N-K$ indices treated as the system.
A configuration is an $N$-tuple of positive real ratios (ledger entries). The total defect is the sum of J-costs on those entries; dynamics and measurement live on that full state. The observer, however, only ever sees its own coordinates.
Subsystem packages the partition: positive $K < N$, a finset obs_indices of cardinality $K$, and the complementary system indices. The observer view is the first half of the partial-view apparatus; the sibling system view does the same for the complement. Apparent randomness later arises because many full configurations share one observer restriction.
proof idea
Pure definition, not a theorem. The body is the lambda that, on a dependent pair $\langle i, h\rangle$ with $i$ in the observer index set, returns c.entries i. No lemmas are applied; it is the canonical restriction map from full configurations to functions on observer indices.
why it matters
This is the concrete "partial view" step in the module's measurement story: the full ledger state determines outcomes, but the observer only holds its own entries, so many full states are observationally equivalent. That ignorance, plus non-local variational update, is how determinism produces apparent randomness without Bell-local hidden variables.
Downstream, quadratic_near_equilibrium develops the Born-rule side (J-cost near equilibrium is quadratic in log-ratio perturbations, hence Gaussian weights). The observer view is the type-level handle that later notions (observational equivalence, measurement events, outcome maps) sit on. In the broader RS chain it supports the measurement-mechanism layer above Determinism and VariationalDynamics, not a T0–T8 forcing step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.