NonContradictionOn
plain-language theorem explainer
Non-contradiction on a comparison operator C over an ordered field K requires that C(x,y) equals C(y,x) for all positive x and y. Researchers closing the loop from the Law of Logic to the reals cite this as one of the four Aristotelian conditions packaged inside LogicSupported. The declaration is a direct definition of the Prop with no lemmas or reductions applied.
Claim. For a comparison operator $C : K → K → K$ on a linearly ordered field $K$, non-contradiction holds when $∀ x,y ∈ K$, if $0 < x$ and $0 < y$ then $C(x,y) = C(y,x)$.
background
DomainBootstrap establishes the bootstrap theorem for the comparison-operator domain. The module recovers an ordered field supporting the Law of Logic and shows it must be isomorphic to the reals once Archimedean and Dedekind-completeness hypotheses are added. ComparisonOperatorOn is the abbreviation for maps of type $K → K → K$ that serve as comparison operators on a linearly ordered field.
proof idea
This is a direct definition of the Prop. The body is the universal statement quantifying over positive elements and requiring symmetry of C on them. No tactics, lemmas, or reductions are invoked.
why it matters
NonContradictionOn supplies one of the four Aristotelian conditions inside the LogicSupported structure. That structure feeds the uniqueness theorem showing any ordered field admitting such a C is canonically isomorphic to R. In the Recognition Science framework the step ensures the comparison operator meets minimal logical consistency before the phi-ladder and forcing chain derive constants and dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.