rcl_is_counted_once_logic_on_positive_ratios
plain-language theorem explainer
Finite logical comparison on positive ratios forces the derived cost function to satisfy the RCL family predicate. Researchers deriving the Recognition Composition Law from Aristotelian logical constraints would cite this result. The proof is a direct term application of the upstream forcing theorem that converts finite logical comparison into an operative domain and then extracts the counted-once combiner.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ satisfy the finite logical comparison axioms (identity, non-contradiction, excluded middle, scale invariance, nontriviality). Then the derived cost $F(r) := C(r,1)$ belongs to the RCL family: there exist a combiner $P$ and constant $c$ such that $P(u,v) = 2u + 2v + c·u·v$ for all positive $u,v$ and $F$ obeys multiplicative consistency with $P$.
background
ComparisonOperator is the type of maps from pairs of positive reals to reals that assign a comparison cost. derivedCost converts such an operator into a one-variable function on positive ratios by fixing the second argument at the multiplicative identity 1. FiniteLogicalComparison packages five structural axioms: identity, non-contradiction, totality (excluded middle), scale invariance, and nontriviality; these encode classical logic as constraints on ratio comparisons. RCLFamily asserts that the resulting one-variable cost admits a bilinear combiner of the explicit affine form 2u + 2v + c uv together with multiplicative consistency. The module assembles the headline chain that scale-free comparison plus no-hidden-state finite logic yields the Recognition Composition Law.
proof idea
The proof is a one-line term wrapper that invokes finite_logical_comparison_forces_rcl C h. That upstream theorem first converts the finite logical comparison into an operative domain via finite_logical_to_operative, then applies counted_once_combiner_forces_rcl to obtain the RCLFamily predicate on the derived cost.
why it matters
This declaration completes one link in the main theorem package for logic as functional equation, showing that finite logical comparison on positive ratios directly produces the RCL family. It supports the Recognition Science program of extracting the composition law from logical axioms and sits inside the forcing chain that later reaches the eight-tick octave and three spatial dimensions. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.