rcl_from_truth_evaluable_comparison
A truth-evaluable comparison operator C on positive reals yields a derived cost function that satisfies multiplicative consistency with some quadratic polynomial combiner P(u, v) = 2u + 2v + c u v. Researchers working on the Logic Functional Equation paper cite this result to close the implication from semantic truth-evaluability to the algebraic RCL family. The argument is a direct one-line application of the polynomial closure theorem after the truth-evaluability hypothesis is translated into operative and finite-pairwise conditions.
claimLet $C$ be a truth-evaluable comparison operator. Then there exist a real number $c$ and a function $P : ℝ → ℝ → ℝ$ such that the derived cost $F(r) := C(r, 1)$ satisfies $F(xy) + F(x/y) = P(F(x), F(y))$ for all positive reals $x, y$, and moreover $P(u, v) = 2u + 2v + c · u v$.
background
A comparison operator maps pairs of positive reals to reals and encodes the cost of comparing two quantities. The derived cost is the slice obtained by fixing the second argument at the multiplicative identity, so $F(r) = C(r, 1)$. TruthEvaluableComparison is the structure requiring self-comparisons to evaluate to zero, symmetry under reordering, continuity on the positive quadrant, finite pairwise polynomial closure for composites, scale invariance, and nontriviality. The module formalises the Reality-to-Logic direction by showing that truth-evaluability implies the four logical conditions (L1)–(L4). The upstream rcl_polynomial_closure_theorem states that any operative positive-ratio comparison possessing finite pairwise polynomial closure has a derived cost obeying the RCL family; HasMultiplicativeConsistency is the predicate asserting the existence of a combiner $P$ such that $F(xy) + F(x/y) = P(F(x), F(y))$.
proof idea
The proof is a one-line wrapper that invokes rcl_polynomial_closure_theorem on the comparison operator C. It supplies the operative positive-ratio comparison hypothesis by calling truth_eval_to_operative C hT and the finite pairwise polynomial closure hypothesis by calling truth_eval_implies_composition C hT, which simply projects the composite_determinate field out of the TruthEvaluableComparison assumption.
why it matters in Recognition Science
This declaration completes the derivation of the Recognition Composition Law family directly from truth-evaluable comparisons, thereby discharging the Reality ⇒ Logic leg of the Logic-as-Functional-Equation paper. It rests on the d’Alembert inevitability results for multiplicative consistency and supplies the algebraic content needed for downstream claims such as reality_satisfies_logic. Within the Recognition Science chain it supplies the bridge from semantic evaluation structures to the functional equation that forces J-uniqueness and the phi-ladder.
scope and limits
- Does not fix the numerical value of the constant c.
- Does not extend beyond finite pairwise polynomial closure.
- Applies only to scale-invariant continuous comparison operators on positive reals.
- Does not derive the explicit form of the J-cost or the phi fixed point.
- Does not address non-polynomial or infinite composite closures.
formal statement (Lean)
85theorem rcl_from_truth_evaluable_comparison
86 (C : ComparisonOperator)
87 (hT : TruthEvaluableComparison C) :
88 ∃ (P : ℝ → ℝ → ℝ) (c : ℝ),
89 DAlembert.Inevitability.HasMultiplicativeConsistency (derivedCost C) P ∧
90 (∀ u v, P u v = 2 * u + 2 * v + c * u * v) :=
proof body
Term-mode proof.
91 rcl_polynomial_closure_theorem C
92 (truth_eval_to_operative C hT)
93 (truth_eval_implies_composition C hT)
94
95end LogicAsFunctionalEquation
96end Foundation
97end IndisputableMonolith