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)
157theorem stable_end_state_exists (cfg : NuclearConfig) :
158 ∃ path : TransmutationPath,
159 path.start = cfg ∧
160 nuclearCost path.finish = 0 := by
proof body
Term-mode proof.
161 use ⟨cfg, stable_config, 1, by rw [stable_config_zero_cost]; exact nuclear_cost_nonneg cfg⟩
162 exact ⟨rfl, stable_config_zero_cost⟩
163
164/-! ## §V. Cost-Descent Optimality -/
165
166/-- **THEOREM EN-006.11**: Cost-decreasing transmutation is optimal.
167 Any sequence of steps that strictly decreases cost will reach stability. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (22)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
V
in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost
decl_use
-
NuclearConfig
in IndisputableMonolith.Engineering.FissionTransmutationStructure
decl_use
-
nuclearCost
in IndisputableMonolith.Engineering.FissionTransmutationStructure
decl_use
-
nuclear_cost_nonneg
in IndisputableMonolith.Engineering.FissionTransmutationStructure
decl_use
-
stable_config
in IndisputableMonolith.Engineering.FissionTransmutationStructure
decl_use
-
stable_config_zero_cost
in IndisputableMonolith.Engineering.FissionTransmutationStructure
decl_use
-
TransmutationPath
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
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
V
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
Cost
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
that
in IndisputableMonolith.NumberTheory.PhiLadderLattice
decl_use
-
V
in IndisputableMonolith.RRF.Core.Glossary
decl_use