IsPowerLaw
plain-language theorem explainer
A multiplicative character with prime weights a is a power law relative to a reference scale w when a single real exponent c equates their log-characters on every nonzero natural. Anyone proving prime-axis coherence or forced common scale cites this predicate. It is a pure definition: existence of one c with logChar a = c · logChar w off zero.
Claim. A pair of weight functions $a,w:\mathbb{N}\to\mathbb{R}$ defines a power-law character against the reference $w$ when there exists $c\in\mathbb{R}$ such that for every $n\neq 0$, the log-character of $a$ at $n$ equals $c$ times the log-character of $w$ at $n$.
background
In the primitive recognition calculus, each assignment of real weights to primes extends uniquely to a log-character on the positive integers by additivity over prime factorization: $\mathrm{logChar}(a,n)=\sum_p v_p(n),a(p)$. Multiplicativity $\mathrm{logChar}(a,mn)=\mathrm{logChar}(a,m)+\mathrm{logChar}(a,n)$ for nonzero $m,n$ is immediate from unique factorization.
The module studies when independent prime axes collapse to one common scale. The reference weights $w$ fix a preferred logarithmic ruler; a second weight system $a$ is then compared to $w$ through their log-characters. The present predicate packages the continuum condition that the two characters differ by a single global exponent.
Upstream, the log-character is the additive extension of prime weights; faithfulness later recovers the weights from the character on primes. The surrounding coherence theorems equate this global power-law condition with pointwise alignment of the prime weights themselves.
proof idea
Definition only: no proof obligations. The body is the existential statement that a single real $c$ satisfies $\mathrm{logChar},a,n = c\cdot\mathrm{logChar},w,n$ for all $n\neq 0$. Downstream lemmas unpack the quantifiers by specializing to primes and using multiplicativity of the log-character.
why it matters
This is the left-hand side of the Prime-Axis Coherence Theorem: a character obeys a single global power law against $w$ if and only if its prime weights are aligned to $w$. That equivalence (powerLaw_iff_aligned) is the synchronization step that turns independent prime axes into one scale.
It is re-exported as the third conjunct of the Phase 5 headline prime_axis_coherence (freedom then collapse: multiplicativity, faithfulness, and power-law iff alignment). Objecthood classification uses the same equivalence as classify_forced_scale: once coherence holds, the prime weights are forced to one common scale and the single exponent is forced.
In the Recognition forcing picture this is the algebraic skeleton of scale collapse: free prime data remain free until a global continuum/order condition (one power law) locks them to the reference ladder. It does not itself invoke $\varphi$, the eight-tick octave, or $D=3$; those enter only when the reference scale is specialized later.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.