possibility_actualization_adjoint_hypothesis
possibility_actualization_adjoint_hypothesis defines the adjointness relation between the possibility operator and the actualization map A for any property p of configurations. A modal physicist working in Recognition Science would cite it when assuming that a property holds in some possible successor exactly when it holds at the minimal-cost actualized state. The declaration is a direct definition of the biconditional with no lemmas or tactics applied.
claimLet $p$ be a predicate on configurations and $c$ a configuration. The hypothesis asserts that possibility of $p$ at $c$ is equivalent to $p$ holding at the actualized configuration $A(c)$, where $A(c)$ is the configuration of minimal $J$-cost among the possible successors of $c$.
background
In the Modal.Actualization module, a configuration is a structure carrying a positive real value together with a time coordinate in ticks. ConfigProp is the abbreviation for predicates on configurations. The actualization operator $A$ is defined by $A(c) = $ argmin of $J(y)$ over $y$ in the possible successors $P(c)$, serving as the dual to the possibility operator.
proof idea
This is a direct definition whose body is the biconditional itself. No upstream lemmas are invoked and no tactics are used.
why it matters in Recognition Science
The definition supplies the hypothesis for the theorem possibility_actualization_adjoint, which simply applies it to recover the equivalence. It encodes the physical principle that properties propagate down the cost gradient to the minimal state, forming part of the modal layer that follows the forcing chain steps T5-T8. The status note indicates it is intended to be restricted later to cost-monotonic properties.
scope and limits
- Does not prove the adjointness holds for arbitrary properties.
- Does not define the possibility operator or the cost function J.
- Does not restrict the hypothesis to cost-monotonic properties.
- Does not supply a derivation or justification of the equivalence.
formal statement (Lean)
389def possibility_actualization_adjoint_hypothesis (p : ConfigProp) (c : Config) : Prop :=
proof body
Definition body.
390 (◇p) c ↔ p (A c)
391