probWeight
plain-language theorem explainer
Defines the Born-rule weight of the zeroth slot of an eight-component complex amplitude: squared modulus of ψ₀ divided by the total squared norm. Used as the scale-invariant target in the vector witness of the scale-homogeneity no-go. The body is a one-line ratio of norms; invariance under joint positive scaling is proved separately.
Claim. For an eight-component complex amplitude $\psi : \mathrm{Fin}\,8 \to \mathbb{C}$, the probability weight of the first component is $p(\psi) = \|\psi_0\|^2 \big/ \sum_{i=0}^{7} \|\psi_i\|^2$.
background
The module ScaleHomogeneityNoGo is the boundary theorem of the forced skeleton: after the uniqueness chain (T-2 through T8) has fixed the dimensionless structure, no selection rule that is blind to joint rescaling of a posted value and its carrier can pin an absolute scale. The carrier may be any type with a positive-real scaling action; the module supplies two concrete witnesses.
One witness uses eight-component complex vectors. The natural scale-invariant observable on that space is the Born weight of a distinguished component: squared modulus over total squared norm. Joint multiplication of every component by a positive real cancels in the ratio, so the weight is homogeneous of degree zero. The eight-tick octave (T7) supplies the dimension of the configuration space; the definition itself is ordinary Hilbert-space probability.
proof idea
Pure definition: the right-hand side is the ratio of $|\psi,0|^2$ to the sum of $|\psi,i|^2$ over $i\in\mathrm{Fin},8$. No lemmas are invoked at the definition site. Downstream, probWeight_scaleInvariant expands the norms under scalar multiplication and factors $c^2$ from numerator and denominator.
why it matters
Feeds the vector witness of the scale-homogeneity no-go. The theorem vec_witness shows that no positivity selector that is jointly scale-invariant can force the posted real $a$ to equal this probability weight: the constant vector of ones has positive weight, yet any positive multiple is accepted while the posted value can be doubled away from the target. That witness, together with the real-pair witness, instantiates the abstract class theorem used in the paper "Recognition Composition and the Forced Skeleton" (S5 / boundary of the forced skeleton). It marks why the chain stops without a scale-bearing input and why the ledger-level T10 joint-scale result must import an external scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.