module module high

`IndisputableMonolith.Foundation.BornRuleForcing`

Foundation module that forces the Born measure on eight-mode complex signals: sector mass equals summed squared norms, is nonnegative and at most one, totals one on a full partition, and is invariant under global phase. Quantum and measurement authors cite it when deriving P = |ψ|² from ledger cost rather than postulating it. The argument assembles norm identities, a normalisation predicate, and phase-rotation invariance on the forced ℂ structure.

claimOn the eight-mode complex signal space forced by the octave shift, a state $\psi$ is normalised when $\sum_k \|\psi_k\|^2 = 1$. The sector measure $\mu(S) = \sum_{k\in S}\|\psi_k\|^2$ is nonnegative, at most one, equals the singleton mass on one mode, totals one over a full partition, and is invariant under global phase rotation $\psi\mapsto e^{i\theta}\psi$.

background

Recognition Science obtains complex amplitudes from the eight-tick ledger cycle (T7): the cyclic shift on the real ledger state space is not diagonalisable over $\mathbb{R}$, so complexification is algebraically forced (Complex Structure Forcing). Once signals live in an eight-mode complex space, squared norms and inner-product identities become the natural mass data.

Independently, the two-outcome measurement bridge upgrades path weights to normalised probabilities $P_{\cos}=\cos^2\theta$ and $P_{\sin}=\sin^2\theta$ via the cost exponentials $\exp(-C)$. This module sits between those two inputs: it defines normalisation of an eight-component signal and the additive sector measure built from squared norms, together with phase rotation and its norm preservation.

Notation: sector measure of a mode set $S$ is the sum of squared mode norms; a signal is normalised when that sum over all eight modes is one. Phase rotation multiplies every component by a common unit complex factor.

proof idea

Definition-heavy module with short supporting lemmas, not a single deep proof. Norm-square identities relate the complex modulus, the star-self product, and the eight-mode inner product on the diagonal. Normalisation is the predicate that total squared norm equals one. Sector measure is defined as the sum of squared norms over a mode set; nonnegativity, the bound $\le 1$ for normalised signals, singleton evaluation, and partition totality are immediate from finite-sum arithmetic and the normalisation hypothesis. Phase rotation is componentwise multiplication by $e^{i\theta}$; its norm is unchanged, so sector measure is phase-invariant by rewriting each term.

why it matters in Recognition Science

Feeds the Quantum BornRule development (QF-002): the Born rule $P=|\psi|^2$ is characterised there as the unique probability measure on eight-mode sectors that is normalised, phase-invariant, additive on disjoint mode sets, and consistent with the two-branch $\exp(-C)$ certificate. Without the sector measure, its bounds, totality, and phase invariance packaged here, that uniqueness theorem has no measure object to pin down.

In the broader forcing chain the module converts T7's complex structure and the two-outcome cost bridge into the concrete mass functional used for quantum probabilities. It is the ledger-side reason amplitudes enter as squared norms rather than as an extra postulate. Downstream work on multi-outcome and continuous measurements builds on the same sector calculus.

scope and limits

Does not prove uniqueness of the Born measure; that lives in Quantum.BornRule.
Does not derive complex structure; it imports ComplexStructureForcing.
Does not treat continuous spectra or infinite-dimensional Hilbert spaces.
Does not re-derive the two-outcome cos²/sin² identities; those come from TwoOutcomeBornCert.
Does not address decoherence, collapse dynamics, or experimental calibration.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Quantum.BornRule module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.ComplexStructureForcing module_import
IndisputableMonolith.Verification.TwoOutcomeBornCert module_import

declarations in this module (26)

theorem normSq_eq_norm_sq L38
theorem star_mul_self_eq_ofReal_normSq L41
theorem inner8_self_eq L45
def IsNormalized L53
def sectorMeasure L58
theorem sectorMeasure_nonneg L61
theorem sectorMeasure_le_one L65
theorem sectorMeasure_singleton L73
theorem sectorMeasure_total L77
def phaseRotate L83
theorem norm_phaseRotate L86
theorem sectorMeasure_phase_invariant L91
theorem isNormalized_phaseRotate L97
theorem sectorMeasure_disjoint_union L105
theorem sectorMeasure_compl L111
theorem dft_sector_total_eq L118
theorem isNormalized_dft8 L126
def twoBranchSignal L134
theorem norm_ofReal_sq L140
theorem twoBranchSignal_normalized L144
theorem sector_matches_cos_branch L167
theorem sector_matches_sin_branch L173
theorem sector_matches_gibbs_born L181
theorem born_weight_forced L194
theorem dft8_sector_forcing L219
theorem dft8_sector_forcing_freq L236