ContradictionConfig
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not derive classical logic from physics; the ambient logic remains Lean's classical metalanguage.
- Does not compute explicit numerical J-cost values; only structures the ratios.
- Does not address continuous spectra or non-multiplicative recognizers.
- Does not claim that every physical system obeys the complementarity constraint.
formal statement (Lean)
100structure ContradictionConfig where
101 /-- The proposition P -/
102 P : Prop
103 /-- Ratio for P -/
104 ratio_P : ℝ
105 /-- Ratio for ¬P (should be complementary) -/
106 ratio_notP : ℝ
107 /-- Both ratios positive -/
108 ratio_P_pos : ratio_P > 0
109 ratio_notP_pos : ratio_notP > 0
110 /-- Complementarity: the product is 1 -/
111 complementary : ratio_P * ratio_notP = 1
112
113/-- The total cost of a contradiction is the sum of costs. -/