module module high

`IndisputableMonolith.Modal.Actualization`

The Actualization module encodes the principle that the universe selects cost-minimizing futures from possibility sets. Researchers deriving RS dynamics from modal structure would cite it when determining actualized states. The module supplies definitions and statements that rest on the imported Possibility module without internal proofs.

claimGiven current state $c$, the actualized future is chosen as $\arg\min_{y \in P(c)} J(y)$, where $P(c)$ is the possibility set. When the minimum is unique actualization is deterministic; multiple minima require further structure to resolve.

background

This module sits inside the modal layer of Recognition Science and imports the Possibility module to access the relation $P$. It introduces the Actualization Principle as the selection rule among possible futures, together with auxiliary notions for degeneracy, contingency, determination, and path actions with positive weights. The local setting treats $J$ as the recognition cost already defined upstream.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the Actualization Principle imported by the main Modal module and by ModalGeometry. It operationalizes the fundamental dynamical principle of RS in which the universe selects cost-minimizing futures, thereby enabling downstream modal geometry constructions.

scope and limits

Does not derive the cost function $J$ or the possibility relation $P$.
Does not specify concrete resolution rules for degenerate minima.
Does not link actualization to the phi-ladder or the T5-T8 forcing chain.
Does not address Berry creation thresholds or mass formulas.

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