Encyclopedia Foundation Foundation Primitive Recognition Calculus Prime Axis Coherence Power Law Iff Ali
ARTICLE 3 claims 3 theorems
Foundation Primitive Recognition Calculus Prime Axis Coherence Power Law Iff Ali
A single global power law holds exactly when the independent prime axes are locked to one common scale.
The coherence theorem
A power law is a relationship where one quantity varies as a constant power of another, like the way the period of a pendulum grows with the square root of its length. In the Recognition Science framework, which studies how a discrete record of events, its ledger, can be structured, this idea takes a precise form. The framework assigns a weight to each prime number, and then extends that assignment to all whole numbers by multiplying through prime factorization. This creates a log-character, a function that turns multiplication into addition, much as a logarithm does.
The central theorem, named powerLaw_iff_aligned, states a clean equivalence. A character follows a single global power law against a fixed reference scale if and only if its prime weights are all aligned to that same reference scale. In plainer terms: the whole system obeys one uniform scaling rule precisely when each of its independent prime axes has been synchronized to a common exponent. Before this alignment is imposed, the prime axes are free; any assignment of weights extends to a valid character, and distinct assignments give distinct characters. The theorem shows that coherence, the condition forcing a global power law, is exactly this synchronization of the independent axes into one shared scale.
When the reference weights are chosen as the natural logarithms of the primes, the log-character becomes the ordinary real logarithm, and an aligned character with exponent c is precisely the power map n ↦ n^c. This gives a concrete picture: the independent prime axes, once locked together, produce a single smooth power law across all positive rationals. The theorem is proved in the framework's machine-checked library of formal theorems, where it appears as part of a larger result called prime_axis_coherence, which bundles together the freedom, the faithfulness, and this final collapse into one statement.
What the theorem does not claim is just as important. It does not say that any particular reference scale is forced; the equivalence holds for any fixed reference weights. It does not assert that the natural logarithm is the only possible choice, only that it is the scale selected by a separate order and continuity condition. And it says nothing about which exponent c might be physically realized. The theorem is a structural fact about how independent axes behave under coherence, not a prediction of any specific power law in nature.
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_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 logChar_log · character_is_rpow · 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
/-- **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
No particular reference scale is forced by the theorem; it holds for any fixed reference weights. The theorem does not predict any specific exponent c or any particular power law in physical systems. The natural logarithm is not derived as the only possible scale, only as the one selected by a separate condition.
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 order or continuity condition selects the natural logarithm as the canonical reference scale?
- How does the coherence of prime axes connect to the forcing chain that derives the golden ratio and three spatial dimensions?
- Which measured physical phenomena, if any, exhibit a power law with an exponent that this framework can predict?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
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] ringA character follows a single global power law against a fixed reference scale if and only if its prime weights are all aligned to that same reference scale. powerLaw_iff_aligned · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PrimeAxisCoherence.leanTHEOREM 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 thisBefore this alignment is imposed, the prime axes are free; any assignment of weights extends to a valid character, and distinct assignments give distinct characters. logChar_mul · faithful · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PrimeAxisCoherence.leanTHEOREM logChar_log · character_is_rpow · 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/-- **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 ringWhen the reference weights are chosen as the natural logarithms of the primes, the log-character becomes the ordinary real logarithm, and an aligned character with exponent c is precisely the power map n ↦ n^c. logChar_log · character_is_rpow · IndisputableMonolith/Foundation/PrimitiveRecognitionCalculus/PrimeAxisCoherence.lean