Foundation Primitive Recognition Calculus Prime Axis Coherence Prime Axis Cohere

Prime-axis coherence

A prime number is a building block of multiplication: every whole number is a product of primes in exactly one way. In Recognition Science, a framework that starts from the idea that reality keeps a discrete record of events, this factorization lets one assign a real number, a weight, to each prime and then extend that assignment to every whole number by addition. The extension is called a log-character. The framework's library, a machine-checked collection of formal theorems, proves that any such assignment automatically respects multiplication: the log-character of a product is the sum of the log-characters of its factors.

The theorem named prime_axis_coherence bundles three facts. First, the additivity just described always holds. Second, distinct assignments give distinct log-characters, so the prime weights are genuinely independent coordinates. Third, and this is the core, a log-character follows a single global power law against a fixed reference scale if and only if all its prime weights are aligned to that same scale by one common exponent. In symbols, the condition is that there exists a real number c such that for every prime p, the weight a(p) equals c times the reference weight w(p). The theorem states that this alignment is equivalent to the character being a power law, meaning logChar a n = c * logChar w n for every nonzero n.

The classical logarithm appears as the canonical reference scale. When the reference weights are w(p) = log p, the log-character of any nonzero natural number n is exactly Real.log n, the ordinary natural logarithm. Under this scale, an aligned character with exponent c is precisely the power map n ↦ n^c. The independent prime axes, once locked to one scale, produce a single global power law on the positive rationals. The theorem does not say that coherence is forced by the additivity and faithfulness conditions alone; those hold for any assignment. Coherence is the additional synchronization of the prime axes, and the theorem proves that this synchronization is exactly equivalent to the global power-law condition.

What the declaration does not claim is equally precise. It does not assert that any particular reference scale is physically selected; the theorem is conditional on a chosen w. It does not claim that the prime weights must be aligned, only that alignment is equivalent to a global power law. And it does not derive the value of the exponent c or the reference scale from first principles. The theorem is a structural equivalence, not a statement about which scale nature uses.

/-- **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

/-- 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

/-- **The synchronized character is a power map.** Under the log reference scale,
an aligned character with exponent `c` is exactly `n ↦ n^c`. The independent
prime axes, once locked to one scale, produce a single global power law on the
positive rationals. -/
theorem character_is_rpow {a : ℕ → ℝ} {c : ℝ}
    (haligned : ∀ p : ℕ, p.Prime → a p = c * Real.log p)
    (n : ℕ) (hn : n ≠ 0) :
    Real.exp (logChar a n) = (n : ℝ) ^ c := by
  have hpl : logChar a n = c * Real.log n := by
    have hdirect : logChar a n = c * logChar (fun p => Real.log p) n := by
      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 [haligned p hpp]; ring
    rw [hdirect, logChar_log n hn]
  rw [hpl]
  have hnpos : (0 : ℝ) < n := by exact_mod_cast Nat.pos_of_ne_zero hn
  rw [Real.rpow_def_of_pos hnpos]
  congr 1
  ring

What this page does not claim

The theorem does not assert that any particular reference scale is physically selected. The theorem does not claim that the prime weights must be aligned, only that alignment is equivalent to a global power law. The theorem does not derive the value of the exponent c or the reference scale from first principles.

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: