module module

`IndisputableMonolith.Modal.Actualization`

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

used by (2)

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

IndisputableMonolith.Modal module_import
IndisputableMonolith.Modal.ModalGeometry module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Modal.Possibility module_import

declarations in this module (30)

structure ActualizationPrinciple L60
def has_actualization L71
theorem every_config_actualizes L75
def Degenerate L92
def Contingent L101
def Determined L108
theorem determined_necessary_for_minimal L113
def PathAction L125
lemma path_action_nil L134
lemma path_action_single L137
def PathWeight L144
lemma path_weight_pos L148
structure BornRule L156
lemma foldl_add_eq_sum L176
theorem born_rule_normalized L197
def collapse_threshold L226
def has_definite_pointer L229
theorem collapse_automatic L236
def A L254
lemma A_well_defined L257
theorem A_toward_identity L260
theorem A_advances_time L264
def CostMonotonic L280
theorem adjoint_from_cost_monotonic L284
theorem H_adjoint_non_minimal L299
theorem possibility_actualization_adjoint_minimal L323
theorem possibility_actualization_adjoint_monotonic L339
def possibility_actualization_adjoint_hypothesis L389
theorem possibility_actualization_adjoint L392
def actualization_status L400