structure definition def or abbrev

`CommittedLedger`

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

formal statement (Lean)

  95structure CommittedLedger (n : ℕ) where
  96  /-- The selected outcome. -/
  97  outcome : Fin n
  98  /-- The final amplitude (phase factor). -/
  99  amplitude : Amplitude
 100  /-- The amplitude has unit norm (after normalization). -/
 101  unit_norm : ‖amplitude‖ = 1
 102
 103/-! ## The Measurement Process -/
 104
 105/-- Helper: sum over filter equals sum over all for norm-squared (zeros contribute nothing). -/

used by (2)

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

commit in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse decl_use
measurement_irreversible in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse decl_use

depends on (14)

Lean names referenced from this declaration's body.

all in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
all in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
Measurement in IndisputableMonolith.Data.Import decl_use
all in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
phase in IndisputableMonolith.Foundation.EightTick decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
Measurement in IndisputableMonolith.Measurement.RSNative.Core decl_use
all in IndisputableMonolith.Musicology.ModalPreferenceFromPhi decl_use
phase in IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge decl_use
amplitude in IndisputableMonolith.QFT.SMatrixUnitarity decl_use
amplitude in IndisputableMonolith.Quantum.DoubleSlit decl_use
Amplitude in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse decl_use
Measurement in IndisputableMonolith.Quantum.NonlocalityNoSignaling decl_use