Encyclopedia Foundation Foundation Primitive Recognition Calculus Prime Axis Coherence Character Is Rpow
ARTICLE 4 claims 4 theorems
Foundation Primitive Recognition Calculus Prime Axis Coherence Character Is Rpow
A theorem in the framework's machine-checked library shows that when independent prime factors are locked to one common scale, the resulting character is simply a power function.
The synchronized power map
A character here is a rule that assigns a real number to every positive integer, and the rule respects multiplication: the number assigned to a product is the sum of the numbers assigned to its factors. The framework's library, a machine-checked collection of formal theorems, proves that such rules are completely free until a coherence condition is imposed. Any assignment of weights to the prime numbers extends uniquely to a multiplicative character, and distinct assignments give distinct characters.
The theorem character_is_rpow states what happens when that freedom is constrained. If the weight assigned to each prime p equals a fixed exponent c times the natural logarithm of p, then the character is exactly the power map n ↦ n^c. The independent prime axes, once synchronized to one scale, collapse into a single global power law on the positive integers. The proof rests on an earlier result: a character obeys a power law against a reference scale if and only if its prime weights are aligned to that scale.
This is a statement about the framework's internal calculus, not a claim about the physical world. The theorem does not assert that any actual process in nature follows a power law, nor does it say which exponent c nature chooses. It establishes a structural equivalence: coherence among prime weights is exactly what produces a power map. The canonical reference scale w(p) = log p makes the log-character equal to the ordinary real logarithm, which is why the exponent c appears as a power rather than as a multiplier.
What the result changes is the picture of how structure emerges. Before coherence, the prime axes are independent coordinates with no forced relations. After coherence, they are locked to one scale and the character becomes a single smooth function. The theorem makes precise that the order condition which synchronizes the axes is the same condition that forces the global power law. This is a formal bridge between two descriptions: one in terms of independent prime weights, the other in terms of a single exponent.
THEOREM logChar_mul · faithful · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PrimeAxisCoherence.lean
/-- **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
THEOREM character_is_rpow · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PrimeAxisCoherence.lean
/-- **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
THEOREM powerLaw_iff_aligned · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PrimeAxisCoherence.lean
/-- **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
THEOREM logChar_log · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PrimeAxisCoherence.lean
/-- 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
What this page does not claim
The theorem does not assert that any natural process follows a power law. The theorem does not determine which exponent c, if any, nature realizes. The theorem does not claim that the prime axes are physically independent before coherence; it is a statement about the formal calculus.
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:
- What physical process, if any, selects the reference scale w(p) = log p?
- How does the coherence condition that aligns prime weights arise from the recognition ledger's order structure?
- Does the power-law equivalence extend from positive integers to positive rationals, and what changes at that boundary?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM logChar_mul · faithful · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PrimeAxisCoherence.lean
/-- **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 thisAny assignment of weights to the prime numbers extends uniquely to a multiplicative character, and distinct assignments give distinct characters. logChar_mul · faithful · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PrimeAxisCoherence.leanTHEOREM character_is_rpow · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PrimeAxisCoherence.lean
/-- **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 ringIf the weight assigned to each prime p equals a fixed exponent c times the natural logarithm of p, then the character is exactly the power map n ↦ n^c. character_is_rpow · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PrimeAxisCoherence.leanTHEOREM powerLaw_iff_aligned · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PrimeAxisCoherence.lean
/-- **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] ringA character obeys a power law against a reference scale if and only if its prime weights are aligned to that scale. powerLaw_iff_aligned · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PrimeAxisCoherence.leanTHEOREM logChar_log · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PrimeAxisCoherence.lean
/-- 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 thisWith the reference weights w(p) = log p, the log-character is exactly the real logarithm. logChar_log · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PrimeAxisCoherence.lean