NonContradictionL
plain-language theorem explainer
Reciprocal symmetry for a two-argument comparison cost on recovered reals: whenever both arguments are positive, C(x,y) equals C(y,x). Anyone packaging the Law of Logic over LogicReal cites this structural field. It is a bare Prop definition (the non-contradiction / swap-symmetry axiom), not a derived theorem.
Claim. A comparison operator $C$ on recovered reals satisfies non-contradiction when, for all positive recovered reals $x$ and $y$, one has $C(x,y)=C(y,x)$.
background
This module is the recovered-real mirror of LogicAsFunctionalEquation. Comparison operators are binary maps $C:\mathrm{LogicReal}\to\mathrm{LogicReal}\to\mathrm{LogicReal}$. Structural Law-of-Logic fields (identity, symmetry, scale invariance, non-triviality) are stated natively on LogicReal; analytic regularity is transported through LogicReal.toReal.
LogicReal is the Cauchy completion of the recovered rationals, realized as a thin wrapper around Mathlib's completed reals so that global instances stay clean. Positivity and equality in the definition are the native LogicReal order and equality.
In the real-side twin, the same symmetry is called non-contradiction: the cost of comparing $x$ to $y$ must match the cost of comparing $y$ to $x$ on the positive cone. That is the reciprocal / swap symmetry of the J-cost comparison.
proof idea
No proof: this is a def whose body is a Prop. It simply packages the universal statement that $C$ is symmetric in its two positive arguments. Downstream lemmas unfold this definition and discharge the corresponding real-side field via transport.
why it matters
This is one of the four native structural fields of SatisfiesLawsOfLogicL (alongside identity, scale invariance, and non-triviality). The companion theorem nonContradictionL_to_real shows that any $C$ satisfying this Prop transports to a real comparison operator satisfying the already-verified real non-contradiction law.
In the broader Recognition chain, reciprocal symmetry of the comparison cost is part of the Law-of-Logic package that forces the J-cost shape (T5: $J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law. Stating it on recovered reals keeps the foundation self-contained before analytic transport.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.