ContradictionConfig
plain-language theorem explainer
ContradictionConfig packages a proposition P together with complementary positive ratios r and 1/r that would be required to assert both P and ¬P. Researchers working on the emergence of logic from cost minimization cite it as the canonical data type for unstable configurations. The declaration is a plain structure definition that simply records the proposition, the two ratios, their positivity, and the product-one constraint.
Claim. A contradiction configuration consists of a proposition $P$, positive reals $r_P>0$ and $r_{¬P}>0$ satisfying $r_P·r_{¬P}=1$, where $r_P$ is the ratio assigned to the assertion of $P$ and $r_{¬P}$ the ratio assigned to the assertion of $¬P$.
background
The module LogicFromCost shows that logical consistency arises as the minimum of a cost functional J. A proposition is represented by a configuration whose stability is measured by defect distance to the fixed point of the Recognition Composition Law; zero defect means the ratio equals 1 and the configuration is stable. Upstream, the cost of any recognition event is defined as the J-cost of its state (ObserverForcing.cost) and the cost induced by a multiplicative recognizer is the derivedCost of its comparator (MultiplicativeRecognizerL4.cost). PhiForcingDerived.of supplies the underlying J-cost structure on positive reals. The local setting is therefore classical metalanguage used to prove that positive-cost object-level configurations cannot be simultaneously asserted and negated.
proof idea
This is a structure definition with no proof body. It simply bundles the proposition P, the two ratios, the two positivity hypotheses, and the complementarity equation ratio_P * ratio_notP = 1.
why it matters
ContradictionConfig is the input type for contradiction_cost, contradiction_positive_cost, IsLogicalContradiction and the main theorem logic_from_cost. Those results establish that any such configuration has strictly positive total defect and therefore cannot stabilize, which is the precise content of the claim that logic is the structure of cost-minimizing states. The construction directly supports the Recognition Science thesis that consistency (rather than contradiction) occupies the zero-cost minima of the J-landscape.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.