pith. the verified trust layer for science. sign in
module module high

IndisputableMonolith.Measurement.BornRule

show as:
view Lean formalization →

The BornRule module derives two-outcome measurement probabilities directly from recognition weights. Quantum foundations researchers would cite it when connecting recognition costs to probabilistic outcomes. It structures the argument as definitions of normalized weights that apply the C=2A equivalence imported from the bridge and path modules.

claimFor a two-outcome measurement the probabilities satisfy $p_i = w_i / (w_+ + w_-)$, where the weights $w$ are obtained from the recognition cost via the relation $C = 2A$ on geodesic paths.

background

Recognition paths carry an action $A$ and a recognition cost $C$. The upstream C2ABridge proves the central equivalence: for any two-branch geodesic rotation, $C = 2A$ exactly. PathAction supplies the lightweight interface for these paths and their weights, omitting heavy measure-theoretic lemmas to keep the build surface stable for paper exports.

proof idea

This is a definition module that introduces TwoOutcomeMeasurement together with prob and probabilities_normalized, then constructs born_rule_from_C and born_rule_normalized by direct substitution of the $C=2A$ relation into the weight definitions supplied by PathAction.

why it matters in Recognition Science

The module supplies the explicit map from recognition weights to Born-rule probabilities for two outcomes, realizing the module doc-comment goal. It advances the measurement domain within the Recognition Science program that begins from the forcing chain and J-uniqueness, even though no downstream uses are recorded yet.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (6)