RouteIndependence
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assume continuity of C or of the derived cost.
- Does not fix the numerical values of the polynomial coefficients.
- Does not apply to zero or negative ratios.
- Does not incorporate non-triviality, which is stated separately.
- Does not yet imply the full Recognition Composition Law without further lemmas.
formal statement (Lean)
128def RouteIndependence (C : ComparisonOperator) : Prop :=
proof body
Definition body.
129 ∃ P : ℝ → ℝ → ℝ,
130 -- P is a polynomial in two variables of degree ≤ 2.
131 (∃ a b c d e f : ℝ, ∀ u v, P u v = a + b*u + c*v + d*u*v + e*u^2 + f*v^2) ∧
132 -- P is symmetric (consequence of non-contradiction at the combiner level).
133 (∀ u v, P u v = P v u) ∧
134 -- The d'Alembert composition law on the derived cost function.
135 (∀ x y : ℝ, 0 < x → 0 < y →
136 derivedCost C (x * y) + derivedCost C (x / y)
137 = P (derivedCost C x) (derivedCost C y))
138
139/-- A comparison operator is **non-trivial** if there exists at least one
140positive ratio with non-zero cost. (Without this assumption the constant zero
141function vacuously satisfies all the constraints.) -/