module module

`IndisputableMonolith.Foundation.BornRuleForcing`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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