def definition def or abbrev

`stateToLedger`

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

formal statement (Lean)

 141noncomputable def stateToLedger {n : ℕ} (ψ : QuantumState n) : UncommittedLedger n :=

proof body

Definition body.

 142  ⟨(Finset.univ.filter (fun i => ψ.amplitudes i ≠ 0)).toList.map
 143    (fun i => ⟨i, ψ.amplitudes i, ‖ψ.amplitudes i‖^2, rfl⟩),
 144   filter_map_weight_sum ψ⟩
 145
 146/-- Probability of measuring outcome i from state ψ (Born rule). -/

depends on (15)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
QuantumState in IndisputableMonolith.Foundation.QuantumLedger decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
QuantumState in IndisputableMonolith.Information.NoCloning decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
map in IndisputableMonolith.Measurement.RSNative.Core decl_use
QuantumState in IndisputableMonolith.QFT.PauliExclusion decl_use
QuantumState in IndisputableMonolith.QFT.Unitarity decl_use
filter_map_weight_sum in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse decl_use
QuantumState in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse decl_use
UncommittedLedger in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse decl_use
toList in IndisputableMonolith.RecogSpec.ObservablePayloads decl_use