WeightsAligned
plain-language theorem explainer
Prime weights of a map a are aligned to a reference scale w when one real constant c satisfies a(p)=c·w(p) at every prime p. Downstream coherence theorems cite this as the discrete synchronization condition equivalent to a global power law. The declaration is pure definitional packaging of that existential Prop.
Claim. For $a,w:\mathbb{N}\to\mathbb{R}$, the prime weights of $a$ are aligned to the reference $w$ when there exists $c\in\mathbb{R}$ such that $a(p)=c\cdot w(p)$ for every prime $p$.
background
In the primitive recognition calculus, multiplicative characters on the positive integers are built from independent assignments of real weights on the primes (via a logarithmic character that is additive on coprime factors). A fixed reference scale $w$ (often a rung or $\phi$-ladder weight) supplies the comparison axis.
Alignment means those free prime weights are not independent after all: they sit on a single common ray through $w$. The companion predicate is a global power-law relation of $a$ against $w$ on all positive integers; the module's coherence theorem equates the two.
Local setting is Phase-5 prime-axis coherence: freedom of prime weights, faithfulness of the character map, then collapse to one scale when a continuum/order condition forces a power law.
proof idea
Definitional. The body is the Prop $\exists c:\mathbb{R},;\forall p\text{ prime},; a,p = c\cdot w,p$. No tactics or lemmas; downstream proofs unpack the witness $c$ or build it from a power-law exponent.
why it matters
This is the discrete half of the Prime-Axis Coherence Theorem: a character obeys a single global power law against $w$ iff its prime weights are aligned to $w$. It is the third conjunct of the Phase-5 headline prime_axis_coherence (freedom, faithfulness, then synchronization) and is re-exported by classify_forced_scale in the objecthood registry: once coherence holds, prime weights are forced to one common scale.
In framework terms it is the collapse step that turns independent prime axes into one rung relative to a reference (the continuum condition that forces the power law is exactly the synchronizer). It does not itself invoke T5–T8, but it is the bookkeeping predicate those later scale and spectrum constructions rely on when they treat a single exponent against $\phi$-ladder weights.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.