Foundation Primitive Recognition Calculus Prime Axis Coherence

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