abbrev definition def or abbrev

`Amplitude`

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

formal statement (Lean)

  56abbrev Amplitude := ℂ

Definition body.

  57
  58/-- A quantum state in a finite-dimensional Hilbert space.
  59    Represented as a function from basis states to amplitudes. -/

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

amplitude_sum_nonneg in IndisputableMonolith.Analysis.BernsteinInequality decl_use
bernstein_bound_pos in IndisputableMonolith.Analysis.BernsteinInequality decl_use
stemCellDecay in IndisputableMonolith.CrossDomain.PhiInverseInvariants decl_use
p_steepness_pos in IndisputableMonolith.Gravity.GravityParameters decl_use
KernelParams in IndisputableMonolith.ILG.Kernel decl_use
weight_equals_born in IndisputableMonolith.Measurement.C2ABridge decl_use
pathWeight in IndisputableMonolith.Measurement.PathAction decl_use
pathWeight_pos in IndisputableMonolith.Measurement.PathAction decl_use
CommittedLedger in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse decl_use
LedgerBranch in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse decl_use
QuantumState in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse decl_use

Lean names referenced from this declaration's body.

A in IndisputableMonolith.Foundation.IntegrationGap decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use