PropConfig
plain-language theorem explainer
PropConfig pairs a proposition with a positive real ratio that encodes its degree of presence or balance in the cost landscape. Researchers deriving logical consistency from minimization in Recognition Science reference this structure when classifying stable versus unstable assertions. The declaration is introduced directly as a structure with three fields: the proposition, the ratio value, and its positivity witness.
Claim. A propositional configuration consists of a proposition $P$ together with a positive real number $r > 0$ that measures the balance or presence of $P$, where $r = 1$ corresponds to perfect stability, $r$ approaching 0 corresponds to absence, and $r$ approaching infinity corresponds to instability.
background
The module shows that logical consistency arises as the minimum-cost configuration within the Recognition Science cost landscape. PropConfig is the basic structure that pairs any proposition with its ratio; the ratio is the argument to the defect function that yields the configuration cost. Upstream definitions supply the necessary cost primitives: ObserverForcing.cost gives the J-cost of a recognition event, MultiplicativeRecognizerL4.cost and PhiForcingDerived.of supply the derived cost on positive ratios, and LedgerFactorization.of calibrates the underlying J function.
proof idea
This is a structure definition that introduces the three fields prop, ratio, and ratio_pos with no further proof obligations or computational content.
why it matters
PropConfig supplies the type used by IsStable (prop_cost c = 0) and IsUnstable (prop_cost c > 0), which in turn support the demonstration that contradictions carry infinite cost. It therefore occupies the first step in the module argument that consistency is the minimum-cost structure and that logic emerges from J-cost minimization. The construction aligns with the eight-tick octave and phi-ladder machinery already fixed in the upstream forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.