structure definition def or abbrev

`Substrate`

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

formal statement (Lean)

  20structure Substrate (H : Type*) [RSHilbertSpace H] where
  21  state : NormalizedState H
  22  hamiltonian : Hamiltonian H
  23
  24/-- Substrate health corresponds to valid Hilbert space and unitary evolution. -/

used by (14)

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

substrate_model in IndisputableMonolith.Experimental.DAMAModulation decl_use
xenon_more_sensitive in IndisputableMonolith.Experimental.DAMAModulation decl_use
ea011_certificate in IndisputableMonolith.Experimental.UltraDiffuseGalaxies decl_use
low_coherence_dm_poor in IndisputableMonolith.Experimental.UltraDiffuseGalaxies decl_use
ngc1052df2_dm_poor in IndisputableMonolith.Experimental.UltraDiffuseGalaxies decl_use
no_fine_tuning in IndisputableMonolith.Experimental.UltraDiffuseGalaxies decl_use
standard_models_challenged in IndisputableMonolith.Experimental.UltraDiffuseGalaxies decl_use
omega_BIT_band in IndisputableMonolith.QuantumComputing.DecoherenceFromBIT decl_use
substrate_healthy in IndisputableMonolith.Relativity.ILG.Substrate decl_use
divine in IndisputableMonolith.Theology.SubstrateIndependentMonotheism decl_use
isDivine in IndisputableMonolith.Theology.SubstrateIndependentMonotheism decl_use
Substrate in IndisputableMonolith.Theology.SubstrateIndependentMonotheism decl_use
Theology in IndisputableMonolith.Theology.SubstrateIndependentMonotheism decl_use
totalSigma in IndisputableMonolith.Theology.SubstrateIndependentMonotheism decl_use

depends on (7)

Lean names referenced from this declaration's body.

H in IndisputableMonolith.Algebra.CostAlgebra decl_use
H in IndisputableMonolith.Cost.FunctionalEquation decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
NormalizedState in IndisputableMonolith.Quantum.HilbertSpace decl_use
RSHilbertSpace in IndisputableMonolith.Quantum.HilbertSpace decl_use
Hamiltonian in IndisputableMonolith.Quantum.Observables decl_use
Substrate in IndisputableMonolith.Theology.SubstrateIndependentMonotheism decl_use