Cost Real Character Factorization

The factorization

In mathematics, a character is a function that turns multiplication into multiplication: χ(x·y) = χ(x)·χ(y). The sign function on the real line is the simplest example, sending every positive number to 1 and every negative number to −1. Cost real character factorization is the Recognition Science result that any cost function satisfying the framework's plain conditions secretly contains such a character, even when the cost itself is built from addition and division.

The framework's cost measures the price of a recognition event, a discrete record of a comparison. Its composition law, which forces how costs combine, is a doubled-trace identity: F(x·y) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y). The factorization result shows that this identity alone, without any anchor at the number two, implies that a related doubled trace obeys the cleaner d'Alembert equation T(x·y) + T(x/y) = T(x)·T(y). That equation is the classical signature of a multiplicative character, and the result is proved twice: once from the full native cost hypotheses and once from the weaker sans-anchor hypotheses that drop the value at two.

The theorem rationalTrace_dAlembert states the identity on rational inputs, while traceDisplay_dAlembert and doubledTrace_dAlembert_of_sansAnchor carry it to the framework's orbit objects. A ratio orbit is an equivalence class of ratios under the framework's own equality, and the trace display is the real-valued reading of the doubled trace. The sans-anchor version matters because it shows the multiplicative core does not depend on a special value at two; the structure is forced by the composition law itself.

The framework then builds the character explicitly. The anchor root is the positive root of the trace at two, and the nontrivial character value is extracted by a linear combination that cancels the additive part. Theorems nontrivialCharacterValue_two and nontrivialCharacterValue_principal_on_nat confirm the extraction lands on the expected values: at two it equals the anchor root, and on positive integers it stays at least one. The sign character, which sends zero to zero and otherwise the sign, is proved multiplicative in rationalSignCharacter_mul, giving the full factorization of the cost into a positive character and a sign factor.

In plain language, the framework establishes that the cost of recognition, despite its additive-looking definition, has a multiplicative skeleton. This is what lets the framework later force the golden ratio and the eight-tick cycle: the character is the hidden ruler that the cost must respect. The result is a theorem in the framework's machine-checked library, with the sans-anchor version extending the reach to a broader class of cost functions.

theorem doubledTrace_dAlembert_of_sansAnchor
    {F : RatioOrbit → RatioOrbit}
    (hF : SansAnchorHypotheses F)
    {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)) :=
  doubledTrace_dAlembert_of_rcl hF.base_sans_two.canonical_rcl hx hy

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

theorem rationalSignCharacter_mul (x y : ℚ) :
    rationalSignCharacter (x * y) =
      rationalSignCharacter x * rationalSignCharacter y := by
  by_cases hx : x = 0
  · subst x
    simp [rationalSignCharacter]
  by_cases hy : y = 0
  · subst y
    simp [rationalSignCharacter]
  have hxy : x * y ≠ 0 := mul_ne_zero hx hy
  rcases lt_or_gt_of_ne hx with hxneg | hxpos
  · rcases lt_or_gt_of_ne hy with hyneg | hypos
    · have hxypos : 0 < x * y := mul_pos_of_neg_of_neg hxneg hyneg
      simp [rationalSignCharacter, hx, hy, hxy, hxneg.not_gt, hyneg.not_gt,
        hxypos]
    · have hxyneg : x * y < 0 := mul_neg_of_neg_of_pos hxneg hypos
      simp [rationalSignCharacter, hx, hy, hxy, hxneg.not_gt, hypos,
        hxyneg.not_gt]
  · rcases lt_or_gt_of_ne hy with hyneg | hypos
    · have hxyneg : x * y < 0 := mul_neg_of_pos_of_neg hxpos hyneg
      simp [rationalSignCharacter, hx, hy, hxy, hxpos, hyneg.not_gt,
        hxyneg.not_gt]
    · have hxypos : 0 < x * y := mul_pos hxpos hypos
      simp [rationalSignCharacter, hx, hy, hxy, hxpos, hypos, hxypos]

theorem nontrivialCharacterValue_two
    {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
    (hnontrivial : rationalTrace F 2 ≠ 2) :
    nontrivialCharacterValue F 2 = anchorRoot F := by
  have htwo : (2 : ℚ) ≠ 0 := by norm_num
  have hd := rationalTrace_dAlembert hF htwo htwo
  have hprod : (2 : ℚ) * 2 = 4 := by norm_num
  have hquot : (2 : ℚ) / 2 = 1 := by norm_num
  rw [hprod, hquot, rationalTrace_one hF] at hd
  have hfour :
      rationalTrace F 4 = rationalTrace F 2 ^ 2 - 2 := by
    nlinarith [hd]
  have hr0 := anchorRoot_ne_zero hF
  have hrden := anchorRoot_sq_sub_one_ne_zero hF hnontrivial
  have hA : rationalTrace F 2 =
      (anchorRoot F ^ 2 + 1) / anchorRoot F := by
    rw [← anchorRoot_add_inv hF, eq_div_iff hr0]
    field_simp [hr0]
  rw [nontrivialCharacterValue, linearExtraction,
    show (2 : ℚ) * 2 = 4 by norm_num, hfour, hA]
  field_simp [hr0, hrden]
  ring

What this page does not claim

The framework does not prove the uniqueness of the cost function J(x) = (x + 1/x)/2 - 1. The sans-anchor result does not require the value at two to be two, but it does not rule out that value either. The factorization does not by itself force the golden ratio; that requires additional steps in the forcing chain.

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: