Foundation Reciprocity Symmetry

The symmetry at the base

Reciprocity symmetry is a simple property a comparison cost can have: the cost of comparing one item to another equals the cost of comparing them in the opposite order. If comparing a book to a pen costs some amount of effort, comparing the pen to the book costs the same. In the framework's notation, this is J(x) = J(1/x) for every positive x, where J is the cost function and x is the ratio of the two things being compared.

This symmetry is one of five plain conditions that together force the cost function to have a single possible form. The other conditions are that comparing something to itself costs zero, that costs compose in a forced way, that the function is calibrated, and that it is continuous. When all five hold, the cost function must be J(x) = (x + 1/x)/2 - 1. Reciprocity symmetry is the condition that rules out any function that treats the two orders of comparison differently.

The function J has two immediate consequences. First, it vanishes when the two inputs are equal, so comparing something to itself costs nothing. Second, it is never negative for positive inputs, so no comparison has a negative cost. Both facts follow directly from the definition of J and are proved in the framework's machine-checked library of formal theorems.

In Recognition Science, this symmetry sits at the base of a longer chain. The unique cost function leads to the golden ratio as a self-similar scaling, an eight-tick recognition cycle, and three spatial dimensions. Reciprocity symmetry is the first gate in that chain: if the cost of comparing A to B did not equal the cost of comparing B to A, none of the later structure would follow.

The framework's library also defines a threshold value, phi - 3/2, and proves it is positive. This threshold is a constant that appears in the framework's internal calculations, and its positivity is a small but necessary fact for later steps in the forcing chain. The library proves these facts about J itself, not about any particular subject, because the cost function is defined generally as J(m/e) for any two real numbers m and e.

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

What this page does not claim

The module proves facts about a specific subject, since it defines cost only as J(m/e) without defining m and e in any particular domain. Reciprocity symmetry alone forces the cost function; the other four conditions are also required. The framework derives the fine-structure constant alpha from this symmetry.

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/Reciprocity_Symmetry.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: