Foundation Cost Axioms Composition Normalization Implies Symmetry

The symmetry of cost

In mathematics, a function's symmetry often hides a deeper structure. The declaration Composition_Normalization_implies_symmetry in the Recognition Science framework's machine-checked library of formal theorems proves exactly such a hidden symmetry. It shows that any cost function satisfying two plain conditions must treat a ratio and its reciprocal as equally costly. Formally, for any positive real number x, the cost at x equals the cost at 1/x.

The first condition is normalization: the cost of unity, the ratio 1, is zero. Perfect balance costs nothing. The second is a composition law, a d'Alembert functional equation: F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y) for all positive x and y. This equation forces multiplicative consistency, meaning the cost of a product and a quotient must relate to the costs of the parts in a fixed way. The theorem states that these two assumptions alone, without any continuity or smoothness requirement, imply the reciprocal symmetry F(x) = F(1/x).

This result is a stepping stone, not the destination. The full Recognition Science framework derives a unique cost function, J(x) = (x + 1/x)/2 - 1, from three axioms: normalization, the composition law, and a calibration condition on the second derivative. The symmetry theorem is a consequence of the first two axioms alone. It does not require the third, and it does not by itself identify the cost function. The uniqueness of J requires additional regularity hypotheses, such as continuity and convexity, which are not part of this declaration.

The practical meaning is that the framework's cost function, whatever its exact form, cannot favor one direction over its inverse. A ratio of 2 and a ratio of 1/2 carry the same cost. This symmetry is a structural constraint that any viable cost function must obey, and it emerges from the most basic assumptions about how recognition works.

/-- Composition + Normalization implies symmetry: F(x) = F(1/x).

    Proof: Apply Composition with x = 1:
    F(1 * y) + F(1 / y) = 2F(1)F(y) + 2F(1) + 2F(y)
    F(y) + F(1/y) = 2 * 0 * F(y) + 2 * 0 + 2F(y)  (by Normalization: F(1) = 0)
    F(y) + F(1/y) = 2F(y)
    F(1/y) = F(y)

    Therefore F(y) = F(1/y) for all y > 0, which is symmetry. -/
theorem Composition_Normalization_implies_symmetry (F : ℝ → ℝ) [Composition F] [Normalization F] :
    ∀ {x : ℝ}, 0 < x → F x = F x⁻¹ := by
  intro x hx
  -- Apply Composition with x = 1, y = x
  have h := Composition.dAlembert (F := F) 1 x one_pos hx
  -- F(1 * x) + F(1 / x) = 2F(1)F(x) + 2F(1) + 2F(x)
  -- Simplify: F(1) = 0, 1 * x = x, 1 / x = x⁻¹
  simp only [one_mul, one_div, Normalization.unit_zero, zero_mul, add_zero, mul_zero] at h
  -- h is now: F(x) + F(x⁻¹) = 2F(x)
  -- Subtracting F(x) from both sides: F(x⁻¹) = F(x)
  have h_symm : F x⁻¹ = F x := by
    have h_sub : F x⁻¹ = (F x + F x⁻¹) - F x := by ring
    rw [h_sub, h]
    ring
  exact h_symm.symm

What this page does not claim

The declaration does not identify the cost function J(x) = (x + 1/x)/2 - 1. The declaration does not require or use continuity, convexity, or any smoothness hypothesis. The declaration does not establish the calibration condition or any other third axiom.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/CostAxioms.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: