constZero_nonContradiction
plain-language theorem explainer
The constant-zero comparison operator satisfies non-contradiction, returning equal costs for any pair of positive reals in either order. Foundation researchers cite this result to confirm the trivial operator meets the symmetry axiom before distinguishability excludes it from SatisfiesLawsOfLogic. The proof is a direct one-line term application of reflexivity after introducing the positive inputs.
Claim. The constant-zero comparison operator $C(x,y) := 0$ satisfies non-contradiction: for all positive real numbers $x$ and $y$, $C(x,y) = C(y,x)$.
background
The NonTrivialityFromDistinguishability module replaces the non-triviality field in SatisfiesLawsOfLogic with the Aristotelian notion of distinguishability. NonContradiction is the symmetry property requiring that the cost of comparing x to y equals the cost of comparing y to x, as defined in LogicAsFunctionalEquation. The constant-zero operator is the function that returns zero for every pair of positive reals.
proof idea
The proof is a one-line term-mode wrapper. It introduces positive reals x and y, discards the positivity hypotheses, and applies reflexivity to the equality 0 = 0.
why it matters
This theorem verifies that the constant-zero operator satisfies non-contradiction, allowing it to be treated as a candidate that meets the Aristotelian conditions before distinguishability rules it out in the same module. It supports the shift from positing non-triviality to deriving it as a corollary from distinguishability under identity, non-contradiction, and scale invariance. No downstream uses appear in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.