theorem proved term proof

`probability_equals_weight`

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

formal statement (Lean)

 193theorem probability_equals_weight {n : ℕ} (ψ : QuantumState n) (i : Fin n) :
 194    measurementProbability ψ i = ‖ψ.amplitudes i‖^2 := rfl

proof body

Term-mode proof.

 195
 196/-! ## Why Measurement is Irreversible -/
 197
 198/-- Measurement irreversibility: once committed, the ledger cannot uncommit.
 199    This explains the thermodynamic arrow in measurement. -/

depends on (13)

Lean names referenced from this declaration's body.

Measurement in IndisputableMonolith.Data.Import decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
QuantumState in IndisputableMonolith.Foundation.QuantumLedger decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
QuantumState in IndisputableMonolith.Information.NoCloning decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
Measurement in IndisputableMonolith.Measurement.RSNative.Core decl_use
QuantumState in IndisputableMonolith.QFT.PauliExclusion decl_use
QuantumState in IndisputableMonolith.QFT.Unitarity decl_use
measurementProbability in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse decl_use
QuantumState in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse decl_use
Measurement in IndisputableMonolith.Quantum.NonlocalityNoSignaling decl_use