Subsystem
plain-language theorem explainer
A subsystem of an N-entry ledger is a proper nonempty observer block of size K together with its index set; the system is the complementary N-K entries. Every measurement construction in F-009 is parameterized by this partition. The declaration is a plain structure with positivity, strict inequality, and cardinality fields; the complement indices and their count are derived immediately.
Claim. For $N\in\mathbb{N}$, a subsystem is data $K\in\mathbb{N}$ with $0<K<N$ and a finite set $I\subset\{0,\ldots,N-1\}$ of cardinality $K$ (the observer indices). The system indices are the complement $\{0,\ldots,N-1\}\setminus I$, which has cardinality $N-K$.
background
Module F-009 (Measurement Mechanism) answers how a fully deterministic ledger trajectory can look random to an internal observer. The key modeling move is that observers are not external: they are subsets of the N ledger entries. An observer of size K sees only its own entries; the complementary N-K entries are the "system."
The structure packages exactly that partition. Field $K$ is the observer cardinality (strictly between 0 and N), obs_indices is the concrete Finset of observer slots in Fin N, and the card equality pins the size. The derived sys_indices is the set difference against the universe, so observer and system form a disjoint cover of all entries.
This sits downstream of the ledger configuration and variational-dynamics apparatus (Determinism, VariationalDynamics, LawOfExistence). It does not itself invoke the J-cost or the forcing chain; it only supplies the geometric split those later theorems quantify over.
proof idea
Definitional: five structure fields with no proof obligation beyond the stated inequalities and the card equality. The companion definition sys_indices is one line, Finset.univ \ obs_indices. The companion lemma sys_card unfolds that definition, applies Finset.card_sdiff_of_subset (observer indices sit inside the universe), then simplifies with card_univ, Fintype.card_fin, and the structure's own obs_card to obtain cardinality $N-K$.
why it matters
This is the first structural brick of F-009. Downstream, MeasurementEvent carries a subsystem : Subsystem N; AreUncoupled states pre-measurement independence relative to observer vs system indices; measurement_creates_correlation and correlation_is_permanent quantify over those index sets; deterministic_but_unpredictable and the F-009 certificate both open with "observers are subsystems" and cite this type together with the partial-view map.
Framework role: it turns the informal slogan "quantum randomness is projection through finite resolution" into a typed split of the ledger, so that outcome determination by the full state and underdetermination by the partial view become ordinary propositions. It does not yet encode Born weights or Bell nonlocality; those land in later theorems that consume this partition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.