RCLFamily
plain-language theorem explainer
RCLFamily characterizes one-variable derived costs F that obey multiplicative consistency with a bilinear combiner of the explicit form 2u + 2v + c u v. Researchers deriving the Recognition Composition Law from counted-once comparisons on positive ratios would cite this predicate when closing the algebraic step from operative logic to the functional equation. The definition is a direct existential statement over the combiner P and scalar c with no additional proof steps.
Claim. A function $F : ℝ → ℝ$ belongs to the RCL family if there exists a combiner $P : ℝ → ℝ → ℝ$ and a constant $c ∈ ℝ$ such that $F(xy) + F(x/y) = P(F(x), F(y))$ for all positive $x, y$ and $P(u, v) = 2u + 2v + c · u · v$.
background
The CountOnceComparison module formalizes the requirement that each constituent comparison is counted once. This means the combiner for two component costs u and v must be affine in each variable separately, taking the general form a + b u + c v + d u v. Identity and symmetry conditions then restrict the combiner to the RCL-family form shown in the definition. Upstream, HasMultiplicativeConsistency from DAlembert.Inevitability states that F(xy) + F(x/y) = P(F(x), F(y)) for positive arguments; the same predicate appears in DAlembert.Ultimate as the definition of multiplicative consistency.
proof idea
This is a direct definition. It asserts the existence of a combiner P satisfying HasMultiplicativeConsistency together with the explicit bilinear form 2u + 2v + c u v.
why it matters
RCLFamily is the algebraic target for the forcing theorems counted_once_combiner_forces_rcl and finite_logical_comparison_forces_rcl, which show that operative positive-ratio comparisons yield this family. It appears in the main chain results operative_domain_rcl_logic_reality_chain and rcl_is_counted_once_logic_on_positive_ratios. The predicate closes the step from counted-once logic to the Recognition Composition Law, aligning with T5 J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.