constZero_identity
plain-language theorem explainer
The constant-zero comparison operator satisfies the identity condition that comparing any positive real number to itself incurs zero cost. Researchers establishing the equivalence between distinguishability and non-triviality in the Recognition Science foundation cite this result. The proof is a direct term-mode reduction that introduces the argument and applies reflexivity.
Claim. The constant-zero comparison operator $C$, defined by $C(x,y)=0$ for all positive reals $x,y$, satisfies the identity property: for all $x>0$, $C(x,x)=0$.
background
In the NonTrivialityFromDistinguishability module the non_trivial field of SatisfiesLawsOfLogic is replaced by the more fundamental distinguishability condition. The Identity predicate is defined as the statement that comparing any positive real to itself costs zero, the direct mathematical counterpart of the Aristotelian law A = A. The constant-zero operator is the function that returns zero on every pair of positive arguments.
proof idea
The proof is a one-line term-mode wrapper. It introduces the positive real x, discards the positivity hypothesis, and applies reflexivity to obtain that the constant-zero function evaluates to zero on equal arguments.
why it matters
This result confirms that the trivial operator meets the identity requirement used in the equivalence between distinguishability and the original non-trivial predicate. It supports the module's replacement of an algebraic posit with Aristotelian content, keeping the framework aligned with the forcing chain from T0 to the derivation of D=3 and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.