Cost Real Character Factorization Real Character Candidate Small Traces Rational

The rational trace

A trace is a numerical value attached to a ratio, and the doubled trace is simply twice that value. The theorem rationalTrace_dAlembert states a clean algebraic identity: for any nonzero rational numbers x and y, the doubled trace of x times y plus the doubled trace of x divided by y equals the doubled trace of x multiplied by the doubled trace of y. In symbols, T(xy) + T(x/y) = T(x)T(y), where T denotes the doubled trace. This is a d'Alembert-style functional equation, named for the 1747 work of Jean le Rond d'Alembert on the composition of forces.

The result is proved from the framework's reciprocal composition law, which states that the cost of recognizing a product of two ratios relates to the costs of recognizing each ratio individually. The key insight is that this law alone, without needing the value at the anchor point two, forces the doubled trace to satisfy the multiplicative identity. This is a theorem in the machine-checked library of formal theorems, meaning it is verified by a computer to follow from the stated hypotheses. The proof does not use any additional assumptions beyond the reciprocal composition law itself.

In Recognition Science, this theorem is a stepping stone. It shows that the doubled trace behaves like a multiplicative character on the positive rationals, a structure that is well understood in classical mathematics. This is a necessary step toward the framework's goal of showing that the cost function J(x) = (x + 1/x)/2 - 1 is the unique function satisfying its defining conditions. The theorem does not, however, establish the full cost function or its uniqueness; it only establishes the multiplicative property of the doubled trace under the given hypotheses.

What the declaration does not claim is just as important. It does not claim that the doubled trace is a character for all real numbers, only for rationals. It does not claim that the reciprocal composition law alone forces the cost function to be J; that requires additional hypotheses. And it does not claim that the theorem applies to any function whatsoever, only to those satisfying the framework's SansAnchorHypotheses, which include the reciprocal composition law and a monotonicity condition on positive integer orbits.

theorem rationalTrace_dAlembert
    {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
    {x y : ℚ} (hx : x ≠ 0) (hy : y ≠ 0) :
    rationalTrace F (x * y) + rationalTrace F (x / y) =
      rationalTrace F x * rationalTrace F y := by
  let ox := ratioOrbitOfRat x
  let oy := ratioOrbitOfRat y
  have hox : ox.toRat ≠ 0 := by
    change (ratioOrbitOfRat x).toRat ≠ 0
    rw [ratioOrbitOfRat_toRat]
    exact hx
  have hoy : oy.toRat ≠ 0 := by
    change (ratioOrbitOfRat y).toRat ≠ 0
    rw [ratioOrbitOfRat_toRat]
    exact hy
  have hd := traceDisplay_dAlembert hF hox hoy
  have hmul :
      traceDisplay F (RatioOrbit.mul ox oy) = rationalTrace F (x * y) := by
    symm
    apply traceDisplay_eq_of_crossEq hF
    rw [RatioOrbit.crossEq_iff_toRat_eq, ratioOrbitOfRat_toRat,
      RatioOrbit.mul_toRat]
    change x * y = (ratioOrbitOfRat x).toRat * (ratioOrbitOfRat y).toRat
    rw [ratioOrbitOfRat_toRat, ratioOrbitOfRat_toRat]
  have hdiv :
      traceDisplay F (div ox oy) = rationalTrace F (x / y) := by
    symm
    apply traceDisplay_eq_of_crossEq hF
    rw [RatioOrbit.crossEq_iff_toRat_eq, ratioOrbitOfRat_toRat, div_toRat]
    change x / y = (ratioOrbitOfRat x).toRat / (ratioOrbitOfRat y).toRat
    rw [ratioOrbitOfRat_toRat, ratioOrbitOfRat_toRat]
  simpa [rationalTrace, ox, oy, hmul, hdiv] using hd

/-- The doubled-trace form of the composition law needs only the RCL. The anchor
at two is not used. -/
theorem doubledTrace_dAlembert_of_rcl
    {F : RatioOrbit → RatioOrbit}
    (hrcl : ∀ {x y : RatioOrbit}, x.toRat ≠ 0 → y.toRat ≠ 0 →
      RatioOrbit.crossEq
        (RatioOrbit.add (F (RatioOrbit.mul x y)) (F (div x y)))
        (RatioOrbit.add
          (RatioOrbit.add
            (RatioOrbit.mul two (RatioOrbit.mul (F x) (F y)))
            (RatioOrbit.mul two (F x)))
          (RatioOrbit.mul two (F y))))
    {x y : RatioOrbit} (hx : x.toRat ≠ 0) (hy : y.toRat ≠ 0) :
    RatioOrbit.crossEq
      (RatioOrbit.add (nativeCostDoubledTrace F (RatioOrbit.mul x y))
        (nativeCostDoubledTrace F (div x y)))
      (RatioOrbit.mul (nativeCostDoubledTrace F x) (nativeCostDoubledTrace F y)) := by
  have h := hrcl hx hy
  rw [RatioOrbit.crossEq_iff_toRat_eq] at h ⊢
  simp only [nativeCostDoubledTrace, doubledTraceValue, RatioOrbit.mul_toRat,
    RatioOrbit.add_toRat, two_toRat, RatioOrbit.one_toRat] at h ⊢
  linarith

What this page does not claim

The theorem does not claim the doubled trace is a character for all real numbers, only for rationals. The reciprocal composition law alone does not force the cost function to be J; additional hypotheses are required. The theorem applies only to functions satisfying the framework's SansAnchorHypotheses, not to arbitrary functions.

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