module module high

`IndisputableMonolith.Modal.Actualization`

The Actualization module encodes the core dynamical rule of Recognition Science: given current state c the universe selects the future y in P(c) that minimizes J-cost. It introduces the ActualizationPrinciple together with degeneracy handling, path actions, and weight predicates. Modal physicists cite this when modeling state transitions from possibility to observed reality. The module is built from definitions and short lemmas rather than extended proofs.

claimThe Actualization Principle states that for current state $c$, the realized future is $y = argmin_{y' in P(c)} J(y')$. When the minimum is unique the outcome is deterministic; multiple minima constitute a degenerate case resolved by further structure.

background

This module belongs to the Modal domain and imports the Possibility module, which supplies the set $P(c)$ of futures reachable from configuration $c$. It defines the ActualizationPrinciple as the selection rule that picks the lowest-J element of that set. Supporting notions include has_actualization, Degenerate configurations, Contingent versus Determined outcomes, PathAction, and PathWeight with its positivity lemma.

proof idea

This is a definition module, no proofs. It declares the central principle and then auxiliary predicates (has_actualization, determined_necessary_for_minimal, path_action_nil, path_weight_pos) that record basic properties of the selection process.

why it matters in Recognition Science

The module supplies the dynamical selection rule imported by the parent Modal module and by ModalGeometry. It operationalizes the cost-minimizing step that turns the possibility set into realized states, thereby anchoring the modal layer of the Recognition Science framework.

scope and limits

Does not specify the explicit functional form of the cost J.
Does not resolve degeneracy beyond noting that further structure is required.
Does not prove existence or uniqueness of minima.
Does not connect actualization to spatial dimension or numerical constants.

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