scale_free_counted_once_logic_forces_ratio_rcl
plain-language theorem explainer
Finite logical comparison operators on positive reals factor their values through the ratio x/y and induce the RCL family on the derived cost. Researchers tracing the Recognition Science derivation from logic axioms to the composition law would cite this to close the scale-free counted-once segment. The proof is a one-line term pairing of the scale-free factoring lemma with the finite-comparison-to-RCL theorem.
Claim. Let $C$ be a comparison operator on positive reals satisfying the finite logical comparison axioms (identity, non-contradiction, excluded middle, scale invariance, nontriviality). 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)$ satisfies the RCL family property.
background
ComparisonOperator abbreviates maps from pairs of positive reals to reals that encode the cost of comparing two quantities under four Aristotelian constraints. derivedCost extracts the one-variable function by fixing the second argument at 1, producing a well-defined map on positive ratios once scale invariance holds. FiniteLogicalComparison packages the structure requiring identity, non-contradiction, excluded middle, scale invariance, and nontriviality for finite logical comparisons on positive ratios. RCLFamily asserts that the derived cost admits a combiner P satisfying HasMultiplicativeConsistency and the affine form P(u,v) = 2u + 2v + c u v. The module collects the headline chain for logic as functional equation: scale-free comparisons factor through ratios, no-hidden-state finite comparisons yield counted-once composition, and counted-once finite logical comparisons force the RCL family.
proof idea
The proof is a direct term-mode wrapper. It applies scale_free_comparison_factors_through_ratio to C and the scale_invariant field of the FiniteLogicalComparison hypothesis to obtain the factoring through ratios, then applies finite_logical_comparison_forces_rcl to C and the full hypothesis to obtain the RCLFamily predicate on derivedCost C.
why it matters
This declaration supplies the scale-free counted-once link that feeds directly into the alias theorem rcl_is_scale_free_counted_once_logic_on_positive_ratios. It advances the Recognition Science program by deriving the Recognition Composition Law from finite logical axioms on positive ratios, consistent with the T0–T8 forcing chain and the RCL identity. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.