route_independence_implies_multiplicative_consistency
plain-language theorem explainer
Route independence of a comparison operator on positive reals forces the derived cost function to satisfy multiplicative consistency with a symmetric quadratic polynomial combiner. Researchers closing the chain from Aristotelian logic to d'Alembert inevitability cite this extraction. The proof is a direct unpacking that obtains the polynomial witness and its properties straight from the route-independence hypothesis.
Claim. Let $C$ be a comparison operator on positive reals. If $C$ satisfies route independence, then there exists a symmetric quadratic polynomial $P$ such that the derived cost function $F$ (obtained by fixing the second argument of $C$ at the multiplicative identity) obeys $F(xy) + F(x/y) = P(F(x), F(y))$ for all positive $x, y$.
background
A ComparisonOperator is a map from pairs of positive reals to reals that encodes the cost of comparing two quantities. RouteIndependence asserts that the composite cost of comparing ratios $xy$ and $x/y$ equals some fixed quadratic polynomial $P$ evaluated at the individual costs, with $P$ required to be symmetric. The derived cost function is obtained by fixing the second argument of $C$ at 1, yielding a function on positive ratios that inherits scale invariance. HasMultiplicativeConsistency is the statement that this derived cost satisfies the composition law with the polynomial $P$. The local setting is the translation of the four Aristotelian constraints plus scale invariance into the hypotheses needed by the d'Alembert inevitability theorems.
proof idea
The term proof obtains the triple consisting of the polynomial $P$, its symmetry, and the consistency property directly from the RouteIndependence hypothesis on $C$. It then refines the existential quantifier by supplying exactly those three components, with the final consistency clause following by definition.
why it matters
This lemma supplies the multiplicative-consistency hypothesis required by bilinear_family_forced in the d'Alembert inevitability chain. It forms the technical bridge inside laws_of_logic_imply_dalembert_hypotheses, the Translation Theorem that converts the laws of logic into the normalized, symmetric, multiplicatively consistent cost function needed by washburn_uniqueness_aczel. The step therefore connects the Recognition Composition Law to the forcing of the J-cost function and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.