outcome
plain-language theorem explainer
Defines the measurement outcome map: given an observer subsystem, a finite outcome space, and a full ledger configuration, return a discrete outcome index in Fin(num_outcomes). The index is the observer-local total defect, scaled by the number of bins, floored, and reduced mod the bin count. Anyone citing F-009 measurement or the deterministic-but-unpredictable claim uses this as the concrete projection. The body is a direct arithmetic construction, not a proof.
Claim. For a ledger size $N$, an observer subsystem $S$ (observer indices of cardinality $K$ with $0<K<N$), an outcome space with $m=\mathrm{num\_outcomes}\ge 1$ bins, and a configuration $c$ of $N$ positive real entries, the outcome is the residue class $$k = \bigl\lfloor D_{\mathrm{obs}}(c)\cdot m\bigr\rfloor \bmod m \in \{0,\ldots,m-1\},$$ where $D_{\mathrm{obs}}(c)=\sum_{i\in S_{\mathrm{obs}}} J(c_i)$ is the sum of defect (J-cost) over observer entries only.
background
Module F-009 formalizes how deterministic ledger dynamics can look random to an internal observer. An observer is not external: it is a Subsystem, a partition of the $N$ ledger slots into observer indices (size $K$) and complementary system indices. A Configuration is an $N$-tuple of positive reals (entry ratios). The scalar defect on an entry is the J-cost $J(x)=(x+x^{-1})/2-1$ from the forcing chain (T5 uniqueness of $J$).
OutcomeSpace packages a positive bin count $m$: the observer's finite resolution. The measurement story is that the full variational update (global, non-local) sets every entry, including the observer's, but the observer only reads its own slots. Many full states share one partial view; ignorance of the complement is the epistemic source of apparent randomness, not ontological chance. Bell-type non-locality is already attributed upstream to the global variational step, not to local hidden variables.
This definition supplies the missing concrete map from full state to discrete label that Determinism.project only gestured at.
proof idea
Definitional construction, not a tactic proof. Sum defect (i.e. $J$) over S.obs_indices to get the observer-local total defect. Multiply by space.num_outcomes, take Int.floor, convert to Nat via Int.toNat, then reduce modulo num_outcomes. The resulting pair is packaged as an element of Fin space.num_outcomes, with the bound discharged by Nat.mod_lt and space.num_pos. No lemmas beyond floor/mod arithmetic and the positivity hypothesis on the bin count.
why it matters
This is the operational heart of F-009: the explicit function that turns a full configuration into a coarse-grained outcome label using only observer-local defect. Downstream, outcome_is_determined and same_state_same_outcome record that the map is a total function of the full state; deterministic_but_unpredictable pairs that fact with the partial-view non-determination theorem to state that randomness is epistemic. The module certificate measurement_mechanism_certificate lists unique determination of outcome as clause (1) of the five structural facts resolving the measurement problem.
It also feeds MeasurementEvent, MeasurementProtocol, uncoupling predicates, and Born-adjacent weighting (lower_defect_higher_weight uses the same J-cost landscape). In framework terms it closes the gap left by Determinism: projection is no longer a slogan, it is a ledger-native coarse-graining of observer defect. It does not itself derive Born frequencies; those sit in the J-weighting layer that consumes this map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.