constZero
plain-language theorem explainer
The constant-zero comparison operator returns zero cost for every pair of positive reals. It is cited by researchers establishing the equivalence between distinguishability and non-triviality as the vacuous case that meets the Aristotelian conditions yet yields the zero cost function. The definition is a direct one-line abbreviation of the comparison operator type.
Claim. Let a comparison operator be any function from pairs of positive reals to the reals. The constant-zero operator is the map sending every such pair to zero.
background
A comparison operator assigns a real-valued cost to any pair of positive quantities and must obey the Aristotelian constraints of identity (zero cost when the arguments are equal), non-contradiction, and scale invariance. The module replaces the non_trivial posit inside SatisfiesLawsOfLogic with the more primitive distinguishability condition, which requires that at least one pair of distinct positive quantities receives non-zero cost. The constant-zero operator is introduced precisely to exhibit the case in which comparison is vacuous and the derived cost function is identically zero.
proof idea
This is a one-line definition that directly instantiates the comparison operator type by returning the constant function zero on every input pair.
why it matters
The definition supplies the canonical counterexample used to prove that distinguishability is strictly stronger than the bare Aristotelian laws, feeding directly into the downstream results constZero_not_distinguishable and constZero_not_nonTrivial. It closes the gap described in the module documentation by showing why the residual non_trivial field must be replaced by distinguishability, thereby making the framework rest on genuinely Aristotelian content rather than an algebraic reformulation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.