ConfigSpace
plain-language theorem explainer
The definition supplies the concrete set of all configurations whose value component is strictly positive. Modal logicians working on possibility statements cite it when instantiating the abstract configuration space for recognition-work arguments. It is realized as a direct set comprehension over the configuration structure.
Claim. $C = { c | 0 < c.value }$ where each $c$ belongs to the structure of recognition states carrying a positive real value, a natural-number time coordinate, and a bound on the absolute logarithm of the value.
background
The module develops modal logic over recognition states using a simplified configuration structure. A configuration consists of a positive real value (generalizing a bond multiplier), a time coordinate in ticks, and a logarithmic bound ensuring physical scale. The module doc notes this is a placeholder for a full LedgerState in later development.
proof idea
One-line definition via set comprehension that retains only those configurations whose value field satisfies the positivity constraint already present in the structure.
why it matters
This supplies the concrete population of configurations required by the abstract ConfigSpace class, the CostFunction structure, and the RecognitionWorkConstraintCert in CostFromDistinction. It is referenced by inconsistency-preservation theorems and by config_exists in RecogGeom.Core. The definition therefore grounds modal extensions of the recognition-work bridge and the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.