BornRule
plain-language theorem explainer
The BornRule structure encodes the emergence of the Born rule by defining path probabilities as normalized exponential weights from the underlying cost function. Physicists deriving quantum probabilities from path integrals or recognition functionals would cite this when showing the rule follows from the J-cost without separate postulate. The definition sets the partition function Z via direct foldl summation over PathWeight and defines the probability field as the conditional ratio.
Claim. Let $P$ be a nonempty list of paths, each a list of configurations. Let $W(γ) = exp(-C(γ))$ be the weight of path $γ$, where $C$ is the path action. Define the partition function $Z = sum_{γ in P} W(γ)$. The probability of path $γ$ is $P(γ) = W(γ)/Z$ if $γ in P$, and zero otherwise.
background
In the Modal.Actualization module the BornRule structure operates over lists of configuration paths drawn from the possibility space. PathWeight is the exponential of the negative path action, $W[γ] = exp(-C[γ])$, supplying the positive quantity that yields probabilities. This rests on upstream J-cost calibration from PhiForcingDerived.of and ledger factorization from DAlembert.LedgerFactorization.of, together with configuration structures from ILG.Config and spectral constraints from SpectralEmergence.of.
proof idea
The declaration is a structure definition whose fields are introduced directly: the path list, the nonempty hypothesis, and the derived partition function Z obtained by foldl summation of PathWeight. The probability field is defined inline as a conditional division by Z. Downstream normalization relies on the supporting lemmas List.sum_map_div' and foldl_add_eq_sum that equate the foldl sum to the mapped sum divided by Z.
why it matters
BornRule supplies the probability mechanism that actualizes paths in the modal framework and directly feeds the born_rule_normalized theorem verifying that probabilities sum to one. It realizes the module claim that the Born rule emerges from the cost structure rather than being postulated, consistent with T5 J-uniqueness and the Recognition Composition Law. The declaration closes one link in the chain from phi-forced costs to observable probabilities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.