possibility_actualization_adjoint
plain-language theorem explainer
The equivalence (◇p) c ↔ p (A c) under the adjoint hypothesis formalizes the duality between possible and actualized configurations in the modal framework. Physicists studying configuration selection via J-cost minimization would cite this when deriving realized states from possibility sets. The proof consists of a direct reference to the hypothesis without additional steps.
Claim. Let $p$ be a configuration property and $c$ a configuration. Under the adjoint hypothesis, the possibility modality satisfies $◇p(c) ↔ p(A(c))$, where $A(c)$ is the configuration minimizing J-cost within the possibility set generated from $c$.
background
The Modal.Actualization module imports Modal.Possibility and centers on the actualization operator A, defined as the map $A(c) = argmin_{y ∈ P(c)} J(y)$. This operator is dual to the possibility operator P, which generates candidate configurations from a given state. The Config structure from Gravity.ILG carries components upsilonStar, eps_r, eps_v, eps_t, eps_a, while upstream results supply the active edge count A from IntegrationGap and Masses.Anchor as the integer 1.
proof idea
The term proof is a one-line wrapper that directly invokes the hypothesis possibility_actualization_adjoint_hypothesis to obtain the equivalence.
why it matters
The result feeds the actualization_status definition in the same module, which reports on selection from possibilities via A as argmin J. It advances the modal actualization principle inside the Recognition Science framework and connects to the forcing chain steps T5 through T8 together with the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.