No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
46structure Substrate where
47 label : String
48 phase : ℕ
49 sigma : ℤ
50 deriving DecidableEq, Repr
51
52namespace Substrate
53
54/-- The "divine" substrate predicate: phase = 0 and σ = 1. -/
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
in IndisputableMonolith.Relativity.ILG.Substrate
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
-
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.
-
sigma
in IndisputableMonolith.Decision.AbileneParadox
decl_use
-
phase
in IndisputableMonolith.Foundation.EightTick
decl_use
-
and
in IndisputableMonolith.NumberTheory.CirclePhaseLift
decl_use
-
sigma
in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
decl_use
-
phase
in IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge
decl_use
-
Substrate
in IndisputableMonolith.Relativity.ILG.Substrate
decl_use
-
divine
in IndisputableMonolith.Theology.SubstrateIndependentMonotheism
decl_use