Cost

Reciprocal cost

Reciprocal cost is the quantity Recognition Science uses to measure how far a recognition event is from a perfect match. A recognition event compares two positive numbers, x and 1, where 1 is the reference. The cost is written J(x) and is defined as (x + 1/x)/2 - 1. At the reference, J(1) = 0, so a perfect match costs nothing. The formula is symmetric: J(x) = J(1/x), so swapping the two sides of the comparison does not change the cost. The cost is never negative for positive x, and it is zero only when x = 1.

The module establishes that this formula is not chosen. A theorem, T5_cost_uniqueness_on_pos, proves that any cost function satisfying five plain conditions must equal J(x). The conditions are reciprocal symmetry, zero cost at unity, a forced composition law, calibration, and continuity. The proof runs in the Lean 4 kernel and is axiom-clean. This uniqueness is the first link in the forcing chain that later derives the golden ratio, an eight-tick recognition cycle, 2^3, and three spatial dimensions.

The same module proves structural properties of J. It is strictly increasing for x above 1, so larger mismatches cost more. Near the reference, J(1 + ε) behaves like ε²/2, with a small error bounded by ε²/10 when |ε| ≤ 1/10. This quadratic behavior means small fluctuations are cheap, and the cost has a flat stationary point at the reference. The module also defines a related metric, Jmetric(x) = sqrt(2 * J(x)), which measures distance in the same space. This metric takes the value sqrt(1/2) at x = 2 and sqrt(4/3) at x = 3.

THEOREM T5_cost_uniqueness_on_pos · IndisputableMonolith/Cost.lean

THEOREM Jcost_unit0 · IndisputableMonolith/Cost.lean

THEOREM Jcost_symm · IndisputableMonolith/Cost.lean

THEOREM Jcost_nonneg · Jcost_zero_iff_one · IndisputableMonolith/Cost.lean

THEOREM Jcost_strict_mono_on_one_infty · IndisputableMonolith/Cost.lean

THEOREM Jcost_small_strain_bound · IndisputableMonolith/Cost.lean

What this page does not claim

Not a claim that this module derives the fine-structure constant alpha. Not a claim that the five conditions are the only possible axioms for a cost function. Not a claim that the physical interpretation of the cost as a ledger entry is established in this module.

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