actualization_status
plain-language theorem explainer
The definition supplies a string constant that reports on actualization as selection from possibilities via the argmin of the J-cost function. A researcher reviewing the modal layer of Recognition Science would cite the report to recall degeneracy as multiple cost-equivalent successors, contingency as alternative outcomes, and the derived Born rule. The implementation is a direct multi-line string concatenation with no logical steps or lemmas applied.
Claim. The status report for the actualization module is the string constant describing the actualization operator as the argmin of the $J$-cost function, degeneracy as the presence of multiple cost-equivalent successors, contingency as the possibility of alternative outcomes, path action as the total $J$-cost along a trajectory, and the Born rule probability $P[γ] ∝ exp(-C[γ])$ as emerging from the cost structure.
background
The Modal.Actualization module imports Modal.Possibility and assembles concepts from the foundation layer. The cost of any recognition event equals its $J$-cost per the ObserverForcing definition. The cost function induced by a multiplicative recognizer is the derived cost of its comparator on positive ratios. The active edge count per fundamental tick is the constant $A := 1$, satisfying the $φ$-power balance identity at $D = 3$. The magnitude-of-mismatch theorem supplies a single-valued comparison operator on any carrier and cost type. Primitive distinction reduces seven independent axioms to four structural conditions plus three definitional facts.
proof idea
The definition is a direct assignment of a concatenated string literal. No lemmas from the upstream results are invoked. It functions as a documentation artifact that enumerates core concepts and lists theorems such as every_config_actualizes and possibility_actualization_adjoint without executing any tactic or term reduction.
why it matters
The declaration earns its place by furnishing a human-readable summary of the actualization principle inside the modal domain. It documents the module containing theorems on total actualization and adjoint relations to possibility, which sit downstream from the forcing chain steps T5 (J-uniqueness) through T8 (D = 3). The report also records the emergence of the Born rule from cost structure, linking to the Recognition Composition Law without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.