pith. sign in
module module high

IndisputableMonolith.Measurement.BornRule

show as:
view Lean formalization →

This module derives two-outcome measurement probabilities from recognition weights. Quantum measurement theorists cite it for the recognition-based account of Born's rule. The module assembles the result by importing the C=2A equivalence and path-action interface without internal proofs.

claimFor two-branch geodesic rotations the outcome probabilities are the normalized recognition weights: $p_i = w_i / (w_1 + w_2)$ where each weight $w$ is obtained from the recognition cost $C$ via the bridge $C = 2A$.

background

The module belongs to the Measurement domain and imports two supporting modules. C2ABridge establishes the central equivalence $C = 2A$ exactly for any two-branch geodesic rotation. PathAction supplies the minimal interface for recognition paths together with their action and weight assignments, deliberately omitting heavy measure-theoretic lemmas.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the recognition-derived Born rule for two-outcome cases and thereby links the C=2A bridge directly to observable probabilities. It occupies the position between the path-action interface and any larger measurement formalism inside the Recognition Science framework.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (6)