NonTrivial
plain-language theorem explainer
NonTrivial encodes that a comparison operator C on positive reals has at least one positive ratio whose derived cost is nonzero. Researchers formalizing logic as a functional equation cite it to exclude the zero-cost operator that would satisfy the other constraints vacuously. The definition is a direct existential quantification on the derived cost function obtained by fixing the second argument at the multiplicative identity.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator. Then $C$ is non-trivial when there exists $x > 0$ such that derivedCost$(C,x) ≠ 0$, where derivedCost$(C,x)$ is the cost of comparing $x$ to the multiplicative identity.
background
ComparisonOperator is the abbreviation for maps from pairs of positive reals to reals that assign a cost to comparing two quantities. DerivedCost is the one-argument function obtained by fixing the second argument at the multiplicative identity 1, yielding a well-defined cost on positive ratios once scale invariance is imposed.
proof idea
This is a definition. It directly states the existential condition ∃ x : ℝ, 0 < x ∧ derivedCost C x ≠ 0 using the derived cost extracted from the comparison operator.
why it matters
NonTrivial is required inside SatisfiesLawsOfLogic to ensure the derived cost is not the zero function. It appears in downstream structures including MagnitudeOfMismatch, OperativePositiveRatioComparison, FiniteLogicalComparison, and TruthEvaluableComparison. The definition prevents vacuous satisfaction of the Aristotelian constraints before scale invariance and route independence are imposed, supporting the passage from logic to the functional equation in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.