CostMonotonic
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.