non_contradiction_and_scale_imply_reciprocal
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assume continuity or excluded middle.
- Does not derive normalization F(1) = 0.
- Does not establish route independence or the full polynomial combiner.
- Applies only to positive real arguments.
- Does not address non-positive or zero arguments.
Lean usage
non_contradiction_and_scale_imply_reciprocal C hOp.non_contradiction hOp.scale_invariantformal statement (Lean)
185theorem non_contradiction_and_scale_imply_reciprocal
186 (C : ComparisonOperator)
187 (hNC : NonContradiction C)
188 (hSI : ScaleInvariant C) :
189 IsSymmetric (derivedCost C) := by
proof body
Tactic-mode proof.
190 intro x hx
191 have hxinv : (0 : ℝ) < x⁻¹ := inv_pos.mpr hx
192 have hx_ne : (x : ℝ) ≠ 0 := ne_of_gt hx
193 -- Step 1: C(x, 1) = C(1, x) by non-contradiction.
194 have h1 : C x 1 = C 1 x := hNC x 1 hx one_pos
195 -- Step 2: scale invariance with x' = 1, y' = x, λ = x⁻¹ gives
196 -- C(x⁻¹·1, x⁻¹·x) = C(1, x), so C(1, x) = C(x⁻¹·1, x⁻¹·x).
197 have h2 : C 1 x = C (x⁻¹ * 1) (x⁻¹ * x) :=
198 (hSI 1 x x⁻¹ one_pos hx hxinv).symm
199 -- Step 3: simplify x⁻¹·1 = x⁻¹ and x⁻¹·x = 1.
200 have h3 : C (x⁻¹ * 1) (x⁻¹ * x) = C x⁻¹ 1 := by
201 rw [mul_one, inv_mul_cancel₀ hx_ne]
202 show derivedCost C x = derivedCost C x⁻¹
203 unfold derivedCost
204 exact h1.trans (h2.trans h3)
205
206/-- **Translation lemma 3 (Excluded middle ⇒ Continuity)**: If a comparison
207operator is jointly continuous in both arguments on the positive quadrant,
208then the derived cost function is continuous on (0, ∞).
209
210The derivedCost C is the composition r ↦ (r, 1) ↦ C(r, 1). The pair-map is
211continuous everywhere; the uncurried C is continuous on the positive
212quadrant by ExcludedMiddle. The pair-map sends (0, ∞) into the positive
213quadrant. Hence the composition is continuous on (0, ∞). -/