Pith. sign in
module module moderate

IndisputableMonolith.Quantum.BornRuleStructure

show as:
view Lean formalization →

Module collecting structural consequences of the Born rule once it is forced from the ledger: probability weights are nonnegative, phase factors cancel in the squared modulus, and the measure is compatible with the two-branch exp(−C) form. Quantum and foundations workers cite it when they need the nonnegativity and phase-invariance layer without reopening uniqueness. The content is mostly short lemmas and structure bundles over the upstream Born-rule derivation.

claimStructural package for the Born rule on 8-mode sectors: probability weights $w$ satisfy $w \ge 0$, global phases cancel in $P = |\psi|^2$, and the measure remains normalised, additive on disjoint mode sets, and consistent with the two-branch form $P \propto e^{-C}$.

background

Recognition Science derives the Born rule as the unique probability measure on 8-mode (DFT-8) sectors that is normalised, phase-invariant, additive over disjoint mode-sets, and consistent with the two-branch exp(−C) rule coming from the J-cost. The upstream module states that uniqueness result (QF-002).

This module sits one layer above that uniqueness theorem. It packages the structural properties that follow once $P = |\psi|^2$ is in hand: nonnegativity of weights, cancellation of pure phases under the modulus squared, and the ledger-facing interface that reads those weights off recognition costs. The eight-tick octave and the J-cost $J(x) = (x + x^{-1})/2 - 1$ remain the ambient forcing background; nothing here re-derives uniqueness.

proof idea

Not a single theorem: a small cluster of structure lemmas and a structure record. Typical steps are: (i) read weights from the ledger cost, (ii) cancel a global $U(1)$ phase in $|e^{i\theta}\psi|^2$, (iii) obtain pointwise nonnegativity, and (iv) bundle those facts so downstream code can assume a nonnegative Born measure without unfolding the uniqueness proof. Several declarations are thin wrappers or elementary inequalities over the upstream Born-rule API.

why it matters in Recognition Science

Closes the structural gap between “Born is unique on 8-mode sectors” and “the weights one actually sums are nonnegative and phase-safe.” That is the layer measurement and decoherence arguments need before they can treat $P = |\psi|^2$ as an ordinary probability. It inherits the QF-002 forcing story (J-cost, DFT-8 sector forcing, two-branch exp(−C)) and does not claim new uniqueness. No downstream modules are wired yet in the graph; the natural consumers are any later quantum or measurement developments that quote nonnegativity or phase cancellation rather than re-proving them.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (5)