CostMonotonic
CostMonotonic defines properties of configurations that transfer from any higher-J-cost element to a lower-J-cost element whenever the target value is positive. Modal physicists working on actualization in Recognition Science cite the definition when establishing inheritance of properties at the J-minimizing actualized state. The declaration is a direct definition that encodes downward propagation along the cost ordering with no further proof content.
claimA property $p$ of configurations is cost-monotonic when, for all configurations $y$ and $y'$, $p(y)$ together with $J(y.value) > J(y'.value)$ and $y'.value > 0$ implies $p(y')$, where $J$ is the cost function on the positive real value carried by each configuration.
background
In the Modal.Actualization module, a configuration is a structure carrying a positive real value field together with a positivity witness. ConfigProp is the abbreviation for the type of predicates on such configurations. The actualization operator A returns the configuration of minimal J-cost inside the possibility set of its argument. The cost function J is supplied by the upstream definitions in MultiplicativeRecognizerL4 (derived cost of a comparator on positive ratios) and ObserverForcing (Jcost of a recognition-event state). This local setting sits inside the Recognition Science development of modal operators over recognition states.
proof idea
The declaration is a direct definition. It introduces the predicate by writing the universal quantification over pairs of configurations and the three-premise implication that encodes propagation down the J-cost gradient. No lemmas are invoked and no tactics are executed.
why it matters in Recognition Science
CostMonotonic is the hypothesis required by adjoint_from_cost_monotonic and possibility_actualization_adjoint_monotonic, which together prove the equivalence (◇p) c ↔ p (A c) precisely for this class of properties. It therefore supplies the missing link that lets the actualization operator inherit properties from any higher-cost possibility. In the broader framework the definition connects cost minimization at T5 (J-uniqueness) to the modal adjointness step that precedes the derivation of D = 3 and the eight-tick octave. It leaves open the question of which physically realized properties satisfy the monotonicity condition.
scope and limits
- Does not assert that every property of configurations is cost-monotonic.
- Does not compute or bound the numerical value of the cost function J.
- Does not treat configurations whose value is non-positive.
- Does not establish existence or uniqueness of the actualization operator A.
formal statement (Lean)
280def CostMonotonic (p : ConfigProp) : Prop :=
proof body
Definition body.
281 ∀ y y' : Config, p y → J y.value > J y'.value → y'.value > 0 → p y'
282
283/-- For cost-monotonic properties, adjointness holds from any higher-cost element. -/