IndisputableMonolith.Foundation.LogicAsFunctionalEquation.PositiveRatioForcing
PositiveRatioForcing introduces ratioCost as the cost of two-argument comparison on positive ratios and proves that scale-free comparison forces the RCL family. Researchers tracing the logic-to-functional-equation derivation cite it for the positive-ratio bridge step. The module structure defines ratioCost, shows its equivalence to derivedCost, and applies uniqueness from FiniteLogicalComparison to reach the forcing result.
claimDefine ratioCost$(x,y)$ as the cost extracted from positive-ratio comparisons. Then scale-free comparison on such pairs forces the family of solutions to $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$.
background
FiniteLogicalComparison packages the sharpened claim that finite logical comparison on positive ratios forces the RCL family, with the finite-pairwise-polynomial condition retained as the algebraic content of logical comparison. PositiveRatioForcing sits inside the same LogicAsFunctionalEquation development and supplies the ratio-specific cost and forcing lemmas. The setting is the Recognition Science chain in which scale-free comparison factors through positive ratios before reaching counted-once composition.
proof idea
The module first defines ratioCost together with scale_free_comparison_factors_through_ratio. It then proves ratioCost_eq_derivedCost and ratio_factor_unique by direct algebraic reduction, followed by positive_ratio_is_forced_by_scale_free_comparison via the upstream finite-comparison results.
why it matters in Recognition Science
The module supplies the positive-ratio forcing step required by MainTheorem, which assembles the headline chain: scale-free comparison factors through positive ratios, no-hidden-state finite comparison yields counted-once composition, and counted-once comparison forces the RCL family. It therefore closes one link in the formalization of logic as functional equation.
scope and limits
- Does not remove the finite-pairwise-polynomial condition.
- Does not treat non-positive ratios or infinite comparisons.
- Does not derive physical constants or spatial dimensions.