constZero_not_distinguishable
plain-language theorem explainer
The constant-zero comparison operator fails distinguishability because it returns zero for every pair of positive reals. Foundation researchers cite this result to exclude the vacuous operator that satisfies the Aristotelian conditions only trivially. The proof is a direct term-mode contradiction: the distinguishability witness supplies a nonzero cost that reflexivity immediately falsifies against the constant definition.
Claim. Let $C$ be the constant-zero comparison operator, defined by $C(x,y)=0$ for all real $x,y$. Then there do not exist positive reals $x,y$ such that $C(x,y)≠0$.
background
The module replaces the non_trivial field inside SatisfiesLawsOfLogic with the more primitive Aristotelian notion of distinguishability. Distinguishability for a comparison operator $C$ asserts the existence of positive reals $x,y$ with $C(x,y)≠0$, ensuring comparison is operative rather than vacuous. The constant-zero operator is defined as the function that returns zero on every pair and is known to satisfy identity while remaining the trivial case that must be ruled out.
proof idea
The term proof assumes distinguishability of constZero, unpacking the existential witness to obtain a proof $h$ that the cost is nonzero. It then applies reflexivity to equate the cost with zero, yielding an immediate contradiction that discharges the assumption.
why it matters
This result closes the trivial case so that non-triviality becomes a corollary of distinguishability under identity, non-contradiction and scale invariance, as described in the module documentation. It supports the surrounding equivalence theorems that promote the non_trivial posit to a derived fact, keeping the foundation free of arbitrary algebraic stipulations. Within Recognition Science it ensures the comparison operator extracted from the functional equation is genuinely operative before further structure such as the phi-ladder is imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.