finite_logical_to_truth_evaluable
plain-language theorem explainer
Finite logical comparison on positive ratios yields truth-evaluable comparison structure. Researchers deriving functional equations for logic from comparison costs would cite this embedding step. The proof is a direct term construction that maps the six logical axioms onto the four evaluability fields and invokes the counted-once polynomial lemma for the composite condition.
Claim. Let $C: (0,∞) × (0,∞) → ℝ$ be a comparison operator. If $C$ satisfies identity ($C(x,x)=0$), non-contradiction (symmetry), totality (excluded middle), scale invariance, nontriviality, and counted-once algebra, then $C$ is truth-evaluable: it obeys self-evaluation at zero cost, symmetry under argument swap, continuity on the positive quadrant, and finite pairwise polynomial closure for composite values.
background
ComparisonOperator abbreviates maps from positive reals to reals that return the cost of comparing two quantities; under scale invariance this descends to the multiplicative group of positive ratios. FiniteLogicalComparison is the structure requiring identity, non-contradiction, totality, scale invariance, nontriviality, and counted-once algebra (the finite algebraic content of logical comparison). TruthEvaluableComparison supplies the minimal semantic structure for evaluating statements about such comparisons, with fields for self-evaluation, reordering, continuity, and composite determinacy via finite polynomials. The module packages the sharpened claim that finite logical comparison forces the RCL family while retaining the finite-pairwise-polynomial condition as necessary.
proof idea
The proof is a term-mode record construction of TruthEvaluableComparison. It assigns self_evaluable directly from the identity field, reorder_single_valued from non_contradiction, determinate_continuous from totality, scale_free from scale_invariant, and nontrivial from the corresponding hypothesis field. The composite_determinate field is supplied by applying the upstream lemma counted_once_to_finite_pairwise_polynomial to the counted_once_algebra component of the hypothesis.
why it matters
This declaration supplies the embedding of finite logical comparison into the truth-evaluable structure required for semantic evaluation inside the Recognition framework. It directly supports the module theorem that finite logical comparison on positive ratios forces the RCL family. The parent results are the TruthEvaluableComparison definition and the counted-once polynomial closure lemma. It fills the sharpened paper claim that the finite algebraic condition cannot be removed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.