non_contradiction_and_scale_imply_reciprocal
plain-language theorem explainer
Non-contradiction together with scale invariance on a comparison operator C imply that its derived cost F(r) := C(r,1) satisfies F(x) = F(x^{-1}) for all x > 0. Researchers extracting d'Alembert data from Aristotelian constraints cite this translation lemma. The argument is a direct three-step equality chain that rewrites arguments via scaling and symmetry, then unfolds the derived-cost definition.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator. If $C(x,y) = C(y,x)$ for all $x,y > 0$ and $C(λx, λy) = C(x,y)$ for all $λ > 0$, then the derived cost $F(r) = C(r,1)$ obeys $F(x) = F(x^{-1})$ for every $x > 0$.
background
ComparisonOperator is the type ℝ → ℝ → ℝ that assigns a real cost to any pair of positive quantities. NonContradiction requires the cost to be unchanged under argument swap, while ScaleInvariant requires the cost to depend only on the ratio of the two arguments. derivedCost extracts the one-argument function r ↦ C(r,1), which is well-defined on positive ratios once scale invariance holds. IsSymmetric is the predicate ∀ x > 0, F x = F x^{-1}, imported from the d'Alembert inevitability module where it appears as the symmetry half of the normalized cost data.
proof idea
The tactic proof fixes x > 0, obtains the positive inverse, and builds three equalities. Non-contradiction supplies C(x,1) = C(1,x). Scale invariance with factor x^{-1} supplies C(1,x) = C(x^{-1}·1, x^{-1}·x). The two multiplications simplify to C(x^{-1},1) by mul_one and inv_mul_cancel. Transitivity of equality after unfolding derivedCost yields the required symmetry.
why it matters
The lemma supplies the symmetry component needed by laws_of_logic_imply_dalembert_hypotheses, which packages the four Aristotelian constraints into the hypotheses of the d'Alembert inevitability theorem. It is applied verbatim inside operative_derived_cost_symmetric and indirectly inside log_aczel_data_of_laws. The result therefore forms one link in the chain that converts logical constraints into the functional equation whose solutions produce the Recognition Science constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Softmax normalization creates attention sinks in language models
"After relaxing such dependence by replacing softmax attention with other attention operations, such as sigmoid attention without normalization, attention sinks do not emerge in LMs up to 1B parameters."