constZero_not_distinguishable
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove distinguishability for any operator other than the constant-zero case.
- Does not invoke scale invariance or the remaining Aristotelian laws.
- Does not connect the result to the phi-ladder, mass formula or physical constants.
- Does not supply a general criterion for when an arbitrary operator satisfies distinguishability.
formal statement (Lean)
205theorem constZero_not_distinguishable : ¬ Distinguishability constZero := by
proof body
Term-mode proof.
206 intro ⟨_, _, _, _, h⟩
207 exact h rfl
208
209/-- Constant zero fails non-triviality. -/