outcome_is_determined
plain-language theorem explainer
For any observer subsystem, outcome space, and full ledger configuration, the measurement outcome is uniquely fixed: exactly one coarse-grained label is produced. Anyone arguing that RS quantum randomness is epistemic rather than ontological cites this. The proof is a one-line existence-uniqueness witness from the fact that outcome is already a total function.
Claim. Let $N\in\mathbb{N}$, let $S$ be a partition of the $N$ ledger entries into observer and system, let $\mathcal{O}$ be a finite outcome space with $m=|\mathcal{O}|>0$ labels, and let $c$ be a positive $N$-entry configuration. Then there exists a unique $k\in\{0,\ldots,m-1\}$ such that the outcome map sends $(S,\mathcal{O},c)$ to $k$.
background
Module F-009 formalizes measurement in Recognition Science: observers are internal subsystems of the ledger, not external agents. A Subsystem on $N$ entries is a partition with observer index set of size $K$ ($0<K<N$) and complementary system indices. A Configuration is an $N$-tuple of positive real ratios (ledger entries).
An OutcomeSpace is a finite coarse-graining with $m>0$ labels. The outcome map sums J-defect on the observer indices of $c$, scales by $m$, floors, and reduces mod $m$, yielding a label in $\mathrm{Fin}, m$. The projection uses only observer-index values, but those values are fixed by the full configuration through the global variational update.
The module's claim is that apparent quantum randomness is projection through finite internal resolution: the full state determines the outcome, while the observer's partial view does not. This theorem records the first half of that split.
proof idea
Term-mode uniqueness for a total function. The witness is the value outcome S space c itself; reflexivity gives existence; any other $k$ equal to that value is identical by symmetry of equality. No lemmas are invoked beyond the definition of the outcome map and the standard unique-existence constructor.
why it matters
This is the deterministic half of the measurement story. Downstream, deterministic_but_unpredictable pairs it with subsystem_cannot_know_whole to conclude that outcomes are determined by the full state yet underdetermined by the observer's partial view, so randomness is epistemic. The F-009 certificate measurement_mechanism_certificate lists it as fact (1): outcomes are deterministic functions of the full state.
In the forcing chain it feeds Variational_To_Measurement_Bridge and variational_to_measurement_bridge_holds, which package variational dynamics plus subsystem projection into the measurement layer. The doc-comment is explicit: stating the triviality matters because it means quantum randomness is not fundamental in RS. It does not itself produce Born weights; those enter later via J-cost near equilibrium.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.