truth_eval_implies_non_contradiction
plain-language theorem explainer
Truth-evaluability of a comparison operator on positive reals implies symmetry of the cost under argument swap. Researchers deriving logical axioms from reality structures in the Logic as Functional Equation paper cite this to obtain non-contradiction. The proof is a direct one-line extraction of the reorder_single_valued field from the hypothesis.
Claim. If a comparison operator $C$ is truth-evaluable, then it satisfies non-contradiction: $C(x,y)=C(y,x)$ for all positive real numbers $x,y$.
background
ComparisonOperator is an abbreviation for maps from pairs of positive reals to reals that assign a comparison cost. TruthEvaluableComparison is a structure whose fields include self-evaluation to zero, reorder_single_valued symmetry, continuity on the positive quadrant, and finite pairwise polynomial closure for composites. NonContradiction is the definition that encodes exactly this symmetry as the mathematical counterpart of the Aristotelian law of non-contradiction.
proof idea
The proof is a one-line wrapper that applies the reorder_single_valued field of the TruthEvaluableComparison hypothesis.
why it matters
This result is used by truth_eval_to_operative to construct OperativePositiveRatioComparison by supplying the non_contradiction component. It advances the Reality ⇒ Logic leg formalized in the module, translating semantic truth-evaluability into the structural condition NonContradiction. In the Recognition Science framework it supports the derivation of logic from the functional equation, consistent with the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.