rcl_is_scale_free_counted_once_logic_on_positive_ratios
plain-language theorem explainer
Any finite logical comparison operator on positive reals factors through the ratio of its arguments, and the derived cost satisfies the RCL family predicate. Researchers formalizing the Recognition Science derivation of logic from functional equations cite this as the terminal step in the main theorem chain. The proof is a direct one-line application of the preceding scale-free forcing theorem.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ satisfy the finite logical comparison axioms. Then there exists $F : ℝ → ℝ$ such that $C(x,y) = F(x/y)$ for all $x>0$, $y>0$, and the derived cost $r ↦ C(r,1)$ belongs to the RCL family.
background
ComparisonOperator is an abbrev for ℝ → ℝ → ℝ encoding the cost of comparing two positive quantities under the four Aristotelian constraints. FiniteLogicalComparison is the structure collecting identity, non-contradiction, excluded middle, scale invariance, and nontriviality. derivedCost extracts the one-variable function by fixing the second argument at 1, which is well-defined once scale invariance holds. RCLFamily asserts that this cost admits a multiplicative consistency combiner of the explicit bilinear form 2u + 2v + c uv.
proof idea
The proof is a one-line wrapper that applies scale_free_counted_once_logic_forces_ratio_rcl to the supplied comparison operator and its FiniteLogicalComparison hypothesis.
why it matters
This declaration is the final named alias in the MainTheorem module, closing the chain from scale-free counted-once logic on positive ratios to the RCL family. It packages the headline result of the module documentation and supplies the formal link between finite logical comparison and the Recognition Composition Law that appears in the T5 J-uniqueness step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.