finite_logical_comparison_forces_rcl
plain-language theorem explainer
Finite logical comparison on positive ratios forces the derived cost to satisfy the RCL family. Researchers closing the logical-to-composition step in Recognition Science cite this to link Aristotelian axioms to the functional equation. The proof is a one-line term application of counted_once_combiner_forces_rcl after extracting the operative and counted-once properties.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator. If $C$ satisfies identity, non-contradiction, excluded middle, scale invariance, nontriviality, and counted-once algebra, then the derived cost $F(r) := C(r,1)$ lies in the RCL family: there exist $P : ℝ → ℝ → ℝ$ and $c ∈ ℝ$ such that $F$ is multiplicatively consistent with $P$ and $P(u,v) = 2u + 2v + c·u·v$ for all $u,v$.
background
ComparisonOperator is an abbrev for maps ℝ → ℝ → ℝ that assign a real cost to comparing two positive quantities. derivedCost extracts the one-variable function by fixing the second argument at the multiplicative identity 1, yielding a cost on positive ratios. RCLFamily asserts existence of a combiner P and constant c making the cost multiplicatively consistent with the specific bilinear form 2u + 2v + c uv.
proof idea
The proof is a one-line term that applies counted_once_combiner_forces_rcl to the operative property obtained from finite_logical_to_operative C h and the counted-once property obtained from finite_logical_has_counted_once C h.
why it matters
This supplies the sharpened implication that finite logical comparison forces the RCL family on the derived cost. It is invoked directly by rcl_is_counted_once_logic_on_positive_ratios and scale_free_counted_once_logic_forces_ratio_rcl. In the framework it completes the passage from the Aristotelian constraints to the Recognition Composition Law that precedes the phi-ladder and eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.