vecScaleAction
plain-language theorem explainer
Pointwise multiplication of an eight-component complex vector by a positive real, packaged as a scaling action. Anyone citing the vector witness of the scale-homogeneity no-go needs this carrier. The two action laws are discharged componentwise by function extensionality and elementary ring arithmetic.
Claim. The assignment $(c,\psi)\mapsto(i\mapsto c\cdot\psi_i)$ is a positive-real scaling action on $\mathbb{C}^8$: scaling by $1$ is the identity, and scaling by $c\cdot d$ equals successive scaling by $d$ then $c$.
background
The module proves the boundary theorem of the forced skeleton: no selection criterion blind to joint rescaling of a posted value and its carrier can fix an absolute scale-invariant target. The carrier is any type with a positive-real scaling action.
A scaling action records a map $\mathrm{scale}:\mathbb{R}\to X\to X$ together with the unit law $\mathrm{scale},1,x=x$ and the multiplicativity law $\mathrm{scale}(cd)x=\mathrm{scale},c(\mathrm{scale},d,x)$. The laws are part of the structure so instances cannot smuggle state-dependent rescaling.
Here $X$ is the space of eight-component complex vectors (indexed by $\mathrm{Fin},8$). The eight slots match the eight-tick octave of the forcing chain (T7). Downstream, the first-component Born weight $|\psi_0|^2/\sum_i|\psi_i|^2$ is the scale-invariant target on this carrier.
proof idea
Definitional instance, not a deep theorem. The scale field is pointwise multiplication by the real cast into $\mathbb{C}$. The unit law is funext then simp. Multiplicativity is funext, push_cast, and ring on each component. No external lemmas beyond Mathlib arithmetic.
why it matters
This is one of the two concrete carriers that instantiate the abstract scale-homogeneity no-go (the other is real pairs with a squared ratio). It feeds probWeight_scaleInvariant, which shows the first-component probability weight is invariant under the action, and vec_witness, which states that no scale-blind positivity criterion can recover absolute normalization from a probability profile.
In the paper "Recognition Composition and the Forced Skeleton" this is the configuration-space side of the boundary theorem: the uniqueness chain (T-2 through T8) derives the skeleton without a scale, so at least one scale-bearing input is required. The eight-component choice aligns with T7 (period $2^3$). The ledger-level mass-genesis instance is a separate specialization of the same class theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.