Foundation Primitive Recognition Calculus Prime Axis Coherence Log Char Log

The logarithm as a character

The natural logarithm, written ln(n), is the familiar function that turns multiplication into addition: ln(m·n) = ln(m) + ln(n). It also has a less familiar property that matters here. Because every whole number factors uniquely into primes, the logarithm of any number can be built by adding up contributions from its prime factors. For example, ln(12) = ln(2·2·3) = 2·ln(2) + ln(3). This decomposition is the classical foundation of number theory, and it is the property the Recognition Science framework's declaration logChar_log formalizes.

The framework starts with a more general idea. A ledger, a discrete record of events, assigns a real number, called a weight, to each prime number. From those weights one can define a log-character: the value it assigns to any whole number n is the sum of its prime weights, each multiplied by how many times that prime appears in n's factorization. This construction is free in a precise sense. Any choice of prime weights extends to a function that respects multiplication, and distinct choices give distinct functions. The framework proves these facts as theorems in its machine-checked library.

The declaration logChar_log then pins down what happens when the weights are chosen to be the logarithms of the primes themselves. In that case, the log-character is exactly the ordinary real logarithm: for every nonzero natural number n, the sum of prime-log contributions equals ln(n). This is not an approximation or a numerical coincidence. It is a proved identity, derived from the definition of the log-character and the fundamental theorem of arithmetic.

In Recognition Science, this identity is the bridge between the abstract ledger and a familiar continuous scale. The framework's broader account shows that a global power law, a rule of the form nᶜ, holds exactly when the prime weights are aligned to a reference scale. When that reference scale is w(p) = ln(p), the synchronized character becomes the power map n ↦ nᶜ. The declaration logChar_log is the specific instance where the exponent is 1, so the character is just the logarithm itself. It establishes that the real logarithm is the canonical reference scale that the framework's order and continuum conditions select.

The declaration does not claim that the logarithm is the only possible character, nor that the prime weights are forced to be logarithms by the definition of the log-character alone. It only states what happens when the weights are chosen to be logarithms. The framework's theorems about freedom and independence show that other weight assignments are perfectly consistent with the additive structure. The logarithm emerges as special only when the additional coherence condition, the alignment to a single global scale, is imposed.

/-- With the reference weights `w(p) = log p`, the log-character is exactly the
real logarithm. This is the scale that the order/continuum condition selects. -/
theorem logChar_log (n : ℕ) (hn : n ≠ 0) :
    logChar (fun p => Real.log p) n = Real.log n := by
  unfold logChar
  rw [Finsupp.sum]
  have hself : n.factorization.prod (fun p k => p ^ k) = n :=
    Nat.factorization_prod_pow_eq_self hn
  have hcast : (n : ℝ) = ∏ p ∈ n.factorization.support, ((p : ℝ) ^ (n.factorization p)) := by
    conv_lhs => rw [← hself, Finsupp.prod]
    push_cast
    rfl
  rw [hcast, Real.log_prod]
  · apply Finset.sum_congr rfl
    intro p hp
    rw [Real.log_pow]
  · intro p hp
    have hpp : p.Prime := by
      rw [Nat.support_factorization] at hp
      exact Nat.prime_of_mem_primeFactors hp
    have : (0 : ℝ) < (p : ℝ) ^ (n.factorization p) := by
      apply pow_pos
      exact_mod_cast hpp.pos
    exact ne_of_gt this

/-- **Freedom.** Every weight assignment extends to a multiplicative character:
the log-character is additive on products of nonzero naturals. The prime axes
are independent; no relation among them is forced before coherence enters. -/
theorem logChar_mul (a : ℕ → ℝ) {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) :
    logChar a (m * n) = logChar a m + logChar a n := by
  unfold logChar
  rw [Nat.factorization_mul hm hn]
  rw [Finsupp.sum_add_index']
  · intro p; simp
  · intro p k1 k2; push_cast; ring

/-- **Independence of the axes.** Two log-characters that agree on all naturals
agree on every prime weight. The prime weights are genuine independent
coordinates of the character. -/
theorem faithful {a b : ℕ → ℝ} (h : ∀ n, logChar a n = logChar b n)
    {p : ℕ} (hp : p.Prime) : a p = b p := by
  have := h p
  rwa [logChar_prime a hp, logChar_prime b hp] at this

/-- **Prime-Axis Coherence Theorem.** A character obeys a single global power law
against the reference scale `w` if and only if its prime weights are all aligned
to `w`. The continuum/order condition that forces a global power law is exactly
the condition that synchronizes the independent prime axes into one common scale. -/
theorem powerLaw_iff_aligned (a w : ℕ → ℝ) : IsPowerLaw a w ↔ WeightsAligned a w := by
  constructor
  · rintro ⟨c, hc⟩
    refine ⟨c, ?_⟩
    intro p hp
    have h := hc p hp.ne_zero
    rwa [logChar_prime a hp, logChar_prime w hp] at h
  · rintro ⟨c, hc⟩
    refine ⟨c, ?_⟩
    intro n hn
    unfold logChar
    rw [Finsupp.sum, Finsupp.sum, Finset.mul_sum]
    apply Finset.sum_congr rfl
    intro p hp
    have hpp : p.Prime := by
      rw [Nat.support_factorization] at hp
      exact Nat.prime_of_mem_primeFactors hp
    rw [hc p hpp]
    ring

What this page does not claim

The declaration does not claim that the logarithm is the only possible log-character. It does not claim that the prime weights are forced to be logarithms by the definition of the log-character alone. It does not claim that the real logarithm is derived from the framework's axioms without the choice of reference weights.

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/PrimitiveRecognitionCalculus/PrimeAxisCoherence.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: