system_view
plain-language theorem explainer
Extracts the system-side ledger entries of a full N-entry configuration under a fixed observer/system partition. Anyone building partial views, observational equivalence, or measurement outcomes cites this restriction. The body is a one-line projection: map each system index to the corresponding configuration entry.
Claim. Fix $N\in\mathbb{N}$, a subsystem partition $S$ of the $N$ ledger indices (observer block of size $K$, system block the complement), and a configuration $c$ with positive real entries on $\mathrm{Fin}\,N$. The system view is the map sending each system index $i$ to $c_i\in\mathbb{R}$.
background
Module F-009 (Measurement Mechanism) explains how a fully deterministic ledger trajectory can look random to an internal observer. The key setup is a partition of the $N$ ledger entries: the observer holds a proper nonempty index set of size $K$, and the system holds the complementary indices.
A configuration is an $N$-tuple of positive reals (ledger ratios), as in InitialCondition. The subsystem structure supplies sys_indices as the set-theoretic complement of the observer indices inside Fin N. The system view is simply the restriction of the configuration to that complement; the matching observer-side restriction is the sibling partial view.
This is structural, not approximate: the observer literally has no access to system entries. Downstream material uses that fact to define observational equivalence (agreement on observer indices) and to separate full-state outcome determination from partial-view ignorance.
proof idea
Pure definition, not a proved theorem. The term is the lambda that, on a dependent pair consisting of a system index and its membership proof, returns the configuration entry at that index. No lemmas or tactics are involved.
why it matters
Fills the "partial view" slot in the F-009 measurement stack: after the subsystem partition, one needs explicit maps from full configurations to observer-only and system-only data. This is the system half; together with the observer view it underwrites observational equivalence and the claim that many full states share one observer reading.
That split is the module's answer to the gap left by Determinism: projection was lossy, but not yet tied to which ledger entries an internal observer can see. Apparent randomness is then ignorance of the complementary entries, while the full state (including nonlocal variational correlations) still fixes the measurement outcome. No downstream theorems currently depend on this def in the graph, but siblings (ObservationallyEquivalent, MeasurementEvent, outcome lemmas) sit in the same Part 2 coupling narrative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.