IsSymmetricComparison
plain-language theorem explainer
The declaration defines symmetric comparison for a cost function F as the property that F(x) equals F of its reciprocal for every positive real x. Researchers deriving minimal foundations for the Recognition Composition Law cite this when showing symmetry is definitional rather than an added assumption. The definition is a direct predicate with no lemmas or computational steps required.
Claim. A function $F : ℝ → ℝ$ is a symmetric comparison when $F(x) = F(x^{-1})$ holds for every $x > 0$.
background
The Ultimate Inevitability module reduces the derivation of the J-cost and Recognition Composition Law to three primitive requirements treated as definitional. Symmetry encodes what comparison means: comparing x to 1 is equivalent to comparing 1 to x. Normalization requires the cost at unity to vanish, while consistency encodes multiplicative structure via some combiner P.
proof idea
The declaration is a primitive definition that unfolds directly into the universal quantification over positive reals of the equality F(x) = F(x^{-1}). No upstream lemmas are applied; the body supplies the predicate itself.
why it matters
This definition underpins the ultimate inevitability theorem in the same module, which shows that symmetry, normalization, and multiplicative consistency plus regularity uniquely fix F as the J function and P as the RCL. It aligns with the forcing chain by treating symmetry as definitional, consistent with J-uniqueness and the eight-tick octave. The module documentation states there is no weaker foundation that still defines cost of comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.