probWeight_scaleInvariant
plain-language theorem explainer
The first-component Born weight on eight-component complex vectors is unchanged under positive real rescaling of the whole amplitude vector. Anyone citing the scale-homogeneity no-go on quantum carriers needs this invariance hypothesis. The proof factors $c^2$ from numerator and denominator via multiplicativity of the complex norm and cancels.
Claim. Let $\mathrm{probWeight}(\psi)=\|\psi_0\|^2/\sum_{i=0}^{7}\|\psi_i\|^2$ on $\psi:\mathrm{Fin}\,8\to\mathbb{C}$. For every $c>0$ and every $\psi$, $\mathrm{probWeight}(c\cdot\psi)=\mathrm{probWeight}(\psi)$. Equivalently, the first-component probability weight is scale-invariant under the positive-real scaling action on eight-component amplitude vectors.
background
The module ScaleHomogeneityNoGo is the boundary theorem of the forced skeleton: the uniqueness chain (T-2 through T8) builds the theory without a scale, and this file proves abstractly why the chain cannot fix absolute normalizations on its own. A target functional is scale-invariant when rescaling the carrier leaves its value unchanged: for every $c>0$ and carrier $x$, $f(\mathrm{scale},c,x)=f(x)$.
The carrier here is eight-component complex amplitude vectors with the natural positive-real action (componentwise multiplication by $c$). The target is the first-component probability weight $|\psi_0|^2/\sum_i|\psi_i|^2$, the Born-rule profile of the zeroth slot. The eight-tick octave (T7) fixes the dimension of the configuration space; the same weight appears in the quantum-ledger probability of a configuration.
Two concrete witnesses instantiate the abstract no-go: real pairs with a squared ratio, and these eight-component vectors with the probability weight. The present lemma discharges the scale-invariance hypothesis for the vector witness.
proof idea
Term-mode proof by direct cancellation. Fix $c>0$ and $\psi$. Multiplicativity of the complex norm gives $|c\psi_i|=c|\psi_i|$ for each $i$ (using that $c$ is a positive real). The denominator sum therefore factors as $c^2\sum_i|\psi_i|^2$ by pulling $c^2$ through the finite sum; the numerator is $c^2|\psi_0|^2$. Cancel the common positive factor $c^2$ in the quotient (via $\mathrm{mul_div_mul_left}$ and $c^2\neq 0$).
why it matters
Feeds the vector witness of the scale-homogeneity no-go: no scale-blind criterion can recover an absolute normalization from a probability profile. That witness is the eight-component instantiation of the class theorem (the doubling decoy): any joint-scale-invariant selector that accepts the intended witness also accepts a doubled decoy whose posted value misses the scale-invariant target.
In the paper "Recognition Composition and the Forced Skeleton" this is the quantum-carrier side of the boundary theorem. The forcing chain stops at T8 without a scale; at least one scale-bearing input is required. The eight-tick octave (period $2^3$) fixes why the sum runs over $\mathrm{Fin},8$. The ledger-level MassGenesis instance is a separate specialization of the same class result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.