rcl_direct_theorem
plain-language theorem explainer
The theorem establishes that any symmetric bi-affine combiner P consistent with the derived cost from an operative positive-ratio comparison must reduce to the form 2u + 2v + c0 uv. Researchers deriving the Recognition Composition Law from logic constraints would cite this for the counted-once subcase. The proof solves the system by substituting the identity element and a non-trivial ratio into the multiplicative consistency equation, then applies non-zero divisors to pin the linear coefficients.
Claim. Let $C$ be an operative positive-ratio comparison operator on positive reals. Let $P(u,v) = a + b u + c v + d u v$ be symmetric and satisfy multiplicative consistency with the derived cost $F(r) = C(r,1)$, i.e., $F(xy) + F(x/y) = P(F(x),F(y))$ for all positive $x,y$. Then there exists $c_0$ such that $P(u,v) = 2u + 2v + c_0 uv$ for all $u,v$.
background
A ComparisonOperator is a map from pairs of positive reals to reals that encodes the cost of comparing two quantities. The derivedCost function extracts the cost relative to the multiplicative identity by setting the second argument to 1, yielding a well-defined function on positive ratios under scale invariance. OperativePositiveRatioComparison packages the structural constraints: identity (cost zero when arguments match), non-contradiction, continuity, scale invariance, and non-triviality (existence of a ratio with non-zero cost). HasMultiplicativeConsistency states that the derived cost satisfies $F(xy) + F(x/y) = P(F(x),F(y))$ for the given combiner $P$. The module isolates the bi-affine counted-once subcase as a direct algebraic route to the Recognition Composition Law family, independent of the broader d'Alembert inevitability argument.
proof idea
The tactic proof first obtains a = 0 by evaluating consistency at (1,1) together with the identity property, which forces P(0,0) = 0. It then selects a non-trivial positive ratio x0 with t = derivedCost C x0 ≠ 0. Consistency at (x0,1) produces the linear relation t + t = a + b t; combined with a = 0 and mul_eq_zero this yields b = 2. Symmetry of P together with the same relation at swapped arguments forces c = 2. The remaining coefficient d is retained and the identity is verified by direct substitution and ring simplification.
why it matters
This declaration supplies the algebraic core for the counted-once route to the Recognition Composition Law. It is invoked directly by counted_once_combiner_forces_rcl to conclude that the derived cost satisfies the RCL family. The result closes the strict bi-affine subcase inside the LogicAsFunctionalEquation module and supplies an independent verification path that does not rely on the full d'Alembert inevitability theorem. Within the Recognition Science chain it confirms that the eight-tick octave and phi-ladder structure can be recovered from the functional equation once the combiner is forced into the canonical form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.