module module

`IndisputableMonolith.Quantum.BornRule`

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 (4)

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

IndisputableMonolith.Quantum module_import
IndisputableMonolith.Quantum.BornRuleStructure module_import
IndisputableMonolith.Quantum.EntanglementOntologyStructure module_import
IndisputableMonolith.Skeleton.Quantum module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.BornRuleForcing module_import
IndisputableMonolith.Foundation.EightTick module_import

declarations in this module (8)

theorem born_rule_consistent L43
lemma normSq_exp_I_eq_one L48
theorem born_rule_phase_independent L54
theorem interference_from_phase L59
theorem born_rule_from_jcost L70
theorem normalization_from_jcost L86
theorem gleason_from_rs L94
structure BornRuleFalsifier L106