Config
plain-language theorem explainer
Configurations model points in recognition state space as positive reals with bounded logarithm and natural-number time ticks. Modal logic and cost-function developments cite this structure when building state spaces from the simplified LedgerState representation. The definition is a direct structure with four fields: value, positivity proof, time, and log bound.
Claim. A configuration is a tuple consisting of a positive real number $v > 0$ (value), a natural number $t$ (time in ticks), and the bound $|$log $v| |$ ≤ 16.
background
Recognition Science treats configurations as points in state space, here simplified from LedgerState for modal development per the module doc-comment. The value field generalizes bond multipliers, time uses the native units abbrev from RSNativeUnits, and the log bound keeps scales between exp(-16) and exp(16). Upstream results include the seven-element list of plot families, the set of eight kinship systems, nuclear density tiers on the phi-ladder, and LedgerFactorization structures for (R+, ×) with J-calibration.
proof idea
The declaration is a structure definition introducing four fields with their types and constraints. No proof body exists; it is a def_or_abbrev.
why it matters
This supplies the base type for ConfigSpace and CostFunction in CostFromDistinction, supporting additive theorems on independent joins and the recognition-work constraint via calibration structures. It advances modal possibility by providing concrete state space, linking to the phi-forcing chain (T5 J-uniqueness, T7 eight-tick octave) and RCL. Downstream doc-comments note its role in enabling cost additivity over three pairwise-independent configurations and strict inequalities for inconsistent pairs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.