module module

`IndisputableMonolith.Engineering.FissionTransmutationStructure`

show as: view Lean formalization →

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

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (24)

structure NuclearConfig L50
def nuclearCost L56
theorem nuclear_cost_nonneg L59
theorem nuclear_cost_zero_iff_stable L64
theorem transmutation_cost_pos L83
structure TransmutationStep L94
theorem transmutation_reduces_cost L101
theorem cost_reduction_bounded L106
structure TransmutationPath L113
theorem path_reduces_total_cost L124
def stable_config L129
theorem stable_config_zero_cost L132
theorem stable_is_optimal L137
structure DoublyMagicAttractor L145
theorem stable_is_attractor L152
theorem stable_end_state_exists L157
theorem cost_monotone_descent_terminates L168
theorem strict_transmutation_progress L181
def transmutation_efficiency L195
theorem efficiency_bounded L200
theorem perfect_transmutation_efficiency L215
theorem fission_transmutation_from_ledger L227
theorem fission_transmutation_structure L236
def en006_certificate L241