module module high

`IndisputableMonolith.Foundation.BornRuleForcing`

Foundation module that equips 8-mode ledger signals with normalisation, sector measures, and phase-rotation invariance needed to force the Born rule. Anyone deriving P = |ψ|² from Recognition cost structure cites it. It sits between complex-structure forcing (eight-tick shift) and the two-outcome exp(−C) certificate, and is imported by the quantum Born-rule uniqueness theorem.

claimA signal $\psi$ on the eight-mode space is normalised when $\sum_k \|\psi_k\|^2 = 1$. For a mode-set $S$, the sector measure is $m_\psi(S) = \sum_{k\in S} \|\psi_k\|^2$. Then $m_\psi\ge 0$, $m_\psi\le 1$, $m_\psi$ recovers singleton squared norms and total mass one on the full set, and $m_\psi$ is invariant under phase rotations $\psi_k\mapsto e^{i\theta_k}\psi_k$.

background

Recognition Science forces an eight-tick cyclic shift on the ledger (T7). Complex Structure Forcing shows that shift cannot be diagonalised over the reals, so the state space is complexified and modes carry complex amplitudes. Squared norms $|\psi_k|^2$ are the natural real weights on those modes.

Independently, the two-outcome Born certificate upgrades the path-weight identity pathWeight = sin²θ into normalised probabilities: $P_{\cos}=\cos^2\theta$ and $P_{\sin}=\sin^2\theta$ obtained from the Boltzmann-like weights exp(−C) on the two cost branches.

This module packages the multi-mode bookkeeping: normalisation of a full eight-component signal, the set-function that sums squared norms over mode sectors, and the phase-rotation action that leaves those measures unchanged. Those are exactly the axioms the downstream uniqueness argument needs.

proof idea

Definition-and-lemma module, not a single deep theorem. It introduces IsNormalized (sum of squared norms equals one), sectorMeasure as the sum of squared norms over a mode-set, and phaseRotate as componentwise unit-modulus multiplication. Elementary lemmas then record nonnegativity, the bound by one, evaluation on singletons and on the full set, preservation of the Euclidean norm under phase rotation, and invariance of sectorMeasure under that action. Supporting identities relate complex norm-squared to the real inner-product form star(z)*z. No heavy tactic proof; the content is the interface those facts expose.

why it matters in Recognition Science

Feeds IndisputableMonolith.Quantum.BornRule (QF-002), whose doc-comment states the target: the Born rule P = |ψ|² is the unique probability measure on 8-mode sectors that is normalised, phase-invariant, additive over disjoint mode-sets, and consistent with the two-branch exp(−C) rule. Without sectorMeasure, IsNormalized, and sectorMeasure_phase_invariant, that uniqueness statement has no carrier.

In the broader chain the module sits after T7 (eight-tick octave) and complexification, and after the two-outcome certificate that already matches sin²/cos². It is the bridge from those forcing results to a genuine multi-outcome probability calculus on the DFT-8 sectors used throughout the quantum layer.

scope and limits

Does not prove uniqueness of the Born measure; that lives in Quantum.BornRule.
Does not derive the two-outcome cos²/sin² identities; those come from TwoOutcomeBornCert.
Does not re-prove complexification of the eight-tick shift; that is ComplexStructureForcing.
Does not address continuous spectra, POVMs beyond mode sectors, or decoherence dynamics.
Does not fix dimension or tick period; it assumes the eight-mode setting already forced upstream.

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