same_state_same_outcome
plain-language theorem explainer
Identical full ledger configurations always yield the same coarse-grained measurement outcome for a fixed observer subsystem and outcome space. Anyone citing full-state determinism of RS measurement (as opposed to observer-relative underdetermination) would cite this. The proof is a short term argument: unfold the outcome map and simplify on equal entry functions.
Claim. Fix a partition $S$ of an $N$-entry ledger into observer and system, a finite outcome space, and two configurations $c_1,c_2$. If the entry functions of $c_1$ and $c_2$ agree pointwise, then the coarse-grained measurement outcome of $c_1$ equals that of $c_2$.
background
Module F-009 formalizes measurement in Recognition Science: observers are internal subsystems of the ledger, not external agents. A configuration is an $N$-tuple of positive real ratios (ledger entries). A subsystem splits the $N$ indices into observer indices of size $K$ and complementary system indices.
The outcome map sends a full configuration to a discrete label in a finite outcome space by summing J-defect on the observer indices, scaling by the number of bins, and reducing modulo that number. By construction the readout depends only on observer-index values, but those values themselves are fixed by the global variational update of the full state.
The surrounding claim is that full-ledger dynamics are deterministic, while an internal observer sees only a partial view and therefore experiences underdetermination. This lemma is the positive half of that split: same full state, same outcome.
proof idea
Term-mode, two steps. Unfold the definition of the outcome map (observer-index defect sum, floor-scale, mod). Then simp with the hypothesis that the two configurations have identical entry functions, so every summand and every arithmetic expression built from them agrees. No external lemmas are required beyond definitional equality.
why it matters
This is the full-state determinism half of the measurement mechanism. Downstream, Variational_To_Measurement_Bridge packages it as the field that outcomes are deterministic functions of the full configuration, and variational_to_measurement_bridge_holds discharges that field by applying this theorem (together with outcome_is_determined). That bridge is the handoff from the variational layer into measurement inside the unified forcing chain.
In the module narrative it pairs with observational equivalence: many distinct full states share one observer view, so the same partial information can sit over different future coupled updates, while any single full state still has one outcome. It does not itself force Born weights; those enter later via J-cost near equilibrium. Landmark contact is the measurement-mechanism layer after variational dynamics, not T5–T8 directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.