constZero_not_nonTrivial
plain-language theorem explainer
The constant-zero operator on positive ratios fails the non-triviality predicate required by the logic-as-functional-equation framework. Foundational researchers cite this to justify replacing the non-triviality posit with distinguishability as the primitive Aristotelian commitment. The proof is a direct term-mode contradiction obtained by introducing the non-triviality structure and resolving its witness field against reflexivity.
Claim. The constant-zero comparison operator does not satisfy the non-triviality predicate, i.e., the derived cost function is identically zero on all positive ratios.
background
In LogicAsFunctionalEquation the SatisfiesLawsOfLogic structure carries a non_trivial field asserting that the derived cost function is not identically zero on positive ratios. The constant-zero operator satisfies the four core Aristotelian conditions vacuously, so an extra commitment is needed to exclude it. This module replaces that algebraic posit with distinguishability, the claim that there exists at least one pair of distinct positive quantities whose comparison cost is non-zero. Under identity, non-contradiction and scale invariance the two formulations become equivalent, so non-triviality is now a corollary rather than a primitive.
proof idea
Term-mode proof. The intro tactic extracts the three-field structure of NonTrivial constZero; the third field h encodes the non-zero witness. Applying h to reflexivity produces an immediate contradiction, discharged by exact.
why it matters
This theorem completes the reduction of the residual posit in SatisfiesLawsOfLogic to a genuinely Aristotelian statement, enabling the canonical formulation SatisfiesLawsOfLogicCanonical. It sits inside the move from T0 to T8 in the unified forcing chain and supports the Recognition Composition Law by ensuring the cost function J is non-degenerate before the phi-ladder and eight-tick octave are derived. No open scaffolding remains on this specific exclusion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.