NonContradiction
plain-language theorem explainer
NonContradiction defines the property that any comparison operator C on positive reals obeys C(x, y) = C(y, x). Researchers deriving Aristotelian logic from the Recognition functional equation cite it when assembling the four constraints on comparison costs. The declaration is a direct Prop definition that encodes reciprocal symmetry of the cost without invoking lemmas or tactics.
Claim. A comparison operator $C : (0,∞) × (0,∞) → ℝ$ satisfies non-contradiction when $C(x,y) = C(y,x)$ holds for every pair of positive real numbers $x$ and $y$.
background
ComparisonOperator is the abbreviation ℝ → ℝ → ℝ for a map that assigns a real cost to any ordered pair of positive quantities. The module LogicAsFunctionalEquation treats this map as the carrier of the four Aristotelian constraints, with non-contradiction supplying the symmetry leg. The surrounding development reduces two-argument comparisons to a one-argument derived cost via scale invariance and the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). Upstream, LedgerFactorization calibrates J on the multiplicative group of positive ratios, while MultiplicativeRecognizerL4 supplies the concrete cost extraction used downstream.
proof idea
The declaration is a direct definition whose body is the universal statement ∀ x y : ℝ, 0 < x → 0 < y → C x y = C y x. No lemmas are applied and no tactics are executed; the Prop is literally the symmetry condition on the comparison operator.
why it matters
NonContradiction supplies the non_contradiction field required by SatisfiesLawsOfLogic and its continuous extension SatisfiesLawsOfLogicContinuous. It implements the symmetry half of T5 J-uniqueness in the forcing chain and is invoked by the translation lemma that derives reciprocity of the derived cost from non-contradiction plus scale invariance. The definition therefore closes the passage from the Recognition functional equation to the classical law ¬(A ∧ ¬A) expressed in cost language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.