OutcomeSpace
plain-language theorem explainer
OutcomeSpace packages a finite, nonempty set of coarse-grained measurement labels: a positive count of distinguishable outcomes. Anyone formalizing readout, Born-structure, or the F-009 measurement certificate cites it as the codomain parameter for the outcome map. It is a bare data structure (cardinality plus positivity), not a derived theorem.
Claim. An outcome space is a pair $(n, h)$ where $n \in \mathbb{N}$ is the number of coarse-grained measurement labels and $h$ asserts $0 < n$. Equivalently: a nonempty finite discrete set of observer-resolvable outcomes.
background
Module F-009 (Measurement Mechanism) explains how a fully deterministic ledger trajectory can look random to an internal observer. Observers are subsystems: $K < N$ ledger entries, not external agents. A measurement couples observer and system via a variational step; the observer then reads only its own post-interaction entries.
The full configuration determines the readout, but many full states share the same observer partial view. Apparent randomness is epistemic ignorance of the complementary entries, not ontological chance. Bell-type nonlocality is already carried by the global variational update, so this is not a local hidden-variable story.
OutcomeSpace is the discrete label set for that readout. The companion map outcome sums defects on observer indices, scales by the number of bins, floors, and reduces modulo $n$, landing in $\mathrm{Fin}, n$. Positivity of $n$ makes the modular reduction well-typed.
proof idea
No proof body: this is a structure declaration. It records two fields only, the natural number of outcomes and a proof that the count is strictly positive. Downstream definitions (the outcome projection into $\mathrm{Fin},\mathrm{num_outcomes}$) and uniqueness lemmas consume those fields directly; nothing is derived here beyond the type former.
why it matters
This is the codomain parameter for the entire measurement layer. It appears in MeasurementProtocol (pre/interact/read stages), in the outcome map, and in the uniqueness and same-state lemmas that say the full configuration fixes a unique label. The headline theorems deterministic_but_unpredictable and measurement_mechanism_certificate both quantify over an OutcomeSpace when they split "determined by the full state" from "underdetermined by the partial view."
In the forcing chain it feeds MeasurementLayer_Forced in UnifiedForcingChain: without a finite positive outcome set there is no formal readout to force. Relative to the module's Born-rule sketch, the bin count is the discrete resolution at which J-cost weighting will later produce $|\psi|^2$-like frequencies. It closes the gap left by Determinism.lean, which had a lossy project but no typed space of observed labels.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.