IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PrimeAxisCoherence

   1/-
   2  PrimitiveRecognitionCalculus/PrimeAxisCoherence.lean
   3
   4  Phase 5 of the Delta-Native Analysis frontier: the Prime-Axis Coherence Theorem.
   5
   6  On the positive rationals the multiplicative group is free abelian on the
   7  primes. Before any continuity or order condition enters, a multiplicative
   8  character may be assigned an independent weight on every prime axis: the prime
   9  directions are independent. A log-character is exactly a choice of one real
  10  weight per prime, extended additively through prime factorization.
  11
  12  The coherence move is the collapse of that freedom. A character obeys a single
  13  global power law `χ(n) = exp(c · W(n))` (one exponent `c` against a fixed
  14  reference scale `W`) if and only if its prime weights are all aligned to that
  15  same reference, `a(p) = c · w(p)`. Independent prime axes are synchronized into
  16  one scale exactly when the global power law holds.
  17
  18  What is proved here:
  19
  20  * `logChar_one`, `logChar_mul`  : log-characters are additive (freedom: every
  21                                    weight assignment is a multiplicative character);
  22  * `logChar_prime`               : a log-character reads back its weight at a prime;
  23  * `faithful`                    : characters agreeing everywhere agree on every
  24                                    prime weight (the axes are independent coordinates);
  25  * `powerLaw_iff_aligned`        : THE collapse. Global power law ⟺ aligned prime
  26                                    weights, against any fixed reference scale `w`;
  27  * `logChar_log`                 : the canonical reference scale `w(p) = log p`
  28                                    gives `logChar log = log`;
  29  * `character_is_rpow`           : under the log reference, an aligned character is
  30                                    exactly `n ↦ n^c`.
  31
  32  No project-local axioms. No sorry.
  33-/
  34
  35import Mathlib
  36
  37namespace IndisputableMonolith
  38namespace Foundation
  39namespace PrimitiveRecognitionCalculus
  40namespace PrimeAxisCoherence
  41
  42open scoped BigOperators
  43
  44/-- The log-character with prime weights `a`: the additive extension of `a`
  45through prime factorization. `a p` is the log-value the character assigns to the
  46prime axis `p`. -/
  47noncomputable def logChar (a : ℕ → ℝ) (n : ℕ) : ℝ :=
  48  n.factorization.sum (fun p k => (k : ℝ) * a p)
  49
  50@[simp] theorem logChar_one (a : ℕ → ℝ) : logChar a 1 = 0 := by
  51  unfold logChar
  52  simp
  53
  54/-- **Freedom.** Every weight assignment extends to a multiplicative character:
  55the log-character is additive on products of nonzero naturals. The prime axes
  56are independent; no relation among them is forced before coherence enters. -/
  57theorem logChar_mul (a : ℕ → ℝ) {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) :
  58    logChar a (m * n) = logChar a m + logChar a n := by
  59  unfold logChar
  60  rw [Nat.factorization_mul hm hn]
  61  rw [Finsupp.sum_add_index']
  62  · intro p; simp
  63  · intro p k1 k2; push_cast; ring
  64
  65/-- A log-character reads back exactly its weight at a prime. -/
  66theorem logChar_prime (a : ℕ → ℝ) {p : ℕ} (hp : p.Prime) : logChar a p = a p := by
  67  unfold logChar
  68  rw [hp.factorization]
  69  rw [Finsupp.sum_single_index (by simp)]
  70  simp
  71
  72/-- **Independence of the axes.** Two log-characters that agree on all naturals
  73agree on every prime weight. The prime weights are genuine independent
  74coordinates of the character. -/
  75theorem faithful {a b : ℕ → ℝ} (h : ∀ n, logChar a n = logChar b n)
  76    {p : ℕ} (hp : p.Prime) : a p = b p := by
  77  have := h p
  78  rwa [logChar_prime a hp, logChar_prime b hp] at this
  79
  80/-- A character is a power law against the reference scale `w` if there is a
  81single exponent `c` with `logChar a n = c · logChar w n` for every nonzero `n`. -/
  82def IsPowerLaw (a w : ℕ → ℝ) : Prop :=
  83  ∃ c : ℝ, ∀ n : ℕ, n ≠ 0 → logChar a n = c * logChar w n
  84
  85/-- The prime weights of `a` are aligned to the reference `w` if a single
  86exponent `c` has `a p = c · w p` on every prime. -/
  87def WeightsAligned (a w : ℕ → ℝ) : Prop :=
  88  ∃ c : ℝ, ∀ p : ℕ, p.Prime → a p = c * w p
  89
  90/-- **Prime-Axis Coherence Theorem.** A character obeys a single global power law
  91against the reference scale `w` if and only if its prime weights are all aligned
  92to `w`. The continuum/order condition that forces a global power law is exactly
  93the condition that synchronizes the independent prime axes into one common scale. -/
  94theorem powerLaw_iff_aligned (a w : ℕ → ℝ) : IsPowerLaw a w ↔ WeightsAligned a w := by
  95  constructor
  96  · rintro ⟨c, hc⟩
  97    refine ⟨c, ?_⟩
  98    intro p hp
  99    have h := hc p hp.ne_zero
 100    rwa [logChar_prime a hp, logChar_prime w hp] at h
 101  · rintro ⟨c, hc⟩
 102    refine ⟨c, ?_⟩
 103    intro n hn
 104    unfold logChar
 105    rw [Finsupp.sum, Finsupp.sum, Finset.mul_sum]
 106    apply Finset.sum_congr rfl
 107    intro p hp
 108    have hpp : p.Prime := by
 109      rw [Nat.support_factorization] at hp
 110      exact Nat.prime_of_mem_primeFactors hp
 111    rw [hc p hpp]
 112    ring
 113
 114/-! ### The canonical reference scale `w(p) = log p` -/
 115
 116/-- With the reference weights `w(p) = log p`, the log-character is exactly the
 117real logarithm. This is the scale that the order/continuum condition selects. -/
 118theorem logChar_log (n : ℕ) (hn : n ≠ 0) :
 119    logChar (fun p => Real.log p) n = Real.log n := by
 120  unfold logChar
 121  rw [Finsupp.sum]
 122  have hself : n.factorization.prod (fun p k => p ^ k) = n :=
 123    Nat.factorization_prod_pow_eq_self hn
 124  have hcast : (n : ℝ) = ∏ p ∈ n.factorization.support, ((p : ℝ) ^ (n.factorization p)) := by
 125    conv_lhs => rw [← hself, Finsupp.prod]
 126    push_cast
 127    rfl
 128  rw [hcast, Real.log_prod]
 129  · apply Finset.sum_congr rfl
 130    intro p hp
 131    rw [Real.log_pow]
 132  · intro p hp
 133    have hpp : p.Prime := by
 134      rw [Nat.support_factorization] at hp
 135      exact Nat.prime_of_mem_primeFactors hp
 136    have : (0 : ℝ) < (p : ℝ) ^ (n.factorization p) := by
 137      apply pow_pos
 138      exact_mod_cast hpp.pos
 139    exact ne_of_gt this
 140
 141/-- **The synchronized character is a power map.** Under the log reference scale,
 142an aligned character with exponent `c` is exactly `n ↦ n^c`. The independent
 143prime axes, once locked to one scale, produce a single global power law on the
 144positive rationals. -/
 145theorem character_is_rpow {a : ℕ → ℝ} {c : ℝ}
 146    (haligned : ∀ p : ℕ, p.Prime → a p = c * Real.log p)
 147    (n : ℕ) (hn : n ≠ 0) :
 148    Real.exp (logChar a n) = (n : ℝ) ^ c := by
 149  have hpl : logChar a n = c * Real.log n := by
 150    have hdirect : logChar a n = c * logChar (fun p => Real.log p) n := by
 151      unfold logChar
 152      rw [Finsupp.sum, Finsupp.sum, Finset.mul_sum]
 153      apply Finset.sum_congr rfl
 154      intro p hp
 155      have hpp : p.Prime := by
 156        rw [Nat.support_factorization] at hp
 157        exact Nat.prime_of_mem_primeFactors hp
 158      rw [haligned p hpp]; ring
 159    rw [hdirect, logChar_log n hn]
 160  rw [hpl]
 161  have hnpos : (0 : ℝ) < n := by exact_mod_cast Nat.pos_of_ne_zero hn
 162  rw [Real.rpow_def_of_pos hnpos]
 163  congr 1
 164  ring
 165
 166/-- **Phase 5 headline.** Freedom then collapse, in one statement. Independent
 167prime weights always define a multiplicative character (`logChar_mul`), distinct
 168weights give distinct characters (`faithful`), and a global power law against any
 169fixed reference scale holds iff the prime weights are aligned to it
 170(`powerLaw_iff_aligned`). Coherence is the synchronization of independent prime
 171axes into one scale. -/
 172theorem prime_axis_coherence :
 173    (∀ (a : ℕ → ℝ) (m n : ℕ), m ≠ 0 → n ≠ 0 →
 174        logChar a (m * n) = logChar a m + logChar a n)
 175      ∧ (∀ (a b : ℕ → ℝ), (∀ n, logChar a n = logChar b n) →
 176          ∀ (p : ℕ), p.Prime → a p = b p)
 177      ∧ (∀ a w : ℕ → ℝ, IsPowerLaw a w ↔ WeightsAligned a w) := by
 178  refine ⟨?_, ?_, ?_⟩
 179  · intro a m n hm hn; exact logChar_mul a hm hn
 180  · intro a b h p hp; exact faithful h hp
 181  · exact powerLaw_iff_aligned
 182
 183end PrimeAxisCoherence
 184end PrimitiveRecognitionCalculus
 185end Foundation
 186end IndisputableMonolith
 187