TwoOutcomeMeasurement
plain-language theorem explainer
TwoOutcomeMeasurement packages two non-negative real recognition costs C1 and C2 that label the outcomes of a binary measurement. Derivations of the Born rule from the J-cost functional cite this structure to parameterize normalized exponential weights. The definition is a direct record with four fields and no computational reduction.
Claim. A two-outcome measurement consists of recognition costs $C_1, C_2 : ℝ$ satisfying $C_1 ≥ 0$ and $C_2 ≥ 0$, from which probabilities are formed as the normalized weights $p_i = e^{-C_i} / (e^{-C_1} + e^{-C_2})$.
background
The module derives Born's rule from the recognition cost functional J and the amplitude bridge 𝒜 = exp(-C/2)·exp(iφ). Recognition costs are supplied by ObserverForcing.cost, which sets cost(e) := Cost.Jcost e.state for a RecognitionEvent, and by MultiplicativeRecognizerL4.cost, which returns derivedCost m.comparator on positive ratios. DAlembert.LedgerFactorization.of calibrates J on the multiplicative monoid (ℝ₊, ×), while PhiForcingDerived.of supplies the concrete structure of J-cost.
proof idea
This is a structure definition with an empty proof body. It introduces the record type directly via four fields: the two costs and their non-negativity assertions. No upstream lemmas are applied; the construction is purely declarative.
why it matters
The structure supplies the input type for born_rule_from_C, which proves that the resulting probabilities equal squared amplitudes, and for probabilities_normalized, which verifies that the two probabilities sum to one. It realizes the recognition weights inside the module's derivation of the Born rule and connects to the forcing chain that recovers quantum measurement from J-cost events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.