truth_eval_implies_composition
Truth-evaluability of a comparison operator on positive reals implies that the operator satisfies finite pairwise polynomial closure. Researchers deriving the recognition composition law from semantic truth conditions cite this step to obtain route independence. The proof is a direct field projection from the truth-evaluability hypothesis.
claimIf $C$ is a comparison operator on positive reals that is truth-evaluable, then $C$ satisfies finite pairwise polynomial closure.
background
A comparison operator maps pairs of positive reals to a real-valued comparison cost. TruthEvaluableComparison is the structure whose fields encode self-evaluation to zero, single-valued reordering, continuity on positive pairs, and composite determinacy via finite pairwise polynomial closure. The module establishes the Reality to Logic implication by translating these semantic conditions into the encoded laws (L1)--(L4). Upstream, FinitePairwisePolynomialClosure is defined as route independence of the comparison.
proof idea
The proof is a one-line wrapper that projects the composite_determinate field from the TruthEvaluableComparison hypothesis.
why it matters in Recognition Science
This result supplies the closure property used by rcl_from_truth_evaluable_comparison to derive the recognition composition law family and by reality_satisfies_logic to confirm that truth-evaluable comparisons satisfy the laws of logic. It advances the Reality implies Logic leg of the framework, connecting truth-evaluable structures to the functional equation that forces J-uniqueness and the phi fixed point.
scope and limits
- Does not derive the explicit multiplicative form of the composition law.
- Does not separately establish scale invariance or nontriviality.
- Does not address continuity implications in isolation.
Lean usage
theorem example_application (C : ComparisonOperator) (hT : TruthEvaluableComparison C) : FinitePairwisePolynomialClosure C := truth_eval_implies_composition C hTformal statement (Lean)
57theorem truth_eval_implies_composition
58 (C : ComparisonOperator)
59 (hT : TruthEvaluableComparison C) :
60 FinitePairwisePolynomialClosure C :=
proof body
Term-mode proof.
61 hT.composite_determinate
62
63/-- Truth-evaluable comparisons are operative positive-ratio comparisons. -/