truth_eval_implies_composition
plain-language theorem explainer
Truth-evaluability of a comparison operator on positive reals implies finite pairwise polynomial closure. Derivations that move from semantic evaluation conditions to the Recognition Composition Law cite this step. The argument is a direct field projection from the TruthEvaluableComparison structure.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator. If $C$ satisfies the truth-evaluability conditions (self-evaluation to zero, single-valued reordering, continuous determinacy, scale invariance, and nontriviality), then $C$ obeys finite pairwise polynomial closure.
background
The module encodes the Reality ⇒ Logic direction of the functional-equation paper. ComparisonOperator is the type ℝ → ℝ → ℝ of cost functions on positive pairs. TruthEvaluableComparison C packages six semantic conditions; one of them, composite_determinate, is exactly the statement FinitePairwisePolynomialClosure C (defined upstream as RouteIndependence C).
proof idea
The proof is the one-line term hT.composite_determinate, which projects the corresponding field of the TruthEvaluableComparison hypothesis.
why it matters
The result is invoked by reality_satisfies_logic (which assembles all four logic laws) and by rcl_from_truth_evaluable_comparison (which extracts the multiplicative form of the Recognition Composition Law). It supplies the composite-determinate leg of the semantic-to-(L1)–(L4) translation inside the Logic Functional Equation paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.