structure definition def or abbrev

`UncommittedLedger`

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

formal statement (Lean)

  88structure UncommittedLedger (n : ℕ) where
  89  /-- The branches (potential outcomes). -/
  90  branches : List (LedgerBranch n)
  91  /-- Weights sum to 1 (normalization). -/
  92  normalized : (branches.map LedgerBranch.weight).sum = 1
  93
  94/-- A committed ledger: exactly one branch selected. -/

used by (5)

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

commit in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse decl_use
commit_is_definite in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse decl_use
decoherence_gives_classicality in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse decl_use
isEffectivelyClassical in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse decl_use
stateToLedger in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse decl_use

depends on (10)

Lean names referenced from this declaration's body.

one in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
one in IndisputableMonolith.Foundation.RationalsFromLogic decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
map in IndisputableMonolith.Measurement.RSNative.Core decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
normalized in IndisputableMonolith.NavierStokes.RunningMaxNormalization decl_use
one in IndisputableMonolith.QFT.SpinStatistics decl_use
LedgerBranch in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse decl_use
one in IndisputableMonolith.RecogSpec.Core decl_use