RouteIndependence
plain-language theorem explainer
RouteIndependence encodes that the symmetric composite cost for ratios xy and x/y equals a fixed quadratic polynomial in the separate costs. Researchers deriving physical laws from functional equations cite it as the Level-1 regularity condition on comparison operators before the upgrade to continuity. The definition directly imposes the polynomial form, symmetry from non-contradiction, and the d'Alembert composition law on the derived cost function.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator. Route independence holds if there exists a symmetric quadratic polynomial $P(u,v) = a + b u + c v + d u v + e u^2 + f v^2$ such that for all positive $x,y$, derivedCost$_C(xy) +$ derivedCost$_C(x/y) = P($derivedCost$_C(x),$ derivedCost$_C(y))$, where derivedCost$_C(r) := C(r,1)$.
background
A ComparisonOperator is a map from pairs of positive reals to reals that assigns a cost to comparing two quantities, subject to the four Aristotelian constraints. The derived cost is obtained by fixing the second argument to the multiplicative identity 1, yielding a function on positive ratios under scale invariance. In the LogicAsFunctionalEquation module this supplies the Level-1 regularity assumption that the symmetric forward-backward decomposition obeys a polynomial combiner. The setting draws on the d'Alembert inevitability results, which establish the functional-equation form on the multiplicative group of positive ratios.
proof idea
This is the direct definition of the route-independence property. It asserts existence of a quadratic polynomial P that is symmetric and satisfies the d'Alembert composition law on derived costs for all positive ratios. No lemmas are applied; the body simply unpacks the six coefficients and the two required equalities.
why it matters
RouteIndependence forms one field of the SatisfiesLawsOfLogic structure that bundles the Aristotelian constraints with scale invariance and non-triviality. It is invoked directly in the theorem that polynomial route-independence implies continuous route-independence and in the construction of LogicRealization from positive-ratio comparisons. Within the Recognition framework it supplies the Level-1 regularity step that precedes continuity, the Recognition Composition Law, and the forcing chain to the eight-tick octave and D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.