powerLaw_iff_aligned
plain-language theorem explainer
A multiplicative character on the naturals obeys a single global power law against a reference weight scale if and only if its values on primes are scalar multiples of that scale. Anyone citing prime-axis coherence or forced common scale uses this equivalence. The proof is a two-direction constructor: specialize the power law to primes one way, and expand the log-character through factorization the other.
Claim. For weight functions $a,w:\mathbb{N}\to\mathbb{R}$, the following are equivalent: (i) there exists $c\in\mathbb{R}$ such that $\mathrm{logChar}(a,n)=c\,\mathrm{logChar}(w,n)$ for every $n\neq 0$; (ii) there exists $c\in\mathbb{R}$ such that $a(p)=c\,w(p)$ for every prime $p$. Here $\mathrm{logChar}(a,n)$ is the additive extension of the prime weights $a$ through the prime factorization of $n$.
background
In the primitive recognition calculus, a character is specified by assigning a real weight to each prime axis and extending additively through factorization. Concretely, $\mathrm{logChar}(a,n)=\sum_p v_p(n),a(p)$, so multiplicativity $\mathrm{logChar}(a,mn)=\mathrm{logChar}(a,m)+\mathrm{logChar}(a,n)$ is automatic for nonzero $m,n$.
Two predicates compare a character $a$ to a fixed reference scale $w$. Being a power law means a single exponent $c$ works globally: $\mathrm{logChar}(a,n)=c,\mathrm{logChar}(w,n)$ for all $n\neq 0$. Weight alignment means the same scalar relation holds just on primes: $a(p)=c,w(p)$ whenever $p$ is prime.
The module's local claim is that continuum/order pressure forcing a global power law is exactly the condition that locks the independent prime axes onto one common scale. The companion fact $\mathrm{logChar}$ on a prime recovers the weight itself is the bridge between the two formulations.
proof idea
Bidirectional constructor on the two existential statements, sharing the same witness $c$.
Power-law to aligned: given $c$ with the global identity, restrict to a prime $p$. Rewrite both sides via the prime evaluation lemma for $\mathrm{logChar}$, which says $\mathrm{logChar}(a,p)=a(p)$ (and likewise for $w$), yielding $a(p)=c,w(p)$.
Aligned to power-law: given $c$ on primes, expand both $\mathrm{logChar}$ sums over the factorization support. Factor $c$ out of the sum, replace each prime weight $a(p)$ by $c,w(p)$ using alignment (after recovering primality of support elements from the factorization support), and finish by ring arithmetic on the coefficients.
why it matters
This is the coherence hinge of Phase 5: independent prime axes always define multiplicative characters and are faithful, but a global power law against any fixed reference holds exactly when the prime weights lock to one scale. The headline theorem packages the three facts together and quotes this equivalence as its third conjunct.
Downstream, the objecthood registry re-exports it as the forced-scale classifier: once coherence (a single global power law) holds, the prime weights are forced to one common scale. Under the canonical log reference $w(p)=\log p$, alignment plus this bridge yields the synchronized character as a pure power map $n\mapsto n^c$.
In Recognition terms, the continuum/order condition that selects a single scale is the synchronization step that collapses free prime axes into one coherent ladder, the arithmetic skeleton behind later forced scales and continuum structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.