ConsistentConfig
plain-language theorem explainer
ConsistentConfig introduces a structure for a proposition P paired with a positive real ratio that admits zero defect. Researchers deriving logic as cost minimization in Recognition Science cite it to separate stable single-assertion states from contradictions. The declaration is a bare structure with three fields and no proof body.
Claim. A consistent configuration consists of a proposition $P$ and a positive real ratio $r>0$.
background
The LogicFromCost module shows that logical consistency arises as the minimum-cost state under the Recognition Science cost landscape. Configurations are propositions assigned ratios whose defect measures departure from stability; zero defect occurs only at ratio 1. ConsistentConfig encodes the case of a single asserted proposition without its negation, in contrast to ContradictionConfig which forces both sides to ratio 1 simultaneously.
proof idea
The declaration is a structure definition with no proof body; it directly records the three fields P, ratio, and ratio_pos.
why it matters
ConsistentConfig supplies the type for the main results of the module: consistent_cost, consistent_zero_cost_possible, logic_from_cost, and why_logic_is_real. These theorems establish that only consistent configurations reach zero cost, while contradictions cannot, thereby grounding the claim that logic is the structure of cost-minimizing states. The construction aligns with the module's thesis that cost is foundational and logical consistency emerges from minimization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.