IndisputableMonolith.Foundation.LogicAsFunctionalEquation.PositiveRatioForcing
PositiveRatioForcing defines the ratio-derived cost of two-argument comparisons and proves that scale-free comparisons on positive ratios force the RCL family. It isolates the ratio case inside the finite logical comparison setting. Researchers tracing the logic-to-functional-equation derivation cite it for the positive-ratio forcing step. The module consists of the ratioCost definition plus four short algebraic theorems that reduce directly to the upstream finite comparison axioms.
claimDefine the ratio-derived cost function $ratioCost(x,y)$ for positive real numbers $x,y$. Prove that scale-free comparison factors through the ratio, that the ratio factor is unique, that $ratioCost$ equals the derived cost, and that positive ratios are forced by scale-free comparison, thereby establishing that finite logical comparison on positive ratios forces the Recognition Composition Law family.
background
The module belongs to the LogicAsFunctionalEquation subpackage. It imports FiniteLogicalComparison, whose documentation states that finite logical comparison on positive ratios forces the RCL family, with the finite-pairwise-polynomial condition named as the finite algebraic content of logical comparison. The key definition introduced is ratioCost, the ratio-derived cost of a two-argument comparison. Related results establish that scale-free comparisons factor through this cost and that positive ratios are forced by such comparisons. The local theoretical setting is the derivation of the Recognition Composition Law from logical comparison axioms without hidden states, using only finite algebraic conditions on positive ratios.
proof idea
The module first defines ratioCost as the ratio-derived cost of a two-argument comparison. It proves that scale-free comparison factors through the ratio by algebraic reduction to the comparison axioms. Uniqueness of the ratio factor and equality of ratioCost to derivedCost follow from direct computation on the ratio. The forcing result that positive ratios are forced by scale-free comparison is obtained by applying the finite logical comparison axioms to the ratio cost. The module therefore consists of one definition and four theorems whose proofs are short algebraic arguments.
why it matters in Recognition Science
The module supplies the positive-ratio component of the formal chain collected in the MainTheorem package. That package's documentation lists the headline results: scale-free comparison factors through positive ratios, no-hidden-state finite comparison gives counted-once composition, and counted-once finite logical comparison forces the RCL family. It advances the paper's sharpened theorem on finite logical comparison forcing the RCL family by handling the ratio case explicitly. In the Recognition Science framework this step contributes to the forcing chain from T0 to the composition law that later yields the phi fixed point and the eight-tick octave.
scope and limits
- Does not address comparisons on non-positive numbers.
- Does not remove the finite-pairwise-polynomial condition from the logical comparison axioms.
- Does not derive the J-uniqueness formula or the phi self-similar fixed point.
- Does not compute numerical values for physical constants such as the fine-structure constant.