ConfigProp
plain-language theorem explainer
ConfigProp is the type of predicates on configurations in the modal possibility layer. Modal actualization results cite it to state properties such as Determined or CostMonotonic that separate necessary from contingent features under cost minimization. The declaration is a direct type alias with no computational content or additional axioms.
Claim. Let $C$ be the space of configurations. Then ConfigProp is the type of all maps $p : C → Prop$.
background
A configuration is a structure with a positive real value (generalizing bond multipliers), a natural-number time coordinate in ticks, and a logarithmic bound |log(value)| ≤ 16 that keeps values within physically relevant scales. The Modal.Possibility module builds a modal logic in which necessity (□p) means the property holds for every possible future, interpreted as cost-forced outcomes.
proof idea
The declaration is a one-line abbreviation that directly sets ConfigProp equal to the function type Config → Prop.
why it matters
ConfigProp supplies the predicate type used throughout the Actualization submodule to define Determined (properties true for all cost-minimal successors) and Contingent (properties that fail in some degenerate possibility). It therefore anchors the modal treatment of necessity as cost minimization, consistent with the Recognition framework's forcing chain and J-cost structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.