Cost Real Character Factorization Nontrivial Character Value Principal On Nat

The principal character value

The theorem nontrivialCharacterValue_principal_on_nat concerns a quantity called the nontrivial character value, which is a real number extracted from a cost function. A cost function, in the Recognition Science framework, assigns a real number to each ratio of two quantities, representing the cost of recognizing one from the other. The theorem states that if the cost function satisfies a set of plain hypotheses (called SansAnchorHypotheses) and if the doubled trace at 2 is not equal to 2, then for every positive integer n, the nontrivial character value at n is at least 1.

The condition that the doubled trace at 2 is not 2 is what makes the character value "nontrivial." If the doubled trace at 2 were exactly 2, the cost function would behave like the trivial character, which assigns the value 1 to everything. The theorem excludes this case, ensuring that the extracted value is genuinely informative. The conclusion, that the value is at least 1 for all positive integers, is a lower bound: it says the extracted value never dips below 1, no matter which positive integer you evaluate it at.

This theorem is proved in the machine-checked library of formal theorems, meaning it has been verified by a computer to follow from the stated hypotheses using only the standard axioms of logic. It does not claim that the nontrivial character value is exactly 1, nor that it is bounded above. It does not claim that the value is positive for all rational numbers, only for positive integers. It also does not claim that the cost function itself is unique or that it equals the specific form J(x) = (x + 1/x)/2 - 1; that is a separate theorem with additional hypotheses.

The practical upshot is that within the Recognition Science framework, any cost function meeting the hypotheses and not collapsing to the trivial case will produce a nontrivial character value that is always at least 1 on the positive integers. This is a structural guarantee that the extracted value is not zero or negative on the natural numbers, which is a necessary condition for interpreting it as a meaningful character in the factorization theory.

theorem nontrivialCharacterValue_principal_on_nat
    {F : RatioOrbit → RatioOrbit} (hF : SansAnchorHypotheses F)
    (hnontrivial : rationalTrace F 2 ≠ 2) :
    ∀ n : ℕ, 1 ≤ n → 1 ≤ nontrivialCharacterValue F n := by
  intro n hn
  let u := nontrivialCharacterValue F n
  let r := anchorRoot F
  have hu : 0 < u := nontrivialCharacterValue_pos_on_nat hF hnontrivial hn
  have hr : 1 < r := anchorRoot_gt_one hF hnontrivial
  by_contra hprincipal
  have hu1 : u < 1 := lt_of_not_ge hprincipal
  obtain ⟨k, hdecrease⟩ := exists_pow_trace_decrease hu hu1 hr
  have hnpowPos : 0 < n ^ k := pow_pos (by omega) k
  have hnpowOne : 1 ≤ n ^ k := hnpowPos
  have hnatMono :=
    nontrivialCharacterValue_nat_trace_mono hF hnontrivial
      hnpowOne (by omega : n ^ k ≤ 2 * n ^ k)
  have hnq : (n : ℚ) ≠ 0 := by exact_mod_cast (show n ≠ 0 by omega)
  have hpowq : (n : ℚ) ^ k ≠ 0 := pow_ne_zero k hnq
  have hcharPow := nontrivialCharacterValue_pow hF hnontrivial hnq k
  have hcharTwoPow :=
    nontrivialCharacterValue_mul hF hnontrivial
      (by norm_num : (2 : ℚ) ≠ 0) hpowq
  have hcastPow : (((n ^ k : ℕ) : ℚ)) = (n : ℚ) ^ k := by norm_num
  have hcastTwoPow :
      (((2 * n ^ k : ℕ) : ℚ)) = (2 : ℚ) * (n : ℚ) ^ k := by norm_num
  rw [hcastPow, hcastTwoPow, hcharPow, hcharTwoPow,
    nontrivialCharacterValue_two hF hnontrivial, hcharPow] at hnatMono
  change u ^ k + (u ^ k)⁻¹ ≤
    r * u ^ k + (r * u ^ k)⁻¹ at hnatMono
  exact (not_lt_of_ge hnatMono) hdecrease

What this page does not claim

The nontrivial character value is exactly 1 for all positive integers. The nontrivial character value is positive for all rational numbers. The cost function itself is uniquely determined by the hypotheses used in this theorem.

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: