truth_eval_to_operative
plain-language theorem explainer
Truth-evaluable comparison operators on positive reals satisfy the operative positive-ratio comparison properties of identity, non-contradiction, continuity, scale invariance, and non-triviality. Workers on the Logic Functional Equation paper cite this to connect truth-evaluability directly to the encoded laws of logic. The proof is a term-mode structure construction that assembles each field from the corresponding implication lemma or hypothesis projection.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator. If $C$ is truth-evaluable (self-comparisons return zero, reordering is single-valued, the map is continuous on positive pairs, composites admit finite pairwise polynomial closure, the operator is scale-invariant, and it is nontrivial), then $C$ satisfies identity, non-contradiction, continuity (as excluded middle), scale invariance, and non-triviality.
background
A ComparisonOperator is an ℝ → ℝ → ℝ function giving the real-valued cost of comparing two positive quantities. TruthEvaluableComparison C is the structure whose fields are self-evaluability (C x x = 0), reorder single-valuedness (C x y = C y x), determinate continuity on the positive quadrant, finite pairwise polynomial closure for composites, scale invariance, and non-triviality. OperativePositiveRatioComparison C encodes the logical conditions identity, non-contradiction, continuity (as excluded middle), scale invariance, and non-triviality.
proof idea
The proof is a term-mode structure construction. It supplies the identity field via truth_eval_implies_identity C hT, the non_contradiction field via truth_eval_implies_non_contradiction C hT, the continuous field via truth_eval_implies_totality C hT, the scale_invariant field by direct projection of hT.scale_free, and the non_trivial field by direct projection of hT.nontrivial.
why it matters
This declaration supplies the bridge from truth-evaluable comparisons to operative ones, which is invoked in reality_satisfies_logic to conclude that such comparisons satisfy the laws of logic and in rcl_from_truth_evaluable_comparison to force the Recognition Composition Law family. It advances the Reality ⇒ Logic leg of the functional-equation framework, placing the logical conditions (L1)–(L4) on a truth-evaluable footing before the J-function and phi-ladder are introduced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.