constZero_nonContradiction
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove that constant zero is excluded from the framework.
- Does not address the distinguishability condition.
- Does not generalize the result beyond the constant-zero operator.
formal statement (Lean)
192theorem constZero_nonContradiction : NonContradiction constZero := by
proof body
Term-mode proof.
193 intro x y _ _; rfl
194
195/-- Constant zero is continuous on the positive quadrant. -/