pith. sign in
module module high

IndisputableMonolith.Measurement.BornRule

show as:
view Lean formalization →

This module derives two-outcome measurement probabilities directly from recognition weights. Quantum foundations researchers would cite it when linking recognition costs to Born-rule statistics. The module imports the C=2A bridge and path-action interface, then normalizes weights into probabilities via sibling definitions and theorems.

claimFor a two-outcome measurement with recognition costs $C_1, C_2$, the probabilities are $p_1 = C_1/(C_1+C_2)$, $p_2 = C_2/(C_1+C_2)$, obtained by normalizing the weights that satisfy $C=2A$ for two-branch geodesic rotations.

background

The module belongs to the Measurement domain. It rests on two upstream modules. The C2ABridge states: 'This module proves the central equivalence between recognition cost C and the residual-model rate action A. Main theorem: For any two-branch geodesic rotation, C = 2A (exactly)'. The PathAction module supplies: 'Lightweight interface for recognition paths and their action/weights. Heavy measure-theoretic lemmas (piecewise additivity, domain shifts, etc.) are intentionally omitted to keep the build surface stable for paper exports.'

proof idea

This is a definition module with supporting theorems. It introduces TwoOutcomeMeasurement as the setup, defines prob and probabilities_normalized, then states born_rule_from_C and born_rule_normalized. The argument applies the imported C=2A equivalence and path weights to obtain the normalized probabilities.

why it matters in Recognition Science

The module supplies the explicit map from recognition weights to two-outcome probabilities, completing the measurement step that follows the C=2A bridge. It feeds the broader derivation of the Born rule inside Recognition Science by turning path actions into observable statistics. No downstream theorems are recorded yet.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (6)