Cost Jcost Logic Composition Law L To Real

The transport mirror

The declaration compositionLawL_to_real establishes a transport mirror. It takes a function that satisfies the Recognition Science composition law on the framework's abstract recovered reals, a number system built from logical primitives, and shows that the same function, when translated to ordinary real numbers, satisfies the standard real-number composition law. The proof is a formal bridge: it reduces the abstract statement to the already-verified real theorem surface through the translation map toReal.

The composition law itself is the forced constraint on any recognition cost. Written in symbols, it demands that for all positive x and y, F(x·y) + F(x/y) = 2·F(x)·F(y) + 2·F(x) + 2·F(y). This equation encodes how the cost of recognizing a product or quotient of two quantities relates to the costs of recognizing each separately. The canonical reciprocal cost J(x) = (x + 1/x)/2 - 1 satisfies this law, and the uniqueness theorem proves it is the only continuous solution.

What the declaration does not claim is equally precise. It does not prove the uniqueness theorem on recovered reals; that result lives on the real side and is transported across. It does not establish that every function satisfying the law is a valid cost, only that the law itself transfers faithfully. And it says nothing about whether recovered reals are the right number system for physics, which remains a modeling choice.

In Recognition Science, this bridge matters because the framework's foundational theorems are proved on recovered reals, while classical physics speaks in ordinary real numbers. The transport mirror ensures that a cost function verified in the abstract setting behaves identically when interpreted concretely. Without it, the framework's results would risk being artifacts of its number system rather than genuine mathematical facts.

/-- Transported RCL: a recovered-real composition law becomes the existing
real composition law under `toReal`. -/
theorem compositionLawL_to_real {F : LogicReal → LogicReal}
    (hF : SatisfiesCompositionLawL F) :
    Cost.FunctionalEquation.SatisfiesCompositionLaw (transportCost F) := by
  intro x y hx hy
  unfold transportCost
  have hxL : (0 : LogicReal) < fromReal x := by
    rw [lt_iff_toReal_lt, toReal_zero, toReal_fromReal]; exact hx
  have hyL : (0 : LogicReal) < fromReal y := by
    rw [lt_iff_toReal_lt, toReal_zero, toReal_fromReal]; exact hy
  have hxy : fromReal x * fromReal y = fromReal (x * y) := by
    rw [eq_iff_toReal_eq]
    simp [toReal_fromReal]
  have hdiv : fromReal x / fromReal y = fromReal (x / y) := by
    rw [eq_iff_toReal_eq]
    simp [toReal_fromReal]
  have hL := hF (fromReal x) (fromReal y) hxL hyL
  rw [hxy, hdiv] at hL
  have h := congrArg toReal hL
  simpa [toReal_add, toReal_mul, toReal_div, toReal_fromReal] using h

theorem JcostL_symm {x : LogicReal} (hx : (0 : LogicReal) < x) :
    JcostL x = JcostL x⁻¹ := by
  rw [eq_iff_toReal_eq, toReal_JcostL, toReal_JcostL, toReal_inv]
  have hx' : 0 < toReal x := by simpa [lt_iff_toReal_lt] using hx
  exact Jcost_symm hx'

What this page does not claim

The declaration does not prove uniqueness of J on recovered reals. It does not assert that recovered reals are the correct number system for physics. It does not claim every solution to the composition law is a valid cost function.

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