ultimate_inevitability
plain-language theorem explainer
Ultimate inevitability establishes that symmetry under inversion, normalization at unity, and multiplicative consistency on the cost functional force it to equal the explicit J expression while pinning its combiner to the recognition composition law. Researchers deriving physical laws from minimal comparison axioms cite this to close the foundation. The term proof verifies the three properties directly for Jcost, exhibits the combiner, and applies the unconditional uniqueness lemma.
Claim. Let $F : (0,∞) → ℝ$. If $F$ satisfies symmetry ($F(x) = F(x^{-1})$ for $x > 0$), normalization ($F(1) = 0$), and multiplicative consistency (there exists $P$ such that $F(xy) + F(x/y) = P(F(x), F(y))$ for all $x,y > 0$), then $F(x) = (x + x^{-1})/2 - 1$ for $x > 0$ and any such $P$ obeys $P(u,v) = 2uv + 2u + 2v$ for $u,v ≥ 0$.
background
The module states the minimal foundation for cost functionals. IsSymmetricComparison encodes that the cost of ratio $x$ equals the cost of ratio $1/x$, which is the definition of symmetric comparison. IsNormalizedCost requires the cost at perfect match to vanish. HasMultiplicativeConsistency asserts existence of a combiner $P$ relating costs under multiplication and division. The local setting reduces five earlier assumptions to these three primitives plus regularity, with the theorem asserting uniqueness of both $F$ and $P$. Upstream, CostAxioms.Normalization supplies the unit-zero property and DAlembert.Inevitability supplies the unconditional uniqueness of the combiner.
proof idea
The term proof refines the five-way conjunction. Symmetry and normalization are discharged by simplification and ring arithmetic on the definition of Jcost. Multiplicative consistency is witnessed by exhibiting the explicit combiner $2uv+2u+2v$ and applying the lemma J_computes_P. The identification of Jcost with the explicit J expression follows by simplification. Uniqueness of the combiner is obtained directly from the unconditional result rcl_unconditional.
why it matters
This theorem supplies the tightest derivation of J-uniqueness and the recognition composition law from the three primitive requirements, showing no weaker set of assumptions still defines comparison cost. It completes the forcing-chain step that pins the cost measure and feeds the inevitability of the RCL throughout the framework. The result closes the minimal axiomatization with no remaining scaffolding in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.