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)
113structure TransmutationPath where
114 /-- Initial fission product configuration. -/
115 start : NuclearConfig
116 /-- Final (stable) end state. -/
117 finish : NuclearConfig
118 /-- Number of steps. -/
119 n_steps : ℕ
120 /-- Net cost reduction from start to finish. -/
121 net_reduction : nuclearCost finish ≤ nuclearCost start
122
123/-- **THEOREM EN-006.6**: Any transmutation path reduces total cost. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (12)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
NuclearConfig
in IndisputableMonolith.Engineering.FissionTransmutationStructure
decl_use
-
nuclearCost
in IndisputableMonolith.Engineering.FissionTransmutationStructure
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
from
in IndisputableMonolith.Foundation.PrimitiveDistinction
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
total
in IndisputableMonolith.NavierStokes.DiscreteVorticity
decl_use
-
total
in IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget
decl_use