classify_forced_scale
plain-language theorem explainer
Once prime-axis coherence holds as a single global power law against a reference scale, the prime weights are forced onto one common scale (a single exponent). Objecthood-registry and forced-classification arguments cite this equivalence. The proof is a one-line re-export of the prime-axis coherence iff.
Claim. For all $a,w:\mathbb{N}\to\mathbb{R}$, the sequence $a$ is a power law relative to the reference scale $w$ if and only if the prime weights of $a$ are aligned with $w$ (share one common exponent).
background
In the primitive recognition calculus, prime axes carry independent real weights. A log-character built from those weights is a power law against a reference scale $w$ when the weights sit on a single exponent relative to $w$. Alignment means exactly that common-scale condition on the primes.
Upstream, axis independence is already settled: if two log-characters agree on all naturals, they agree on every prime weight (the primes are genuine independent coordinates). The power-law predicate and the alignment predicate are therefore two readings of the same rigidity.
This module's objecthood registry sorts commitments by how much structure is forced versus conventional. The present lemma is the scale slot in that taxonomy: coherence forces the exponent.
proof idea
One-line term wrapper: the statement is definitionally the already-proved equivalence powerLaw_iff_aligned from PrimeAxisCoherence, applied universally to weight and scale sequences $a,w$. No extra cases or rewriting.
why it matters
Fills the forced scale cell in the objecthood registry's classification table (siblings cover rationals, display, completion, convention, quotient, observable, permitted). Doc-comment gloss: once coherence (a single global power law) holds, prime weights are forced to one common scale; coherence forces the single exponent.
That rigidity is the local reason a recognition ledger cannot smuggle independent prime scalings once a global power law is imposed. It sits under the foundation layer that feeds later forcing (unique $J$, $\varphi$, eight-tick structure) by keeping scale data from floating freely. No downstream consumers are wired yet; the lemma is registry infrastructure rather than a leaf of the T0–T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.