Foundation Rs Uniqueness Master Thm3

What the module proves

In mathematics, a cost function measures the price of a transition or a difference. A natural requirement is that the cost of moving from a quantity to itself should be zero, and that cost should never be negative. The ledger of formal results proves exactly these two properties for a specific cost function, plus a third fact about a threshold constant. All three are verified step by step in a machine-checked library.

The cost function in question is J(x) = (x + 1/x)/2 - 1. The domain cost is defined as J applied to the ratio m/e. The first theorem states that when m equals e, the ratio is 1, and J(1) equals 0. The second theorem states that for positive m and e, the cost is nonnegative. The third theorem states that the golden ratio phi minus 3/2 is positive, which is a threshold used elsewhere in the framework. These are the three facts established.

In Recognition Science, the framework models physical structure as forced by a unique cost function. This result is part of that project, but it does not by itself connect the cost to any physical quantity. The variables m and e are left undefined here. The proof works for any real numbers, but the meaning of those numbers as masses, energies, or other physical quantities is not established. The result is a template, shared verbatim with many sibling modules, waiting for a definition of m and e in a specific subject's terms.

What this means in plain language: the result proves three general facts about a cost function, facts that are true for any positive inputs. It does not prove that any particular physical system obeys this cost. The research note attached to the result says the idea was meant to connect to physical constants, but the formal content stops at the three general properties. This is a clean, verified foundation, but the bridge to physics is a separate step.

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

This module does not prove any statement about specific physical constants or particle masses. The module does not establish that any real-world system actually follows this cost function. The uniqueness of J itself is not proved in this module, only referenced in a research note.

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