constZero_continuous
plain-language theorem explainer
The declaration establishes that the constant-zero comparison operator satisfies the continuity requirement of ExcludedMiddle on the positive quadrant. Foundation researchers cite it when confirming that the trivial operator meets structural conditions before distinguishability excludes it from SatisfiesLawsOfLogic. The proof is a one-line term wrapper that unfolds the definition and invokes the standard continuity of constant functions.
Claim. The constant-zero comparison operator defined by $C(x,y) := 0$ is continuous on $(0,∞) × (0,∞)$.
background
The NonTrivialityFromDistinguishability module replaces the non_trivial field in SatisfiesLawsOfLogic with the Aristotelian distinguishability predicate. ExcludedMiddle is the upstream definition requiring that every comparison operator C be continuous when viewed as a function on positive ratios: ContinuousOn (Function.uncurry C) (Set.Ioi 0 ×ˢ Set.Ioi 0). The constant-zero operator is introduced as constZero x y := 0, which vacuously meets identity and non-contradiction but must still be checked against continuity and scale invariance.
proof idea
The proof is a one-line term-mode wrapper. It unfolds ExcludedMiddle to obtain the continuity statement on the positive quadrant, then applies the library lemma continuousOn_const to the constant function.
why it matters
This result verifies that constZero satisfies the continuity half of ExcludedMiddle, isolating distinguishability as the sole condition that rules out the trivial operator. It supports the module's equivalence between nonTrivial and distinguishability under Identity, Non-Contradiction, and Scale Invariance. In the Recognition framework it closes the algebraic reformulation step that converts the original posit into genuinely Aristotelian content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.